%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD066-3 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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 : Sat Jul 16 02:28:37 EDT 2022 % Result : Unsatisfiable 1.40s 1.58s % Output : Refutation 1.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : FLD066-3 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n023.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 : Tue Jun 7 00:47:54 EDT 2022 % 0.12/0.33 % CPUTime : % 1.40/1.58 % 1.40/1.58 SPASS V 3.9 % 1.40/1.58 SPASS beiseite: Proof found. % 1.40/1.58 % SZS status Theorem % 1.40/1.58 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.40/1.58 SPASS derived 3521 clauses, backtracked 0 clauses, performed 5 splits and kept 2863 clauses. % 1.40/1.58 SPASS allocated 79212 KBytes. % 1.40/1.58 SPASS spent 0:00:01.22 on the problem. % 1.40/1.58 0:00:00.04 for the input. % 1.40/1.58 0:00:00.00 for the FLOTTER CNF translation. % 1.40/1.58 0:00:00.03 for inferences. % 1.40/1.58 0:00:00.00 for the backtracking. % 1.40/1.58 0:00:01.11 for the reduction. % 1.40/1.58 % 1.40/1.58 % 1.40/1.58 Here is a proof with depth 5, length 36 : % 1.40/1.58 % SZS output start Refutation % 1.40/1.58 1[0:Inp] || -> defined(a)*. % 1.40/1.58 2[0:Inp] || -> defined(b)*. % 1.40/1.58 3[0:Inp] || -> defined(c)*. % 1.40/1.58 6[0:Inp] || -> sum__dfg(a,c,u__dfg)*. % 1.40/1.58 7[0:Inp] || -> sum__dfg(b,c,v__dfg)*. % 1.40/1.58 8[0:Inp] || -> less_or_equal(u__dfg,v__dfg)*l. % 1.40/1.58 9[0:Inp] || less_or_equal(a,b)*l -> . % 1.40/1.58 10[0:Inp] || sum__dfg(u,v,w)*+ sum__dfg(x,v,y)* sum__dfg(z,x,u)* -> sum__dfg(z,y,w)*. % 1.40/1.58 11[0:Inp] || sum__dfg(u,v,w)*+ sum__dfg(x,y,v)* sum__dfg(u,x,z)* -> sum__dfg(z,y,w)*. % 1.40/1.58 12[0:Inp] defined(u) || -> sum__dfg(additive_identity,u,u)*. % 1.40/1.58 13[0:Inp] defined(u) || -> sum__dfg(additive_inverse(u),u,additive_identity)*. % 1.40/1.58 14[0:Inp] || sum__dfg(u,v,w)*+ -> sum__dfg(v,u,w)*. % 1.40/1.58 33[0:Inp] || less_or_equal(u,v)*+ sum__dfg(v,w,x)* sum__dfg(u,w,y)* -> less_or_equal(y,x)*. % 1.40/1.58 39[0:Res:7.0,11.0] || sum__dfg(b,u,v)*+ sum__dfg(c,w,u)* -> sum__dfg(v__dfg,w,v)*. % 1.40/1.58 51[0:Res:6.0,11.0] || sum__dfg(a,u,v)*+ sum__dfg(c,w,u)* -> sum__dfg(u__dfg,w,v)*. % 1.40/1.58 55[0:Res:6.0,10.1] || sum__dfg(u,c,v)*+ sum__dfg(w,a,u)* -> sum__dfg(w,u__dfg,v)*. % 1.40/1.58 65[0:Res:33.3,9.0] || less_or_equal(u,v)*+ sum__dfg(v,w,b)* sum__dfg(u,w,a)* -> . % 1.40/1.58 104[0:Res:12.1,14.0] defined(u) || -> sum__dfg(u,additive_identity,u)*. % 1.40/1.58 107[0:Res:13.1,14.0] defined(u) || -> sum__dfg(u,additive_inverse(u),additive_identity)*. % 1.40/1.58 153[0:Res:13.1,11.0] defined(u) || sum__dfg(v,w,u)* sum__dfg(additive_inverse(u),v,x)*+ -> sum__dfg(x,w,additive_identity)*. % 1.40/1.58 167[0:Res:104.1,51.0] defined(a) || sum__dfg(c,u,additive_identity)* -> sum__dfg(u__dfg,u,a). % 1.40/1.58 169[0:SSi:167.0,1.0] || sum__dfg(c,u,additive_identity)* -> sum__dfg(u__dfg,u,a). % 1.40/1.58 174[0:Res:107.1,169.0] defined(c) || -> sum__dfg(u__dfg,additive_inverse(c),a)*. % 1.40/1.58 176[0:SSi:174.0,3.0] || -> sum__dfg(u__dfg,additive_inverse(c),a)*. % 1.40/1.58 426[0:Res:104.1,39.0] defined(b) || sum__dfg(c,u,additive_identity)* -> sum__dfg(v__dfg,u,b). % 1.40/1.58 430[0:SSi:426.0,2.0] || sum__dfg(c,u,additive_identity)* -> sum__dfg(v__dfg,u,b). % 1.40/1.58 527[0:Res:12.1,55.0] defined(c) || sum__dfg(u,a,additive_identity)* -> sum__dfg(u,u__dfg,c). % 1.40/1.58 537[0:SSi:527.0,3.0] || sum__dfg(u,a,additive_identity)* -> sum__dfg(u,u__dfg,c). % 1.40/1.58 713[0:Res:13.1,537.0] defined(a) || -> sum__dfg(additive_inverse(a),u__dfg,c)*. % 1.40/1.58 715[0:SSi:713.0,1.0] || -> sum__dfg(additive_inverse(a),u__dfg,c)*. % 1.40/1.58 1291[0:Res:715.0,153.2] defined(a) || sum__dfg(u__dfg,u,a) -> sum__dfg(c,u,additive_identity)*. % 1.40/1.58 1295[0:SSi:1291.0,1.0] || sum__dfg(u__dfg,u,a) -> sum__dfg(c,u,additive_identity)*. % 1.40/1.58 1422[0:Res:8.0,65.0] || sum__dfg(v__dfg,u,b) sum__dfg(u__dfg,u,a)* -> . % 1.40/1.58 4618[0:Res:1295.1,430.0] || sum__dfg(u__dfg,u,a)* -> sum__dfg(v__dfg,u,b). % 1.40/1.58 4658[0:MRR:4618.1,1422.0] || sum__dfg(u__dfg,u,a)* -> . % 1.40/1.58 4659[0:UnC:4658.0,176.0] || -> . % 1.40/1.58 % SZS output end Refutation % 1.40/1.58 Formulae used in the proof : a_is_defined b_is_defined c_is_defined sum_6 sum_7 less_or_equal_8 not_less_or_equal_9 associativity_addition_1 associativity_addition_2 existence_of_identity_addition existence_of_inverse_addition commutativity_addition compatibility_of_order_relation_and_addition % 1.40/1.58 %------------------------------------------------------------------------------