%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR039+1 : 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:30 EDT 2022 % Result : Theorem 0.62s 0.82s % Output : Refutation 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : CSR039+1 : TPTP v8.1.0. Released v3.4.0. % 0.00/0.10 % Command : run_spass %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Fri Jun 10 19:02:09 EDT 2022 % 0.09/0.29 % CPUTime : % 0.62/0.82 % 0.62/0.82 SPASS V 3.9 % 0.62/0.82 SPASS beiseite: Proof found. % 0.62/0.82 % SZS status Theorem % 0.62/0.82 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.62/0.82 SPASS derived 8900 clauses, backtracked 0 clauses, performed 0 splits and kept 2285 clauses. % 0.62/0.82 SPASS allocated 102024 KBytes. % 0.62/0.82 SPASS spent 0:00:00.47 on the problem. % 0.62/0.82 0:00:00.03 for the input. % 0.62/0.82 0:00:00.02 for the FLOTTER CNF translation. % 0.62/0.82 0:00:00.07 for inferences. % 0.62/0.82 0:00:00.00 for the backtracking. % 0.62/0.82 0:00:00.29 for the reduction. % 0.62/0.82 % 0.62/0.82 % 0.62/0.82 Here is a proof with depth 23, length 82 : % 0.62/0.82 % SZS output start Refutation % 0.62/0.82 8[0:Inp] || -> genls(c_tptpcol_2_2,c_tptpcol_1_1)*l. % 0.62/0.82 9[0:Inp] || -> genls(c_tptpcol_3_16386,c_tptpcol_2_2)*r. % 0.62/0.82 10[0:Inp] || -> genls(c_tptpcol_4_16387,c_tptpcol_3_16386)*r. % 0.62/0.82 11[0:Inp] || -> genls(c_tptpcol_5_16388,c_tptpcol_4_16387)*r. % 0.62/0.82 12[0:Inp] || -> genls(c_tptpcol_6_18436,c_tptpcol_5_16388)*r. % 0.62/0.82 13[0:Inp] || -> genls(c_tptpcol_7_18437,c_tptpcol_6_18436)*r. % 0.62/0.82 14[0:Inp] || -> genls(c_tptpcol_8_18438,c_tptpcol_7_18437)*r. % 0.62/0.82 15[0:Inp] || -> genls(c_tptpcol_9_18439,c_tptpcol_8_18438)*r. % 0.62/0.82 16[0:Inp] || -> genls(c_tptpcol_10_18567,c_tptpcol_9_18439)*r. % 0.62/0.82 17[0:Inp] || -> genls(c_tptpcol_11_18631,c_tptpcol_10_18567)*r. % 0.62/0.82 18[0:Inp] || -> genls(c_tptpcol_12_18663,c_tptpcol_11_18631)*r. % 0.62/0.82 19[0:Inp] || -> genls(c_tptpcol_13_18664,c_tptpcol_12_18663)*r. % 0.62/0.82 20[0:Inp] || -> genls(c_tptpcol_2_65537,c_tptpcol_1_65536)*l. % 0.62/0.82 21[0:Inp] || -> genls(c_tptpcol_3_81921,c_tptpcol_2_65537)*r. % 0.62/0.82 22[0:Inp] || -> genls(c_tptpcol_4_90113,c_tptpcol_3_81921)*r. % 0.62/0.82 23[0:Inp] || -> genls(c_tptpcol_5_90114,c_tptpcol_4_90113)*r. % 0.62/0.82 24[0:Inp] || -> genls(c_tptpcol_6_92162,c_tptpcol_5_90114)*r. % 0.62/0.82 25[0:Inp] || -> genls(c_tptpcol_7_93186,c_tptpcol_6_92162)*r. % 0.62/0.82 26[0:Inp] || -> genls(c_tptpcol_8_93698,c_tptpcol_7_93186)*r. % 0.62/0.82 27[0:Inp] || -> genls(c_tptpcol_9_93699,c_tptpcol_8_93698)*r. % 0.62/0.82 28[0:Inp] || -> genls(c_tptpcol_10_93700,c_tptpcol_9_93699)*r. % 0.62/0.82 29[0:Inp] || -> genls(c_tptpcol_11_93764,c_tptpcol_10_93700)*r. % 0.62/0.82 30[0:Inp] || -> genls(c_tptpcol_12_93765,c_tptpcol_11_93764)*r. % 0.62/0.82 31[0:Inp] || -> genls(c_tptpcol_13_93766,c_tptpcol_12_93765)*r. % 0.62/0.82 32[0:Inp] || -> genls(c_tptpcol_14_93774,c_tptpcol_13_93766)*r. % 0.62/0.82 33[0:Inp] || -> genls(c_tptpcol_15_93775,c_tptpcol_14_93774)*r. % 0.62/0.82 34[0:Inp] || -> disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)*. % 0.62/0.82 37[0:Inp] || disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)* -> . % 0.62/0.82 159[0:Inp] || disjointwith(u,v)*+ -> disjointwith(v,u)*. % 0.62/0.82 165[0:Inp] || genls(u,v)*+ disjointwith(w,v)* -> disjointwith(w,u)*. % 0.62/0.82 166[0:Inp] || genls(u,v)*+ disjointwith(v,w)* -> disjointwith(u,w)*. % 0.62/0.82 167[0:Inp] || genls(u,v)* genls(v,w)* -> genls(u,w)*. % 0.62/0.82 654[0:Res:25.0,166.0] || disjointwith(c_tptpcol_6_92162,u)* -> disjointwith(c_tptpcol_7_93186,u). % 0.62/0.82 655[0:Res:24.0,166.0] || disjointwith(c_tptpcol_5_90114,u)* -> disjointwith(c_tptpcol_6_92162,u). % 0.62/0.82 656[0:Res:23.0,166.0] || disjointwith(c_tptpcol_4_90113,u)* -> disjointwith(c_tptpcol_5_90114,u). % 0.62/0.82 657[0:Res:22.0,166.0] || disjointwith(c_tptpcol_3_81921,u)* -> disjointwith(c_tptpcol_4_90113,u). % 0.62/0.82 658[0:Res:21.0,166.0] || disjointwith(c_tptpcol_2_65537,u)* -> disjointwith(c_tptpcol_3_81921,u). % 0.62/0.82 670[0:Res:9.0,166.0] || disjointwith(c_tptpcol_2_2,u)* -> disjointwith(c_tptpcol_3_16386,u). % 0.62/0.82 671[0:Res:8.0,166.0] || disjointwith(c_tptpcol_1_1,u) -> disjointwith(c_tptpcol_2_2,u)*. % 0.62/0.82 676[0:NCh:167.2,167.1,166.0,32.0] || genls(u,c_tptpcol_14_93774)+ disjointwith(c_tptpcol_13_93766,v)* -> disjointwith(u,v)*. % 0.62/0.82 678[0:NCh:167.2,167.1,166.0,30.0] || genls(u,c_tptpcol_12_93765)+ disjointwith(c_tptpcol_11_93764,v)* -> disjointwith(u,v)*. % 0.62/0.82 680[0:NCh:167.2,167.1,166.0,28.0] || genls(u,c_tptpcol_10_93700)+ disjointwith(c_tptpcol_9_93699,v)* -> disjointwith(u,v)*. % 0.62/0.82 682[0:NCh:167.2,167.1,166.0,26.0] || genls(u,c_tptpcol_8_93698)+ disjointwith(c_tptpcol_7_93186,v)* -> disjointwith(u,v)*. % 0.62/0.82 712[0:Res:20.0,165.0] || disjointwith(u,c_tptpcol_1_65536) -> disjointwith(u,c_tptpcol_2_65537)*. % 0.62/0.82 713[0:Res:19.0,165.0] || disjointwith(u,c_tptpcol_12_18663)* -> disjointwith(u,c_tptpcol_13_18664). % 0.62/0.82 714[0:Res:18.0,165.0] || disjointwith(u,c_tptpcol_11_18631)* -> disjointwith(u,c_tptpcol_12_18663). % 0.62/0.82 715[0:Res:17.0,165.0] || disjointwith(u,c_tptpcol_10_18567)* -> disjointwith(u,c_tptpcol_11_18631). % 0.62/0.82 716[0:Res:16.0,165.0] || disjointwith(u,c_tptpcol_9_18439)* -> disjointwith(u,c_tptpcol_10_18567). % 0.62/0.82 717[0:Res:15.0,165.0] || disjointwith(u,c_tptpcol_8_18438)* -> disjointwith(u,c_tptpcol_9_18439). % 0.62/0.82 718[0:Res:14.0,165.0] || disjointwith(u,c_tptpcol_7_18437)* -> disjointwith(u,c_tptpcol_8_18438). % 0.62/0.82 719[0:Res:13.0,165.0] || disjointwith(u,c_tptpcol_6_18436)* -> disjointwith(u,c_tptpcol_7_18437). % 0.62/0.82 720[0:Res:12.0,165.0] || disjointwith(u,c_tptpcol_5_16388)* -> disjointwith(u,c_tptpcol_6_18436). % 0.62/0.82 721[0:Res:11.0,165.0] || disjointwith(u,c_tptpcol_4_16387)* -> disjointwith(u,c_tptpcol_5_16388). % 0.62/0.82 722[0:Res:10.0,165.0] || disjointwith(u,c_tptpcol_3_16386)* -> disjointwith(u,c_tptpcol_4_16387). % 0.62/0.82 1013[0:Res:712.1,670.0] || disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)* -> disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537). % 0.62/0.82 1732[0:Res:33.0,676.0] || disjointwith(c_tptpcol_13_93766,u)* -> disjointwith(c_tptpcol_15_93775,u). % 0.62/0.82 1778[0:Res:31.0,678.0] || disjointwith(c_tptpcol_11_93764,u)* -> disjointwith(c_tptpcol_13_93766,u). % 0.62/0.82 1837[0:Res:29.0,680.0] || disjointwith(c_tptpcol_9_93699,u)* -> disjointwith(c_tptpcol_11_93764,u). % 0.62/0.82 1882[0:Res:27.0,682.0] || disjointwith(c_tptpcol_7_93186,u)* -> disjointwith(c_tptpcol_9_93699,u). % 0.62/0.82 6375[0:Res:671.1,1013.0] || disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)* -> disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537). % 0.62/0.82 6376[0:MRR:6375.0,34.0] || -> disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)*. % 0.62/0.82 6378[0:Res:6376.0,159.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386)*. % 0.62/0.82 6388[0:Res:6378.0,722.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_4_16387)*. % 0.62/0.82 6411[0:Res:6388.0,721.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_5_16388)*. % 0.62/0.82 6446[0:Res:6411.0,720.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_6_18436)*. % 0.62/0.82 6499[0:Res:6446.0,719.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_7_18437)*. % 0.62/0.82 6566[0:Res:6499.0,718.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_8_18438)*. % 0.62/0.82 6651[0:Res:6566.0,717.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_9_18439)*. % 0.62/0.82 6748[0:Res:6651.0,716.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_10_18567)*. % 0.62/0.82 6863[0:Res:6748.0,715.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_11_18631)*. % 0.62/0.82 6980[0:Res:6863.0,714.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_12_18663)*. % 0.62/0.82 7095[0:Res:6980.0,713.0] || -> disjointwith(c_tptpcol_2_65537,c_tptpcol_13_18664)*. % 0.62/0.82 7221[0:Res:7095.0,658.0] || -> disjointwith(c_tptpcol_3_81921,c_tptpcol_13_18664)*. % 0.62/0.82 7354[0:Res:7221.0,657.0] || -> disjointwith(c_tptpcol_4_90113,c_tptpcol_13_18664)*. % 0.62/0.82 7492[0:Res:7354.0,656.0] || -> disjointwith(c_tptpcol_5_90114,c_tptpcol_13_18664)*. % 0.62/0.82 7653[0:Res:7492.0,655.0] || -> disjointwith(c_tptpcol_6_92162,c_tptpcol_13_18664)*. % 0.62/0.82 7870[0:Res:7653.0,654.0] || -> disjointwith(c_tptpcol_7_93186,c_tptpcol_13_18664)*. % 0.62/0.82 8123[0:Res:7870.0,1882.0] || -> disjointwith(c_tptpcol_9_93699,c_tptpcol_13_18664)*. % 0.62/0.82 8443[0:Res:8123.0,1837.0] || -> disjointwith(c_tptpcol_11_93764,c_tptpcol_13_18664)*. % 0.62/0.82 8829[0:Res:8443.0,1778.0] || -> disjointwith(c_tptpcol_13_93766,c_tptpcol_13_18664)*. % 0.62/0.82 9158[0:Res:8829.0,1732.0] || -> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)*. % 0.62/0.82 9160[0:MRR:9158.0,37.0] || -> . % 0.62/0.82 % SZS output end Refutation % 0.62/0.82 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 query39 just76 just77 just78 just139 % 0.62/0.82 %------------------------------------------------------------------------------