show/hide visualization coordinates
a : (0.9346716832137345, -0.03771732128225569, -0.1862836492828659)
b : (0.4346716832137345, -0.3263924558770686, -1.002780230210592)
c : (0.9346716832137345, 0.5396329479073699, -1.002780230210592)
d : (1.4346716832137345, 0.828308082502183, -0.1862836492828659)
e : (1.4346716832137345, 0.2509578133125572, 0.6302129316448601)
f : (0.57229924751794, -0.24693314457812304, 0.7219646411809971)
g : (0.07229924751794004, -0.535608279172936, -0.09453193974672891)
h : (-0.42770075248205996, -0.8242834137677488, -0.9110285206744548)
i : (-0.30270075248205996, -0.17476436092941983, -1.6610285206744548)
j : (-0.0653283167862655, 0.5396329479073699, -1.002780230210592)
k : (0.4346716832137345, 0.828308082502183, -0.1862836492828659)
l : (0.9346716832137345, 1.1169832170969958, 0.6302129316448601)
m : (0.8096716832137345, 0.4674641642586669, 1.3802129316448601)
n : (-0.052700752482059965, -0.030426793632013394, 1.471964641180997)
o : (-0.29007318817785444, -0.7448241024688033, 0.8137163507171341)
p : (-0.7900731881778544, -1.0334992370636162, -0.0027802302105919274)
q : (-1.4150731881778544, -0.8169928861175064, -0.7527802302105919)
r : (-0.92770075248206, 0.04174199001668988, -0.9110285206744548)
s : (-0.42770075248205996, 0.33041712461150274, -0.09453193974672891)
t : (0.07229924751794004, 0.6190922592063156, 0.7219646411809971)
u : (-0.7900731881778544, 0.12120130131563533, 0.8137163507171341)
v : (-1.2900731881778544, -0.7448241024688033, 0.8137163507171341)
w : (-1.2900731881778544, -0.16747383327917753, -0.0027802302105919274)
show/hide computer existence proof (failed)
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['s', 'w', 'r'], ['a', 'f', 'e'], ['m', 'n', 'f'], ['v', 'o', 'p'], ['j', 'k', 'c'], ['d', 'k', 'l'], ['n', 't', 'u'], ['i', 'h', 'r'], ['d', 'a', 'c'], ['f', 'm', 'e'], ['j', 's', 'r'], ['o', 'n', 'u'], ['i', 'j', 'r'], ['d', 'k', 'c'], ['i', 'h', 'b'], ['m', 'l', 't'], ['j', 'b', 'c'], ['d', 'l', 'e'], ['h', 'p', 'g'], ['i', 'j', 'b'], ['s', 'w', 'u'], ['a', 'g', 'b'], ['o', 'p', 'g'], ['s', 'k', 't'], ['v', 'w', 'u'], ['h', 'b', 'g'], ['r', 'w', 'q'], ['a', 'c', 'b'], ['h', 'r', 'q'], ['t', 'n', 'm'], ['j', 'k', 's'], ['a', 'g', 'f'], ['d', 'a', 'e'], ['h', 'p', 'q'], ['t', 's', 'u'], ['v', 'o', 'u'], ['v', 'p', 'w'], ['o', 'g', 'f'], ['o', 'n', 'f'], ['p', 'w', 'q'], ['l', 'm', 'e'], ['k', 'l', 't']]
Coordinate Data:
v : [-229343489015702678457247828559 / 5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, -1324115251201123049587486013463 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, 2839456501779039189984741976311 / 5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
q : [-1 / 8, -36084391824351610281821798781 / 500000000000000000000000000000, -1566496580927726032732428024901 / 1000000000000000000000000000000]
k : [215593108923948631137330254669 / 125000000000000000000000000000, 1573132184970986171164567532857 / 1000000000000000000000000000000, -1]
t : [340593108923948631137330254669 / 250000000000000000000000000000, 136391636167511885009143254693 / 100000000000000000000000000000, -91751709536136983633785987549 / 1000000000000000000000000000000]
h : [215593108923948631137330254669 / 250000000000000000000000000000, -19864827824736390295359851081 / 250000000000000000000000000000, -215593108923948631137330254669 / 125000000000000000000000000000]
w : [-2073916320693451954039853849289 / 250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, 577350269189625764509148780501 / 1000000000000000000000000000000, -816496580927726032732428024901 / 1000000000000000000000000000000]
i : [246843108923948631137330254669 / 250000000000000000000000000000, 28502987076969171194567648687 / 50000000000000000000000000000, -309343108923948631137330254669 / 125000000000000000000000000000]
u : [1 / 2, 13531646934131853855683174543 / 15625000000000000000000000000, -413767732144638140869898396041 / 2000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
o : [1, 2403365717362851833838769787737 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, -274376152898601059985659963187 / 2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
l : [278093108923948631137330254669 / 125000000000000000000000000000, 465451829891449763354785480777 / 250000000000000000000000000000, -91751709536136983633785987549 / 500000000000000000000000000000]
m : [262468108923948631137330254669 / 125000000000000000000000000000, 303072066681867517086587386261 / 250000000000000000000000000000, 566496580927726032732428024901 / 1000000000000000000000000000000]
p : [1 / 2, -1154700538379251529018297561 / 4000000000000000000000000000, -816496580927726032732428024901 / 1000000000000000000000000000000]
f : [465593108923948631137330254669 / 250000000000000000000000000000, 497890957890680203327709376177 / 1000000000000000000000000000000, -91751709536136983633785987549 / 1000000000000000000000000000000]
c : [278093108923948631137330254669 / 125000000000000000000000000000, 642228525188086644454996571303 / 500000000000000000000000000000, -1816496580927726032732428024901 / 1000000000000000000000000000000]
e : [340593108923948631137330254669 / 125000000000000000000000000000, 199156383156272081331083750471 / 200000000000000000000000000000, -91751709536136983633785987549 / 500000000000000000000000000000]
b : [215593108923948631137330254669 / 125000000000000000000000000000, 418431646591734642146269971853 / 1000000000000000000000000000000, -1816496580927726032732428024901 / 1000000000000000000000000000000]
r : [90593108923948631137330254669 / 250000000000000000000000000000, 196641523121373271395570941607 / 250000000000000000000000000000, -215593108923948631137330254669 / 125000000000000000000000000000]
d : [340593108923948631137330254669 / 125000000000000000000000000000, 1573132184970986171164567532857 / 1000000000000000000000000000000, -1]
n : [309343108923948631137330254669 / 250000000000000000000000000000, 357198654418394932509320084433 / 500000000000000000000000000000, 13164965809277260327324280249 / 20000000000000000000000000000]
s : [862372435695794524549320976813 / 1000000000000000000000000000000, 1075241227080305967836858229189 / 1000000000000000000000000000000, -18164965809277260327324280249 / 20000000000000000000000000000]
g : [681186217847897262274660530261 / 500000000000000000000000000000, 104607911647933660536567456723 / 500000000000000000000000000000, -18164965809277260327324280249 / 20000000000000000000000000000]
a : [278093108923948631137330254669 / 125000000000000000000000000000, 88388347648318440550105545263 / 125000000000000000000000000000, -1]
j : [153093108923948631137330254669 / 125000000000000000000000000000, 642228525188086644454996571303 / 500000000000000000000000000000, -1816496580927726032732428024901 / 1000000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 55533835000351005498688928538385288417313811658618413708569396482326294418865179408251979084447237336177482760652425849 / 111109741908026306461196281448996842617081561220000393912321865276328143997831980000000000000000000000000000000000000000
Collision distance in [353486447436111055408258575909 / 500000000000000000000000000000, 706972894872222110816517151819 / 1000000000000000000000000000000] ~ [0.70697, 0.70697]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [26401780079223227 / 100000000000000000000000000000000, 26403780079223227 / 100000000000000000000000000000000] ~ [0.0, 0.0]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 686729338140195296754301018596937287322163230033013044575615645271201163858467947160643079275105580204648438595975147637579981343363928761094697285631592368244928983954776264546876759247313007144773308281809139006595431378479336876816414090240512519764998747852649379397716952206717384538578576314571292901473963473572850392634966634167703677217671211638074479992165453780597446126577556013042239063261171046187161697132239070134752436610609126803561185206142839615849346283991515468659 / 5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [585973266514862133754808101197 / 50000000000000000000000000000000000000000000000000000000000, 635973266514862133754808101197 / 50000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [697053991351668426564439696293529 / 1269960629311003483440775561746880000000000000000000000000000000000, 697159602471985319472439696293529 / 1269960629311003483440775561746720000000000000000000000000000000000] ~ [0.0, 0.0]
Failed: unable to verify rho < sigma_min ^ 2 / (16 * E ^ .5)