%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR036+2 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 23:24:27 EDT 2022 % Result : Theorem 99.20s 99.46s % Output : Refutation 101.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.07 % Problem : CSR036+2 : TPTP v8.1.0. Released v3.4.0. % 0.02/0.08 % Command : run_spass %d %s % 0.06/0.26 % Computer : n032.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 600 % 0.06/0.26 % DateTime : Fri Jun 10 08:22:38 EDT 2022 % 0.06/0.26 % CPUTime : % 99.20/99.46 % 99.20/99.46 SPASS V 3.9 % 99.20/99.46 SPASS beiseite: Proof found. % 99.20/99.46 % SZS status Theorem % 99.20/99.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 99.20/99.46 SPASS derived 89170 clauses, backtracked 0 clauses, performed 0 splits and kept 71700 clauses. % 99.20/99.46 SPASS allocated 153689 KBytes. % 99.20/99.46 SPASS spent 0:1:39.12 on the problem. % 99.20/99.46 0:00:00.03 for the input. % 99.20/99.46 0:00:00.16 for the FLOTTER CNF translation. % 99.20/99.46 0:00:01.29 for inferences. % 99.20/99.46 0:00:00.00 for the backtracking. % 99.20/99.46 0:1:32.06 for the reduction. % 99.20/99.46 % 99.20/99.46 % 99.20/99.46 Here is a proof with depth 5, length 92 : % 99.20/99.46 % SZS output start Refutation % 99.20/99.46 26[0:Inp] || -> genls(c_tptpcol_10_72710,c_tptpcol_9_72709)*l. % 99.20/99.46 32[0:Inp] || -> genls(c_tptpcol_9_22021,c_tptpcol_8_22020)*l. % 99.20/99.46 34[0:Inp] || -> genls(c_tptpcol_14_72792,c_tptpcol_13_72791)*l. % 99.20/99.46 35[0:Inp] || -> genls(c_tptpcol_5_20483,c_tptpcol_4_16387)*r. % 99.20/99.46 36[0:Inp] || -> genls(c_tptpcol_11_22023,c_tptpcol_10_22022)*l. % 99.20/99.46 60[0:Inp] || -> genls(c_tptpcol_8_72708,c_tptpcol_7_72707)*l. % 99.20/99.46 92[0:Inp] || -> genls(c_tptpcol_2_2,c_tptpcol_1_1)*l. % 99.20/99.46 96[0:Inp] || -> disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)*. % 99.20/99.46 102[0:Inp] || -> genls(c_tptpcol_12_22055,c_tptpcol_11_22023)*r. % 99.20/99.46 112[0:Inp] || -> genls(c_tptpcol_14_22072,c_tptpcol_13_22071)*l. % 99.20/99.46 114[0:Inp] || -> genls(c_tptpcol_10_22022,c_tptpcol_9_22021)*r. % 99.20/99.46 117[0:Inp] || -> genls(c_tptpcol_9_72709,c_tptpcol_8_72708)*l. % 99.20/99.46 128[0:Inp] || -> genls(c_tptpcol_5_69635,c_tptpcol_4_65539)*l. % 99.20/99.46 130[0:Inp] || -> genls(c_tptpcol_13_22071,c_tptpcol_12_22055)*r. % 99.20/99.46 156[0:Inp] || -> genls(c_tptpcol_15_72793,c_tptpcol_14_72792)*r. % 99.20/99.46 158[0:Inp] || -> genls(c_tptpcol_4_16387,c_tptpcol_3_16386)*l. % 99.20/99.46 165[0:Inp] || -> genls(c_tptpcol_8_22020,c_tptpcol_7_21508)*l. % 99.20/99.46 167[0:Inp] || -> genls(c_tptpcol_3_65538,c_tptpcol_2_65537)*r. % 99.20/99.46 180[0:Inp] || -> genls(c_tptpcol_6_20484,c_tptpcol_5_20483)*r. % 99.20/99.46 186[0:Inp] || -> genls(c_tptpcol_2_65537,c_tptpcol_1_65536)*l. % 99.20/99.46 206[0:Inp] || -> genls(c_tptpcol_3_16386,c_tptpcol_2_2)*r. % 99.20/99.46 210[0:Inp] || -> genls(c_tptpcol_12_72775,c_tptpcol_11_72774)*l. % 99.20/99.46 211[0:Inp] || -> genls(c_tptpcol_7_72707,c_tptpcol_6_71683)*l. % 99.20/99.46 214[0:Inp] || -> genls(c_tptpcol_16_72795,c_tptpcol_15_72793)*l. % 99.20/99.46 215[0:Inp] || -> genls(c_tptpcol_6_71683,c_tptpcol_5_69635)*r. % 99.20/99.46 231[0:Inp] || -> genls(c_tptpcol_4_65539,c_tptpcol_3_65538)*l. % 99.20/99.46 233[0:Inp] || -> genls(c_tptpcol_15_22076,c_tptpcol_14_22072)*l. % 99.20/99.46 237[0:Inp] || -> genls(c_tptpcol_11_72774,c_tptpcol_10_72710)*r. % 99.20/99.46 241[0:Inp] || -> genls(c_tptpcol_7_21508,c_tptpcol_6_20484)*l. % 99.20/99.46 255[0:Inp] || -> genls(c_tptpcol_13_72791,c_tptpcol_12_72775)*l. % 99.20/99.46 268[0:Inp] || disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)* -> . % 99.20/99.46 1124[0:Inp] || genls(u,v)*+ disjointwith(w,v)* -> disjointwith(w,u)*. % 99.20/99.46 1125[0:Inp] || genls(u,v)*+ disjointwith(v,w)* -> disjointwith(u,w)*. % 99.20/99.46 6886[0:Res:241.0,1125.0] || disjointwith(c_tptpcol_6_20484,u) -> disjointwith(c_tptpcol_7_21508,u)*. % 99.20/99.46 6890[0:Res:233.0,1125.0] || disjointwith(c_tptpcol_14_22072,u) -> disjointwith(c_tptpcol_15_22076,u)*. % 99.20/99.46 6909[0:Res:206.0,1125.0] || disjointwith(c_tptpcol_2_2,u)* -> disjointwith(c_tptpcol_3_16386,u). % 99.20/99.46 6927[0:Res:180.0,1125.0] || disjointwith(c_tptpcol_5_20483,u)* -> disjointwith(c_tptpcol_6_20484,u). % 99.20/99.46 6936[0:Res:165.0,1125.0] || disjointwith(c_tptpcol_7_21508,u) -> disjointwith(c_tptpcol_8_22020,u)*. % 99.20/99.46 6939[0:Res:158.0,1125.0] || disjointwith(c_tptpcol_3_16386,u) -> disjointwith(c_tptpcol_4_16387,u)*. % 99.20/99.46 6956[0:Res:130.0,1125.0] || disjointwith(c_tptpcol_12_22055,u)* -> disjointwith(c_tptpcol_13_22071,u). % 99.20/99.46 6966[0:Res:114.0,1125.0] || disjointwith(c_tptpcol_9_22021,u)* -> disjointwith(c_tptpcol_10_22022,u). % 99.20/99.46 6968[0:Res:112.0,1125.0] || disjointwith(c_tptpcol_13_22071,u) -> disjointwith(c_tptpcol_14_22072,u)*. % 99.20/99.46 6975[0:Res:102.0,1125.0] || disjointwith(c_tptpcol_11_22023,u)* -> disjointwith(c_tptpcol_12_22055,u). % 99.20/99.46 6980[0:Res:92.0,1125.0] || disjointwith(c_tptpcol_1_1,u) -> disjointwith(c_tptpcol_2_2,u)*. % 99.20/99.46 7006[0:Res:36.0,1125.0] || disjointwith(c_tptpcol_10_22022,u) -> disjointwith(c_tptpcol_11_22023,u)*. % 99.20/99.46 7007[0:Res:35.0,1125.0] || disjointwith(c_tptpcol_4_16387,u)* -> disjointwith(c_tptpcol_5_20483,u). % 99.20/99.46 7010[0:Res:32.0,1125.0] || disjointwith(c_tptpcol_8_22020,u) -> disjointwith(c_tptpcol_9_22021,u)*. % 99.20/99.46 7171[0:Res:255.0,1124.0] || disjointwith(u,c_tptpcol_12_72775) -> disjointwith(u,c_tptpcol_13_72791)*. % 99.20/99.46 7184[0:Res:237.0,1124.0] || disjointwith(u,c_tptpcol_10_72710)* -> disjointwith(u,c_tptpcol_11_72774). % 99.20/99.46 7189[0:Res:231.0,1124.0] || disjointwith(u,c_tptpcol_3_65538) -> disjointwith(u,c_tptpcol_4_65539)*. % 99.20/99.46 7197[0:Res:215.0,1124.0] || disjointwith(u,c_tptpcol_5_69635)* -> disjointwith(u,c_tptpcol_6_71683). % 99.20/99.46 7198[0:Res:214.0,1124.0] || disjointwith(u,c_tptpcol_15_72793) -> disjointwith(u,c_tptpcol_16_72795)*. % 99.20/99.46 7201[0:Res:211.0,1124.0] || disjointwith(u,c_tptpcol_6_71683) -> disjointwith(u,c_tptpcol_7_72707)*. % 99.20/99.46 7202[0:Res:210.0,1124.0] || disjointwith(u,c_tptpcol_11_72774) -> disjointwith(u,c_tptpcol_12_72775)*. % 99.20/99.46 7219[0:Res:186.0,1124.0] || disjointwith(u,c_tptpcol_1_65536) -> disjointwith(u,c_tptpcol_2_65537)*. % 99.20/99.46 7231[0:Res:167.0,1124.0] || disjointwith(u,c_tptpcol_2_65537)* -> disjointwith(u,c_tptpcol_3_65538). % 99.20/99.46 7239[0:Res:156.0,1124.0] || disjointwith(u,c_tptpcol_14_72792)* -> disjointwith(u,c_tptpcol_15_72793). % 99.20/99.46 7254[0:Res:128.0,1124.0] || disjointwith(u,c_tptpcol_4_65539) -> disjointwith(u,c_tptpcol_5_69635)*. % 99.20/99.46 7261[0:Res:117.0,1124.0] || disjointwith(u,c_tptpcol_8_72708) -> disjointwith(u,c_tptpcol_9_72709)*. % 99.20/99.46 7293[0:Res:60.0,1124.0] || disjointwith(u,c_tptpcol_7_72707) -> disjointwith(u,c_tptpcol_8_72708)*. % 99.20/99.46 7306[0:Res:34.0,1124.0] || disjointwith(u,c_tptpcol_13_72791) -> disjointwith(u,c_tptpcol_14_72792)*. % 99.20/99.46 7309[0:Res:26.0,1124.0] || disjointwith(u,c_tptpcol_9_72709) -> disjointwith(u,c_tptpcol_10_72710)*. % 99.20/99.46 23642[0:Res:6890.1,268.0] || disjointwith(c_tptpcol_14_22072,c_tptpcol_16_72795)* -> . % 99.20/99.46 25037[0:Res:7171.1,6956.0] || disjointwith(c_tptpcol_12_22055,c_tptpcol_12_72775)* -> disjointwith(c_tptpcol_13_22071,c_tptpcol_13_72791). % 99.20/99.46 26168[0:Res:7006.1,7184.0] || disjointwith(c_tptpcol_10_22022,c_tptpcol_10_72710) -> disjointwith(c_tptpcol_11_22023,c_tptpcol_11_72774)*. % 99.20/99.46 26513[0:Res:7189.1,7007.0] || disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538)* -> disjointwith(c_tptpcol_5_20483,c_tptpcol_4_65539). % 99.20/99.46 27061[0:Res:6886.1,7197.0] || disjointwith(c_tptpcol_6_20484,c_tptpcol_5_69635) -> disjointwith(c_tptpcol_7_21508,c_tptpcol_6_71683)*. % 99.20/99.46 27420[0:Res:7201.1,6966.0] || disjointwith(c_tptpcol_9_22021,c_tptpcol_6_71683)* -> disjointwith(c_tptpcol_10_22022,c_tptpcol_7_72707). % 99.20/99.46 27489[0:Res:7202.1,6975.0] || disjointwith(c_tptpcol_11_22023,c_tptpcol_11_72774)* -> disjointwith(c_tptpcol_12_22055,c_tptpcol_12_72775). % 99.20/99.46 28772[0:Res:7219.1,6909.0] || disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)* -> disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537). % 99.20/99.46 29726[0:Res:6939.1,7231.0] || disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537) -> disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538)*. % 99.20/99.46 30263[0:Res:6968.1,7239.0] || disjointwith(c_tptpcol_13_22071,c_tptpcol_14_72792) -> disjointwith(c_tptpcol_14_22072,c_tptpcol_15_72793)*. % 99.20/99.46 31488[0:Res:7254.1,6927.0] || disjointwith(c_tptpcol_5_20483,c_tptpcol_4_65539)* -> disjointwith(c_tptpcol_6_20484,c_tptpcol_5_69635). % 99.20/99.46 87958[0:Res:7198.1,23642.0] || disjointwith(c_tptpcol_14_22072,c_tptpcol_15_72793)* -> . % 99.20/99.46 87960[0:MRR:30263.1,87958.0] || disjointwith(c_tptpcol_13_22071,c_tptpcol_14_72792)* -> . % 99.20/99.46 88221[0:Res:7306.1,87960.0] || disjointwith(c_tptpcol_13_22071,c_tptpcol_13_72791)* -> . % 99.20/99.46 88222[0:MRR:25037.1,88221.0] || disjointwith(c_tptpcol_12_22055,c_tptpcol_12_72775)* -> . % 99.20/99.46 88223[0:MRR:27489.1,88222.0] || disjointwith(c_tptpcol_11_22023,c_tptpcol_11_72774)* -> . % 99.20/99.46 88224[0:MRR:26168.1,88223.0] || disjointwith(c_tptpcol_10_22022,c_tptpcol_10_72710)* -> . % 99.20/99.46 88493[0:Res:7309.1,88224.0] || disjointwith(c_tptpcol_10_22022,c_tptpcol_9_72709)* -> . % 99.20/99.46 88803[0:Res:7261.1,88493.0] || disjointwith(c_tptpcol_10_22022,c_tptpcol_8_72708)* -> . % 99.20/99.46 89228[0:Res:7293.1,88803.0] || disjointwith(c_tptpcol_10_22022,c_tptpcol_7_72707)* -> . % 99.20/99.46 89229[0:MRR:27420.1,89228.0] || disjointwith(c_tptpcol_9_22021,c_tptpcol_6_71683)* -> . % 99.20/99.46 89625[0:Res:7010.1,89229.0] || disjointwith(c_tptpcol_8_22020,c_tptpcol_6_71683)* -> . % 99.20/99.46 90209[0:Res:6936.1,89625.0] || disjointwith(c_tptpcol_7_21508,c_tptpcol_6_71683)* -> . % 99.20/99.46 90210[0:MRR:27061.1,90209.0] || disjointwith(c_tptpcol_6_20484,c_tptpcol_5_69635)* -> . % 101.19/101.46 90211[0:MRR:31488.1,90210.0] || disjointwith(c_tptpcol_5_20483,c_tptpcol_4_65539)* -> . % 101.19/101.46 90212[0:MRR:26513.1,90211.0] || disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538)* -> . % 101.19/101.46 90213[0:MRR:29726.1,90212.0] || disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)* -> . % 101.19/101.46 90214[0:MRR:28772.1,90213.0] || disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)* -> . % 101.19/101.46 91104[0:Res:6980.1,90214.0] || disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)* -> . % 101.19/101.46 91105[0:MRR:91104.0,96.0] || -> . % 101.19/101.46 % SZS output end Refutation % 101.19/101.46 Formulae used in the proof : ax1_6 ax1_21 ax1_26 ax1_28 ax1_30 ax1_74 ax1_145 ax1_152 ax1_168 ax1_189 ax1_193 ax1_199 ax1_224 ax1_230 ax1_280 ax1_285 ax1_305 ax1_311 ax1_335 ax1_348 ax1_385 ax1_395 ax1_397 ax1_403 ax1_405 ax1_436 ax1_442 ax1_449 ax1_456 ax1_491 query86 ax1_1121 ax1_1122 % 101.19/101.46 %------------------------------------------------------------------------------