%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:20:00 AM UTC 2026 % Result : Theorem 0.55s 0.82s % Output : Refutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n006.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Mon Sep 7 14:19:01 UTC 2026 % 0.12/0.36 % CPUTime : % 0.55/0.82 % 0.55/0.82 SPASS V 3.9 % 0.55/0.82 SPASS beiseite: Proof found. % 0.55/0.82 % SZS status Theorem % 0.55/0.82 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.82 SPASS derived 1460 clauses, backtracked 287 clauses, performed 24 splits and kept 1179 clauses. % 0.55/0.82 SPASS allocated 98524 KBytes. % 0.55/0.82 SPASS spent 0:00:00.46 on the problem. % 0.55/0.82 0:00:00.06 for the input. % 0.55/0.82 0:00:00.06 for the FLOTTER CNF translation. % 0.55/0.82 0:00:00.03 for inferences. % 0.55/0.82 0:00:00.01 for the backtracking. % 0.55/0.82 0:00:00.25 for the reduction. % 0.55/0.82 % 0.55/0.82 % 0.55/0.82 Here is a proof with depth 4, length 209 : % 0.55/0.82 % SZS output start Refutation % 0.55/0.82 9[0:Inp] || -> leq(v400,skc5)*r. % 0.55/0.82 10[0:Inp] || -> leq(v200,skc4)*r. % 0.55/0.82 11[0:Inp] || -> leq(v100,skc3)*r. % 0.55/0.82 16[0:Inp] || -> less(v50,v100)*r. % 0.55/0.82 19[0:Inp] || -> less(v100,v200)*r. % 0.55/0.82 21[0:Inp] || -> less(v200,v400)*r. % 0.55/0.82 26[0:Inp] || equal(v100,v50)** -> . % 0.55/0.82 29[0:Inp] || equal(v200,v100)** -> . % 0.55/0.82 31[0:Inp] || equal(v400,v200)** -> . % 0.55/0.82 38[0:Inp] || less(u,v)* -> leq(u,v). % 0.55/0.82 41[0:Inp] || in_lopen(u,v,w)* -> less(v,u). % 0.55/0.82 42[0:Inp] || in_lopen(u,v,w)* -> leq(u,w). % 0.55/0.82 49[0:Inp] || leq(u,v)* -> equal(u,v) less(u,v). % 0.55/0.82 50[0:Inp] || less(u,v)* less(v,w)* -> less(u,w)*. % 0.55/0.82 51[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 0.55/0.82 54[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 0.55/0.82 55[0:Inp] || -> in_lopen(skc3,v0,v50) in_lopen(skc4,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.82 79[0:Res:11.0,51.0] || leq(skc3,v100)*l -> equal(skc3,v100). % 0.55/0.82 80[0:Res:11.0,49.0] || -> equal(skc3,v100) less(v100,skc3)*r. % 0.55/0.82 88[0:Res:10.0,51.0] || leq(skc4,v200)*l -> equal(skc4,v200). % 0.55/0.82 89[0:Res:10.0,49.0] || -> equal(skc4,v200) less(v200,skc4)*r. % 0.55/0.82 97[0:Res:9.0,51.0] || leq(skc5,v400)*l -> equal(skc5,v400). % 0.55/0.82 98[0:Res:9.0,49.0] || -> equal(skc5,v400) less(v400,skc5)*r. % 0.55/0.82 103[1:Spt:98.0] || -> equal(skc5,v400)**. % 0.55/0.82 107[1:Rew:103.0,55.2] || -> in_lopen(skc3,v0,v50) in_lopen(skc4,v0,v100)* in_lopen(v400,v0,v200). % 0.55/0.82 115[2:Spt:89.0] || -> equal(skc4,v200)**. % 0.55/0.82 123[2:Rew:115.0,107.1] || -> in_lopen(skc3,v0,v50)* in_lopen(v200,v0,v100) in_lopen(v400,v0,v200). % 0.55/0.82 127[3:Spt:80.0] || -> equal(skc3,v100)**. % 0.55/0.82 135[3:Rew:127.0,123.0] || -> in_lopen(v100,v0,v50) in_lopen(v200,v0,v100) in_lopen(v400,v0,v200)*. % 0.55/0.82 165[3:Res:135.2,42.0] || -> in_lopen(v100,v0,v50) in_lopen(v200,v0,v100)* leq(v400,v200). % 0.55/0.82 217[3:Res:165.1,42.0] || -> in_lopen(v100,v0,v50)* leq(v400,v200) leq(v200,v100). % 0.55/0.82 230[0:Res:21.0,38.0] || -> leq(v200,v400)*r. % 0.55/0.82 234[0:Res:19.0,38.0] || -> leq(v100,v200)*r. % 0.55/0.82 237[0:Res:16.0,38.0] || -> leq(v50,v100)*r. % 0.55/0.82 426[0:Res:234.0,51.0] || leq(v200,v100)*l -> equal(v200,v100). % 0.55/0.82 429[0:Res:230.0,51.0] || leq(v400,v200)*l -> equal(v400,v200). % 0.55/0.82 433[0:Res:237.0,51.0] || leq(v100,v50)*l -> equal(v100,v50). % 0.55/0.82 456[0:MRR:426.1,29.0] || leq(v200,v100)*l -> . % 0.55/0.82 457[3:MRR:217.2,456.0] || -> in_lopen(v100,v0,v50)* leq(v400,v200). % 0.55/0.82 460[0:MRR:429.1,31.0] || leq(v400,v200)*l -> . % 0.55/0.82 465[0:MRR:433.1,26.0] || leq(v100,v50)*l -> . % 0.55/0.82 468[3:MRR:457.1,460.0] || -> in_lopen(v100,v0,v50)*. % 0.55/0.82 470[3:Res:468.0,42.0] || -> leq(v100,v50)*l. % 0.55/0.82 471[3:MRR:470.0,465.0] || -> . % 0.55/0.82 472[3:Spt:471.0,80.0,127.0] || equal(skc3,v100)** -> . % 0.55/0.82 473[3:Spt:471.0,80.1] || -> less(v100,skc3)*r. % 0.55/0.82 474[3:MRR:79.1,472.0] || leq(skc3,v100)*l -> . % 0.55/0.82 483[0:Res:11.0,49.0] || -> equal(skc3,v100) less(v100,skc3)*r. % 0.55/0.82 487[0:NCh:54.2,54.1,11.0,49.0] || equal(u,v100) -> equal(u,skc3) less(u,skc3)*. % 0.55/0.82 488[2:Res:123.0,41.0] || -> in_lopen(v200,v0,v100) in_lopen(v400,v0,v200)* less(v0,skc3). % 0.55/0.82 489[2:Res:123.0,42.0] || -> in_lopen(v200,v0,v100) in_lopen(v400,v0,v200)* leq(skc3,v50). % 0.55/0.82 667[4:Spt:488.0] || -> in_lopen(v200,v0,v100)*. % 0.55/0.82 669[4:Res:667.0,42.0] || -> leq(v200,v100)*l. % 0.55/0.82 670[4:MRR:669.0,456.0] || -> . % 0.55/0.82 671[4:Spt:670.0,488.0,667.0] || in_lopen(v200,v0,v100)* -> . % 0.55/0.82 672[4:Spt:670.0,488.1,488.2] || -> in_lopen(v400,v0,v200)* less(v0,skc3). % 0.55/0.82 674[4:MRR:489.0,671.0] || -> in_lopen(v400,v0,v200)* leq(skc3,v50). % 0.55/0.82 675[5:Spt:672.0] || -> in_lopen(v400,v0,v200)*. % 0.55/0.82 677[5:Res:675.0,42.0] || -> leq(v400,v200)*l. % 0.55/0.82 678[5:MRR:677.0,460.0] || -> . % 0.55/0.82 679[5:Spt:678.0,672.0,675.0] || in_lopen(v400,v0,v200)* -> . % 0.55/0.82 680[5:Spt:678.0,672.1] || -> less(v0,skc3)*r. % 0.55/0.82 682[5:MRR:674.0,679.0] || -> leq(skc3,v50)*l. % 0.55/0.82 707[5:NCh:54.2,54.0,682.0,474.0] || leq(v50,v100)*r -> . % 0.55/0.82 710[5:MRR:707.0,237.0] || -> . % 0.55/0.82 711[2:Spt:710.0,89.0,115.0] || equal(skc4,v200)** -> . % 0.55/0.82 712[2:Spt:710.0,89.1] || -> less(v200,skc4)*r. % 0.55/0.82 713[2:MRR:88.1,711.0] || leq(skc4,v200)*l -> . % 0.55/0.82 728[0:Res:10.0,49.0] || -> equal(skc4,v200) less(v200,skc4)*r. % 0.55/0.82 745[3:Spt:483.0] || -> equal(skc3,v100)**. % 0.55/0.82 753[3:Rew:745.0,107.0] || -> in_lopen(v100,v0,v50) in_lopen(skc4,v0,v100)* in_lopen(v400,v0,v200). % 0.55/0.82 795[4:Spt:753.0] || -> in_lopen(v100,v0,v50)*. % 0.55/0.82 797[4:Res:795.0,42.0] || -> leq(v100,v50)*l. % 0.55/0.82 798[4:MRR:797.0,465.0] || -> . % 0.55/0.82 799[4:Spt:798.0,753.0,795.0] || in_lopen(v100,v0,v50)* -> . % 0.55/0.82 800[4:Spt:798.0,753.1,753.2] || -> in_lopen(skc4,v0,v100)* in_lopen(v400,v0,v200). % 0.55/0.82 803[5:Spt:800.0] || -> in_lopen(skc4,v0,v100)*. % 0.55/0.82 805[5:Res:803.0,42.0] || -> leq(skc4,v100)*l. % 0.55/0.82 829[5:NCh:54.2,54.0,805.0,713.0] || leq(v100,v200)*r -> . % 0.55/0.82 832[5:MRR:829.0,234.0] || -> . % 0.55/0.82 833[5:Spt:832.0,800.0,803.0] || in_lopen(skc4,v0,v100)* -> . % 0.55/0.82 834[5:Spt:832.0,800.1] || -> in_lopen(v400,v0,v200)*. % 0.55/0.82 836[5:Res:834.0,42.0] || -> leq(v400,v200)*l. % 0.55/0.82 837[5:MRR:836.0,460.0] || -> . % 0.55/0.82 838[3:Spt:837.0,483.0,745.0] || equal(skc3,v100)** -> . % 0.55/0.82 839[3:Spt:837.0,483.1] || -> less(v100,skc3)*r. % 0.55/0.82 840[3:MRR:79.1,838.0] || leq(skc3,v100)*l -> . % 0.55/0.82 853[0:Res:11.0,49.0] || -> equal(skc3,v100) less(v100,skc3)*r. % 0.55/0.82 867[4:Spt:107.0] || -> in_lopen(skc3,v0,v50)*. % 0.55/0.82 869[4:Res:867.0,42.0] || -> leq(skc3,v50)*l. % 0.55/0.82 890[4:NCh:54.2,54.0,869.0,840.0] || leq(v50,v100)*r -> . % 0.55/0.82 893[4:MRR:890.0,237.0] || -> . % 0.55/0.82 894[4:Spt:893.0,107.0,867.0] || in_lopen(skc3,v0,v50)* -> . % 0.55/0.82 895[4:Spt:893.0,107.1,107.2] || -> in_lopen(skc4,v0,v100)* in_lopen(v400,v0,v200). % 0.55/0.82 898[5:Spt:895.0] || -> in_lopen(skc4,v0,v100)*. % 0.55/0.82 900[5:Res:898.0,42.0] || -> leq(skc4,v100)*l. % 0.55/0.82 926[5:NCh:54.2,54.0,900.0,713.0] || leq(v100,v200)*r -> . % 0.55/0.82 929[5:MRR:926.0,234.0] || -> . % 0.55/0.82 930[5:Spt:929.0,895.0,898.0] || in_lopen(skc4,v0,v100)* -> . % 0.55/0.82 931[5:Spt:929.0,895.1] || -> in_lopen(v400,v0,v200)*. % 0.55/0.82 933[5:Res:931.0,42.0] || -> leq(v400,v200)*l. % 0.55/0.82 934[5:MRR:933.0,460.0] || -> . % 0.55/0.82 935[1:Spt:934.0,98.0,103.0] || equal(skc5,v400)** -> . % 0.55/0.82 936[1:Spt:934.0,98.1] || -> less(v400,skc5)*r. % 0.55/0.82 937[1:MRR:97.1,935.0] || leq(skc5,v400)*l -> . % 0.55/0.82 963[2:Spt:853.0] || -> equal(skc3,v100)**. % 0.55/0.82 995[2:Rew:963.0,55.0] || -> in_lopen(v100,v0,v50) in_lopen(skc4,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.82 1007[2:Res:995.2,42.0] || -> in_lopen(v100,v0,v50) in_lopen(skc4,v0,v100)* leq(skc5,v200). % 0.55/0.82 1008[3:Spt:728.0] || -> equal(skc4,v200)**. % 0.55/0.82 1012[3:Rew:1008.0,995.1] || -> in_lopen(v100,v0,v50) in_lopen(v200,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.82 1025[3:Rew:1008.0,1007.1] || -> in_lopen(v100,v0,v50) in_lopen(v200,v0,v100)* leq(skc5,v200). % 0.55/0.82 1036[4:Spt:1012.0] || -> in_lopen(v100,v0,v50)*. % 0.55/0.82 1038[4:Res:1036.0,42.0] || -> leq(v100,v50)*l. % 0.55/0.82 1039[4:MRR:1038.0,465.0] || -> . % 0.55/0.82 1040[4:Spt:1039.0,1012.0,1036.0] || in_lopen(v100,v0,v50)* -> . % 0.55/0.82 1041[4:Spt:1039.0,1012.1,1012.2] || -> in_lopen(v200,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.82 1042[4:MRR:1025.0,1040.0] || -> in_lopen(v200,v0,v100)* leq(skc5,v200). % 0.55/0.82 1044[5:Spt:1041.0] || -> in_lopen(v200,v0,v100)*. % 0.55/0.82 1046[5:Res:1044.0,42.0] || -> leq(v200,v100)*l. % 0.55/0.82 1047[5:MRR:1046.0,456.0] || -> . % 0.55/0.82 1048[5:Spt:1047.0,1041.0,1044.0] || in_lopen(v200,v0,v100)* -> . % 0.55/0.82 1049[5:Spt:1047.0,1041.1] || -> in_lopen(skc5,v0,v200)*. % 0.55/0.82 1050[5:MRR:1042.0,1048.0] || -> leq(skc5,v200)*l. % 0.55/0.82 1066[5:NCh:54.2,54.0,1050.0,937.0] || leq(v200,v400)*r -> . % 0.55/0.82 1069[5:MRR:1066.0,230.0] || -> . % 0.55/0.82 1070[3:Spt:1069.0,728.0,1008.0] || equal(skc4,v200)** -> . % 0.55/0.82 1071[3:Spt:1069.0,728.1] || -> less(v200,skc4)*r. % 0.55/0.82 1072[3:MRR:88.1,1070.0] || leq(skc4,v200)*l -> . % 0.55/0.82 1085[0:Res:10.0,49.0] || -> equal(skc4,v200) less(v200,skc4)*r. % 0.55/0.82 1092[4:Spt:995.0] || -> in_lopen(v100,v0,v50)*. % 0.55/0.82 1094[4:Res:1092.0,42.0] || -> leq(v100,v50)*l. % 0.55/0.82 1095[4:MRR:1094.0,465.0] || -> . % 0.55/0.82 1096[4:Spt:1095.0,995.0,1092.0] || in_lopen(v100,v0,v50)* -> . % 0.55/0.82 1097[4:Spt:1095.0,995.1,995.2] || -> in_lopen(skc4,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.82 1099[4:MRR:1007.0,1096.0] || -> in_lopen(skc4,v0,v100)* leq(skc5,v200). % 0.55/0.82 1100[5:Spt:1097.0] || -> in_lopen(skc4,v0,v100)*. % 0.55/0.82 1102[5:Res:1100.0,42.0] || -> leq(skc4,v100)*l. % 0.55/0.82 1124[5:NCh:54.2,54.0,1102.0,1072.0] || leq(v100,v200)*r -> . % 0.55/0.82 1127[5:MRR:1124.0,234.0] || -> . % 0.55/0.82 1128[5:Spt:1127.0,1097.0,1100.0] || in_lopen(skc4,v0,v100)* -> . % 0.55/0.84 1129[5:Spt:1127.0,1097.1] || -> in_lopen(skc5,v0,v200)*. % 0.55/0.84 1131[5:MRR:1099.0,1128.0] || -> leq(skc5,v200)*l. % 0.55/0.84 1155[5:NCh:54.2,54.0,1131.0,937.0] || leq(v200,v400)*r -> . % 0.55/0.84 1158[5:MRR:1155.0,230.0] || -> . % 0.55/0.84 1159[2:Spt:1158.0,853.0,963.0] || equal(skc3,v100)** -> . % 0.55/0.84 1160[2:Spt:1158.0,853.1] || -> less(v100,skc3)*r. % 0.55/0.84 1161[2:MRR:79.1,1159.0] || leq(skc3,v100)*l -> . % 0.55/0.84 1187[3:Spt:1085.0] || -> equal(skc4,v200)**. % 0.55/0.84 1203[3:Rew:1187.0,55.1] || -> in_lopen(skc3,v0,v50) in_lopen(v200,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.84 1212[3:Res:1203.2,41.0] || -> in_lopen(skc3,v0,v50)* in_lopen(v200,v0,v100) less(v0,skc5). % 0.55/0.84 1213[3:Res:1203.2,42.0] || -> in_lopen(skc3,v0,v50)* in_lopen(v200,v0,v100) leq(skc5,v200). % 0.55/0.84 1279[1:OCh:50.1,50.0,487.2,936.0] || equal(skc5,v100)** -> equal(skc5,skc3) less(v400,skc3). % 0.55/0.84 1294[4:Spt:1212.0] || -> in_lopen(skc3,v0,v50)*. % 0.55/0.84 1296[4:Res:1294.0,42.0] || -> leq(skc3,v50)*l. % 0.55/0.84 1317[4:NCh:54.2,54.0,1296.0,1161.0] || leq(v50,v100)*r -> . % 0.55/0.84 1320[4:MRR:1317.0,237.0] || -> . % 0.55/0.84 1321[4:Spt:1320.0,1212.0,1294.0] || in_lopen(skc3,v0,v50)* -> . % 0.55/0.84 1322[4:Spt:1320.0,1212.1,1212.2] || -> in_lopen(v200,v0,v100)* less(v0,skc5). % 0.55/0.84 1324[4:MRR:1213.0,1321.0] || -> in_lopen(v200,v0,v100)* leq(skc5,v200). % 0.55/0.84 1325[5:Spt:1322.0] || -> in_lopen(v200,v0,v100)*. % 0.55/0.84 1327[5:Res:1325.0,42.0] || -> leq(v200,v100)*l. % 0.55/0.84 1328[5:MRR:1327.0,456.0] || -> . % 0.55/0.84 1329[5:Spt:1328.0,1322.0,1325.0] || in_lopen(v200,v0,v100)* -> . % 0.55/0.84 1330[5:Spt:1328.0,1322.1] || -> less(v0,skc5)*r. % 0.55/0.84 1332[5:MRR:1324.0,1329.0] || -> leq(skc5,v200)*l. % 0.55/0.84 1358[5:NCh:54.2,54.0,1332.0,937.0] || leq(v200,v400)*r -> . % 0.55/0.84 1361[5:MRR:1358.0,230.0] || -> . % 0.55/0.84 1362[3:Spt:1361.0,1085.0,1187.0] || equal(skc4,v200)** -> . % 0.55/0.84 1363[3:Spt:1361.0,1085.1] || -> less(v200,skc4)*r. % 0.55/0.84 1364[3:MRR:88.1,1362.0] || leq(skc4,v200)*l -> . % 0.55/0.84 1394[0:Res:55.2,42.0] || -> in_lopen(skc3,v0,v50) in_lopen(skc4,v0,v100)* leq(skc5,v200). % 0.55/0.84 1433[4:Spt:1279.1] || -> equal(skc5,skc3)**. % 0.55/0.84 1437[4:Rew:1433.0,937.0] || leq(skc3,v400)*l -> . % 0.55/0.84 1446[4:Rew:1433.0,55.2] || -> in_lopen(skc3,v0,v50) in_lopen(skc4,v0,v100)* in_lopen(skc3,v0,v200). % 0.55/0.84 1476[4:Rew:1433.0,1394.2] || -> in_lopen(skc3,v0,v50) in_lopen(skc4,v0,v100)* leq(skc3,v200). % 0.55/0.84 1528[5:Spt:1446.0] || -> in_lopen(skc3,v0,v50)*. % 0.55/0.84 1530[5:Res:1528.0,42.0] || -> leq(skc3,v50)*l. % 0.55/0.84 1554[5:NCh:54.2,54.0,1530.0,1161.0] || leq(v50,v100)*r -> . % 0.55/0.84 1559[5:MRR:1554.0,237.0] || -> . % 0.55/0.84 1560[5:Spt:1559.0,1446.0,1528.0] || in_lopen(skc3,v0,v50)* -> . % 0.55/0.84 1561[5:Spt:1559.0,1446.1,1446.2] || -> in_lopen(skc4,v0,v100)* in_lopen(skc3,v0,v200). % 0.55/0.84 1562[5:MRR:1476.0,1560.0] || -> in_lopen(skc4,v0,v100)* leq(skc3,v200). % 0.55/0.84 1563[6:Spt:1561.0] || -> in_lopen(skc4,v0,v100)*. % 0.55/0.84 1565[6:Res:1563.0,42.0] || -> leq(skc4,v100)*l. % 0.55/0.84 1590[6:NCh:54.2,54.0,1565.0,1364.0] || leq(v100,v200)*r -> . % 0.55/0.84 1593[6:MRR:1590.0,234.0] || -> . % 0.55/0.84 1594[6:Spt:1593.0,1561.0,1563.0] || in_lopen(skc4,v0,v100)* -> . % 0.55/0.84 1595[6:Spt:1593.0,1561.1] || -> in_lopen(skc3,v0,v200)*. % 0.55/0.84 1598[6:MRR:1562.0,1594.0] || -> leq(skc3,v200)*l. % 0.55/0.84 1623[6:NCh:54.2,54.0,1598.0,1437.0] || leq(v200,v400)*r -> . % 0.55/0.84 1628[6:MRR:1623.0,230.0] || -> . % 0.55/0.84 1629[4:Spt:1628.0,1279.1,1433.0] || equal(skc5,skc3)** -> . % 0.55/0.84 1630[4:Spt:1628.0,1279.0,1279.2] || equal(skc5,v100)** -> less(v400,skc3). % 0.55/0.84 1665[5:Spt:55.0] || -> in_lopen(skc3,v0,v50)*. % 0.55/0.84 1667[5:Res:1665.0,42.0] || -> leq(skc3,v50)*l. % 0.55/0.84 1688[5:NCh:54.2,54.0,1667.0,1161.0] || leq(v50,v100)*r -> . % 0.55/0.84 1691[5:MRR:1688.0,237.0] || -> . % 0.55/0.84 1692[5:Spt:1691.0,55.0,1665.0] || in_lopen(skc3,v0,v50)* -> . % 0.55/0.84 1693[5:Spt:1691.0,55.1,55.2] || -> in_lopen(skc4,v0,v100) in_lopen(skc5,v0,v200)*. % 0.55/0.84 1694[5:MRR:1394.0,1692.0] || -> in_lopen(skc4,v0,v100)* leq(skc5,v200). % 0.55/0.84 1696[6:Spt:1693.0] || -> in_lopen(skc4,v0,v100)*. % 0.55/0.84 1698[6:Res:1696.0,42.0] || -> leq(skc4,v100)*l. % 0.55/0.84 1723[6:NCh:54.2,54.0,1698.0,1364.0] || leq(v100,v200)*r -> . % 0.55/0.84 1726[6:MRR:1723.0,234.0] || -> . % 0.55/0.84 1727[6:Spt:1726.0,1693.0,1696.0] || in_lopen(skc4,v0,v100)* -> . % 0.55/0.84 1728[6:Spt:1726.0,1693.1] || -> in_lopen(skc5,v0,v200)*. % 0.55/0.84 1729[6:MRR:1694.0,1727.0] || -> leq(skc5,v200)*l. % 0.55/0.84 1744[6:NCh:54.2,54.0,1729.0,937.0] || leq(v200,v400)*r -> . % 0.55/0.84 1747[6:MRR:1744.0,230.0] || -> . % 0.55/0.84 % SZS output end Refutation % 0.55/0.84 Formulae used in the proof : odrl445 ord_v50_v100 ord_v100_v200 ord_v200_v400 distinct less_implies_leq in_lopen leq_def transitive leq_antisym leq_trans % 0.55/0.84 %------------------------------------------------------------------------------