%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN345-1 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n014.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 : Thu Jul 21 12:20:34 EDT 2022 % Result : Unsatisfiable 0.12s 0.40s % Output : Refutation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYN345-1 : TPTP v8.1.0. Released v1.2.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n014.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 : Mon Jul 11 19:35:04 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.40 % 0.12/0.40 SPASS V 3.9 % 0.12/0.40 SPASS beiseite: Proof found. % 0.12/0.40 % SZS status Theorem % 0.12/0.40 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.40 SPASS derived 7 clauses, backtracked 13 clauses, performed 2 splits and kept 21 clauses. % 0.12/0.40 SPASS allocated 63092 KBytes. % 0.12/0.40 SPASS spent 0:00:00.05 on the problem. % 0.12/0.40 0:00:00.03 for the input. % 0.12/0.40 0:00:00.00 for the FLOTTER CNF translation. % 0.12/0.40 0:00:00.00 for inferences. % 0.12/0.40 0:00:00.00 for the backtracking. % 0.12/0.40 0:00:00.00 for the reduction. % 0.12/0.40 % 0.12/0.40 % 0.12/0.40 Here is a proof with depth 1, length 28 : % 0.12/0.40 % SZS output start Refutation % 0.12/0.40 1[0:Inp] || f(a,a,b)* -> f(a,b,u)* f(a,b,b). % 0.12/0.40 3[0:Inp] || f(a,b,b) -> f(b,u,v)* f(a,a,b)*. % 0.12/0.40 4[0:Inp] || f(u,z__dfg(u,v),z__dfg(u,v))* f(a,b,b) -> f(a,a,b). % 0.12/0.40 5[0:Inp] || -> f(u,v,z__dfg(u,v))* f(a,a,b) f(a,b,b). % 0.12/0.40 6[0:Inp] || f(a,a,b) f(a,b,b) -> f(u,v,z__dfg(u,v))*. % 0.12/0.40 7[0:Inp] || f(b,b,u)* -> f(a,a,b)* f(a,b,b). % 0.12/0.40 8[0:Inp] || f(b,b,u)* f(a,a,b)* f(a,b,b) -> . % 0.12/0.40 9[0:Con:1.1] || f(a,a,b)* -> f(a,b,b). % 0.12/0.40 10[0:MRR:7.1,9.0] || f(b,b,u)*+ -> f(a,b,b)*. % 0.12/0.40 11[0:MRR:5.1,9.0] || -> f(u,v,z__dfg(u,v))* f(a,b,b). % 0.12/0.40 12[0:MRR:8.2,10.1] || f(b,b,u)* f(a,a,b)* -> . % 0.12/0.40 13[0:MRR:6.1,11.1] || f(a,a,b) -> f(u,v,z__dfg(u,v))*. % 0.12/0.40 14[1:Spt:9.0] || f(a,a,b)* -> . % 0.12/0.40 15[1:MRR:3.2,14.0] || f(a,b,b)* -> f(b,u,v)*. % 0.12/0.40 16[1:MRR:4.2,14.0] || f(u,z__dfg(u,v),z__dfg(u,v))* f(a,b,b) -> . % 0.12/0.40 17[2:Spt:10.1] || -> f(a,b,b)*. % 0.12/0.40 18[2:MRR:15.0,17.0] || -> f(b,u,v)*. % 0.12/0.40 19[2:MRR:16.1,17.0] || f(u,z__dfg(u,v),z__dfg(u,v))* -> . % 0.12/0.40 20[2:UnC:19.0,18.0] || -> . % 0.12/0.40 21[2:Spt:20.0,10.1,17.0] || f(a,b,b)* -> . % 0.12/0.40 22[2:Spt:20.0,10.0] || f(b,b,u)* -> . % 0.12/0.40 23[2:MRR:11.1,21.0] || -> f(u,v,z__dfg(u,v))*. % 0.12/0.40 24[2:UnC:23.0,22.0] || -> . % 0.12/0.40 25[1:Spt:24.0,9.0,14.0] || -> f(a,a,b)*. % 0.12/0.40 26[1:Spt:24.0,9.1] || -> f(a,b,b)*. % 0.12/0.40 27[1:MRR:12.1,25.0] || f(b,b,u)* -> . % 0.12/0.40 28[1:MRR:13.0,25.0] || -> f(u,v,z__dfg(u,v))*. % 0.12/0.40 29[1:UnC:28.0,27.0] || -> . % 0.12/0.40 % SZS output end Refutation % 0.12/0.40 Formulae used in the proof : clause1 clause3 clause4 clause5 clause6 clause7 clause8 % 0.12/0.40 %------------------------------------------------------------------------------