%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:39 EDT 2022 % Result : Theorem 0.42s 0.60s % Output : Refutation 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0. % 0.10/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 10 13:53:07 EDT 2022 % 0.12/0.33 % CPUTime : % 0.42/0.60 % 0.42/0.60 SPASS V 3.9 % 0.42/0.60 SPASS beiseite: Proof found. % 0.42/0.60 % SZS status Theorem % 0.42/0.60 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.42/0.60 SPASS derived 3234 clauses, backtracked 0 clauses, performed 0 splits and kept 1440 clauses. % 0.42/0.60 SPASS allocated 99184 KBytes. % 0.42/0.60 SPASS spent 0:00:00.26 on the problem. % 0.42/0.60 0:00:00.03 for the input. % 0.42/0.60 0:00:00.03 for the FLOTTER CNF translation. % 0.42/0.60 0:00:00.02 for inferences. % 0.42/0.60 0:00:00.00 for the backtracking. % 0.42/0.60 0:00:00.13 for the reduction. % 0.42/0.60 % 0.42/0.60 % 0.42/0.60 Here is a proof with depth 30, length 97 : % 0.42/0.60 % SZS output start Refutation % 0.42/0.60 10[0:Inp] || -> genls(c_tptpcol_2_2,c_tptpcol_1_1)*l. % 0.42/0.60 11[0:Inp] || -> genls(c_tptpcol_3_16386,c_tptpcol_2_2)*r. % 0.42/0.60 12[0:Inp] || -> genls(c_tptpcol_4_24578,c_tptpcol_3_16386)*r. % 0.42/0.60 13[0:Inp] || -> genls(c_tptpcol_5_24579,c_tptpcol_4_24578)*r. % 0.42/0.60 14[0:Inp] || -> genls(c_tptpcol_6_26627,c_tptpcol_5_24579)*r. % 0.42/0.60 15[0:Inp] || -> genls(c_tptpcol_7_26628,c_tptpcol_6_26627)*r. % 0.42/0.60 16[0:Inp] || -> genls(c_tptpcol_8_26629,c_tptpcol_7_26628)*r. % 0.42/0.60 17[0:Inp] || -> genls(c_tptpcol_9_26885,c_tptpcol_8_26629)*r. % 0.42/0.60 18[0:Inp] || -> genls(c_tptpcol_10_26886,c_tptpcol_9_26885)*r. % 0.42/0.60 19[0:Inp] || -> genls(c_tptpcol_11_26887,c_tptpcol_10_26886)*r. % 0.42/0.60 20[0:Inp] || -> genls(c_tptpcol_12_26919,c_tptpcol_11_26887)*r. % 0.42/0.60 21[0:Inp] || -> genls(c_tptpcol_13_26920,c_tptpcol_12_26919)*r. % 0.42/0.60 22[0:Inp] || -> genls(c_tptpcol_14_26921,c_tptpcol_13_26920)*r. % 0.42/0.60 23[0:Inp] || -> genls(c_tptpcol_15_26925,c_tptpcol_14_26921)*r. % 0.42/0.60 24[0:Inp] || -> genls(c_tptpcol_16_26926,c_tptpcol_15_26925)*r. % 0.42/0.60 25[0:Inp] || -> genls(c_tptpcol_2_65537,c_tptpcol_1_65536)*l. % 0.42/0.60 26[0:Inp] || -> genls(c_tptpcol_3_81921,c_tptpcol_2_65537)*r. % 0.42/0.60 27[0:Inp] || -> genls(c_tptpcol_4_90113,c_tptpcol_3_81921)*r. % 0.42/0.60 28[0:Inp] || -> genls(c_tptpcol_5_90114,c_tptpcol_4_90113)*r. % 0.42/0.60 29[0:Inp] || -> genls(c_tptpcol_6_92162,c_tptpcol_5_90114)*r. % 0.42/0.60 30[0:Inp] || -> genls(c_tptpcol_7_92163,c_tptpcol_6_92162)*r. % 0.42/0.60 31[0:Inp] || -> genls(c_tptpcol_8_92164,c_tptpcol_7_92163)*r. % 0.42/0.60 32[0:Inp] || -> genls(c_tptpcol_9_92165,c_tptpcol_8_92164)*r. % 0.42/0.60 33[0:Inp] || -> genls(c_tptpcol_10_92166,c_tptpcol_9_92165)*r. % 0.42/0.60 34[0:Inp] || -> genls(c_tptpcol_11_92230,c_tptpcol_10_92166)*r. % 0.42/0.60 35[0:Inp] || -> genls(c_tptpcol_12_92262,c_tptpcol_11_92230)*r. % 0.42/0.60 36[0:Inp] || -> genls(c_tptpcol_13_92263,c_tptpcol_12_92262)*r. % 0.42/0.60 37[0:Inp] || -> genls(c_tptpcol_14_92264,c_tptpcol_13_92263)*r. % 0.42/0.60 38[0:Inp] || -> genls(c_tptpcol_15_92268,c_tptpcol_14_92264)*r. % 0.42/0.60 39[0:Inp] || -> genls(c_tptpcol_16_92269,c_tptpcol_15_92268)*r. % 0.42/0.60 40[0:Inp] || -> disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)*. % 0.42/0.60 41[0:Inp] || disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)*+ -> . % 0.42/0.60 165[0:Inp] || disjointwith(u,v)*+ -> disjointwith(v,u)*. % 0.42/0.60 172[0:Inp] || genls(u,v)*+ disjointwith(v,w)* -> disjointwith(u,w)*. % 0.42/0.60 173[0:Inp] || genls(u,v)* genls(v,w)* -> genls(u,w)*. % 0.42/0.60 180[0:Res:172.2,41.0] || disjointwith(u,c_tptpcol_16_92269)* genls(c_tptpcol_16_26926,u)+ -> . % 0.42/0.60 367[0:Res:40.0,165.0] || -> disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)*. % 0.42/0.60 696[0:Res:39.0,172.0] || disjointwith(c_tptpcol_15_92268,u)*+ -> disjointwith(c_tptpcol_16_92269,u). % 0.42/0.60 697[0:Res:38.0,172.0] || disjointwith(c_tptpcol_14_92264,u)*+ -> disjointwith(c_tptpcol_15_92268,u). % 0.42/0.60 698[0:Res:37.0,172.0] || disjointwith(c_tptpcol_13_92263,u)*+ -> disjointwith(c_tptpcol_14_92264,u). % 0.42/0.60 699[0:Res:36.0,172.0] || disjointwith(c_tptpcol_12_92262,u)*+ -> disjointwith(c_tptpcol_13_92263,u). % 0.42/0.60 700[0:Res:35.0,172.0] || disjointwith(c_tptpcol_11_92230,u)*+ -> disjointwith(c_tptpcol_12_92262,u). % 0.42/0.60 701[0:Res:34.0,172.0] || disjointwith(c_tptpcol_10_92166,u)*+ -> disjointwith(c_tptpcol_11_92230,u). % 0.42/0.60 702[0:Res:33.0,172.0] || disjointwith(c_tptpcol_9_92165,u)*+ -> disjointwith(c_tptpcol_10_92166,u). % 0.42/0.60 703[0:Res:32.0,172.0] || disjointwith(c_tptpcol_8_92164,u)*+ -> disjointwith(c_tptpcol_9_92165,u). % 0.42/0.60 704[0:Res:31.0,172.0] || disjointwith(c_tptpcol_7_92163,u)*+ -> disjointwith(c_tptpcol_8_92164,u). % 0.42/0.60 705[0:Res:30.0,172.0] || disjointwith(c_tptpcol_6_92162,u)*+ -> disjointwith(c_tptpcol_7_92163,u). % 0.42/0.60 706[0:Res:29.0,172.0] || disjointwith(c_tptpcol_5_90114,u)*+ -> disjointwith(c_tptpcol_6_92162,u). % 0.42/0.60 707[0:Res:28.0,172.0] || disjointwith(c_tptpcol_4_90113,u)*+ -> disjointwith(c_tptpcol_5_90114,u). % 0.42/0.60 708[0:Res:27.0,172.0] || disjointwith(c_tptpcol_3_81921,u)*+ -> disjointwith(c_tptpcol_4_90113,u). % 0.42/0.60 709[0:Res:26.0,172.0] || disjointwith(c_tptpcol_2_65537,u)*+ -> disjointwith(c_tptpcol_3_81921,u). % 0.42/0.60 710[0:Res:25.0,172.0] || disjointwith(c_tptpcol_1_65536,u)+ -> disjointwith(c_tptpcol_2_65537,u)*. % 0.42/0.60 713[0:Res:22.0,172.0] || disjointwith(c_tptpcol_13_26920,u)*+ -> disjointwith(c_tptpcol_14_26921,u). % 0.42/0.60 714[0:Res:21.0,172.0] || disjointwith(c_tptpcol_12_26919,u)*+ -> disjointwith(c_tptpcol_13_26920,u). % 0.42/0.60 715[0:Res:20.0,172.0] || disjointwith(c_tptpcol_11_26887,u)*+ -> disjointwith(c_tptpcol_12_26919,u). % 0.42/0.60 716[0:Res:19.0,172.0] || disjointwith(c_tptpcol_10_26886,u)*+ -> disjointwith(c_tptpcol_11_26887,u). % 0.42/0.60 717[0:Res:18.0,172.0] || disjointwith(c_tptpcol_9_26885,u)*+ -> disjointwith(c_tptpcol_10_26886,u). % 0.42/0.60 718[0:Res:17.0,172.0] || disjointwith(c_tptpcol_8_26629,u)*+ -> disjointwith(c_tptpcol_9_26885,u). % 0.42/0.60 719[0:Res:16.0,172.0] || disjointwith(c_tptpcol_7_26628,u)*+ -> disjointwith(c_tptpcol_8_26629,u). % 0.42/0.60 720[0:Res:15.0,172.0] || disjointwith(c_tptpcol_6_26627,u)*+ -> disjointwith(c_tptpcol_7_26628,u). % 0.42/0.60 721[0:Res:14.0,172.0] || disjointwith(c_tptpcol_5_24579,u)*+ -> disjointwith(c_tptpcol_6_26627,u). % 0.42/0.60 722[0:Res:13.0,172.0] || disjointwith(c_tptpcol_4_24578,u)*+ -> disjointwith(c_tptpcol_5_24579,u). % 0.42/0.60 723[0:Res:12.0,172.0] || disjointwith(c_tptpcol_3_16386,u)*+ -> disjointwith(c_tptpcol_4_24578,u). % 0.42/0.60 724[0:Res:11.0,172.0] || disjointwith(c_tptpcol_2_2,u)*+ -> disjointwith(c_tptpcol_3_16386,u). % 0.42/0.60 725[0:Res:10.0,172.0] || disjointwith(c_tptpcol_1_1,u)+ -> disjointwith(c_tptpcol_2_2,u)*. % 0.42/0.60 893[0:Res:367.0,710.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1)*. % 0.42/0.60 898[0:Res:893.0,709.0] || -> disjointwith(c_tptpcol_3_81921,c_tptpcol_1_1)*. % 0.42/0.60 907[0:Res:898.0,708.0] || -> disjointwith(c_tptpcol_4_90113,c_tptpcol_1_1)*. % 0.42/0.60 916[0:Res:907.0,707.0] || -> disjointwith(c_tptpcol_5_90114,c_tptpcol_1_1)*. % 0.42/0.60 925[0:Res:916.0,706.0] || -> disjointwith(c_tptpcol_6_92162,c_tptpcol_1_1)*. % 0.42/0.60 934[0:Res:925.0,705.0] || -> disjointwith(c_tptpcol_7_92163,c_tptpcol_1_1)*. % 0.42/0.60 943[0:Res:934.0,704.0] || -> disjointwith(c_tptpcol_8_92164,c_tptpcol_1_1)*. % 0.42/0.60 952[0:Res:943.0,703.0] || -> disjointwith(c_tptpcol_9_92165,c_tptpcol_1_1)*. % 0.42/0.60 961[0:Res:952.0,702.0] || -> disjointwith(c_tptpcol_10_92166,c_tptpcol_1_1)*. % 0.42/0.60 970[0:Res:961.0,701.0] || -> disjointwith(c_tptpcol_11_92230,c_tptpcol_1_1)*. % 0.42/0.60 979[0:Res:970.0,700.0] || -> disjointwith(c_tptpcol_12_92262,c_tptpcol_1_1)*. % 0.42/0.60 988[0:Res:979.0,699.0] || -> disjointwith(c_tptpcol_13_92263,c_tptpcol_1_1)*. % 0.42/0.60 997[0:Res:988.0,698.0] || -> disjointwith(c_tptpcol_14_92264,c_tptpcol_1_1)*. % 0.42/0.60 1006[0:Res:997.0,697.0] || -> disjointwith(c_tptpcol_15_92268,c_tptpcol_1_1)*. % 0.42/0.60 1015[0:Res:1006.0,696.0] || -> disjointwith(c_tptpcol_16_92269,c_tptpcol_1_1)*. % 0.42/0.60 1021[0:Res:1015.0,165.0] || -> disjointwith(c_tptpcol_1_1,c_tptpcol_16_92269)*. % 0.42/0.60 1043[0:Res:1021.0,725.0] || -> disjointwith(c_tptpcol_2_2,c_tptpcol_16_92269)*. % 0.42/0.60 1131[0:Res:1043.0,724.0] || -> disjointwith(c_tptpcol_3_16386,c_tptpcol_16_92269)*. % 0.42/0.60 1318[0:Res:1131.0,723.0] || -> disjointwith(c_tptpcol_4_24578,c_tptpcol_16_92269)*. % 0.42/0.60 1501[0:Res:1318.0,722.0] || -> disjointwith(c_tptpcol_5_24579,c_tptpcol_16_92269)*. % 0.42/0.60 1707[0:Res:1501.0,721.0] || -> disjointwith(c_tptpcol_6_26627,c_tptpcol_16_92269)*. % 0.42/0.60 1935[0:Res:1707.0,720.0] || -> disjointwith(c_tptpcol_7_26628,c_tptpcol_16_92269)*. % 0.42/0.60 2133[0:Res:1935.0,719.0] || -> disjointwith(c_tptpcol_8_26629,c_tptpcol_16_92269)*. % 0.42/0.60 2331[0:Res:2133.0,718.0] || -> disjointwith(c_tptpcol_9_26885,c_tptpcol_16_92269)*. % 0.42/0.60 2529[0:Res:2331.0,717.0] || -> disjointwith(c_tptpcol_10_26886,c_tptpcol_16_92269)*. % 0.42/0.60 2765[0:Res:2529.0,716.0] || -> disjointwith(c_tptpcol_11_26887,c_tptpcol_16_92269)*. % 0.42/0.60 2867[0:NCh:173.2,173.1,180.1,23.0] || disjointwith(c_tptpcol_14_26921,c_tptpcol_16_92269)* genls(c_tptpcol_16_26926,c_tptpcol_15_26925) -> . % 0.42/0.60 2881[0:MRR:2867.1,24.0] || disjointwith(c_tptpcol_14_26921,c_tptpcol_16_92269)* -> . % 0.42/0.60 3055[0:Res:2765.0,715.0] || -> disjointwith(c_tptpcol_12_26919,c_tptpcol_16_92269)*. % 0.42/0.60 3286[0:Res:3055.0,714.0] || -> disjointwith(c_tptpcol_13_26920,c_tptpcol_16_92269)*. % 0.43/0.61 3510[0:Res:3286.0,713.0] || -> disjointwith(c_tptpcol_14_26921,c_tptpcol_16_92269)*. % 0.43/0.61 3511[0:MRR:3510.0,2881.0] || -> . % 0.43/0.61 % SZS output end Refutation % 0.43/0.61 Formulae used in the proof : just7 just9 just11 just13 just15 just17 just19 just21 just23 just25 just27 just29 just31 just33 just35 just37 just39 just41 just43 just45 just47 just49 just51 just53 just55 just57 just59 just61 just63 just65 just67 query49 just84 just86 just155 % 0.43/0.61 %------------------------------------------------------------------------------