%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD036-3 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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:25 EDT 2022 % Result : Unsatisfiable 86.91s 87.10s % Output : Refutation 89.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : FLD036-3 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon Jun 6 18:15:07 EDT 2022 % 0.14/0.35 % CPUTime : % 86.91/87.10 % 86.91/87.10 SPASS V 3.9 % 86.91/87.10 SPASS beiseite: Proof found. % 86.91/87.10 % SZS status Theorem % 86.91/87.10 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 86.91/87.10 SPASS derived 29919 clauses, backtracked 783 clauses, performed 25 splits and kept 22144 clauses. % 86.91/87.10 SPASS allocated 105961 KBytes. % 86.91/87.10 SPASS spent 0:1:26.69 on the problem. % 86.91/87.10 0:00:00.02 for the input. % 86.91/87.10 0:00:00.00 for the FLOTTER CNF translation. % 86.91/87.10 0:00:00.28 for inferences. % 86.91/87.10 0:00:04.18 for the backtracking. % 86.91/87.10 0:1:21.77 for the reduction. % 86.91/87.10 % 86.91/87.10 % 86.91/87.10 Here is a proof with depth 12, length 96 : % 86.91/87.10 % SZS output start Refutation % 86.91/87.10 1[0:Inp] || -> defined(a)*. % 86.91/87.10 2[0:Inp] || -> defined(b)*. % 86.91/87.10 3[0:Inp] || -> defined(c)*. % 86.91/87.10 5[0:Inp] || -> product(a,c,u__dfg)*. % 86.91/87.10 6[0:Inp] || -> product(b,c,u__dfg)*. % 86.91/87.10 7[0:Inp] || product(multiplicative_identity,a,b)* -> . % 86.91/87.10 8[0:Inp] || sum__dfg(additive_identity,c,additive_identity)* -> . % 86.91/87.10 9[0:Inp] || sum__dfg(u,v,w)*+ sum__dfg(x,v,y)* sum__dfg(z,x,u)* -> sum__dfg(z,y,w)*. % 86.91/87.10 11[0:Inp] defined(u) || -> sum__dfg(additive_identity,u,u)*. % 86.91/87.10 13[0:Inp] || sum__dfg(u,v,w)*+ -> sum__dfg(v,u,w)*. % 86.91/87.10 14[0:Inp] || product(u,v,w)*+ product(x,v,y)* product(z,x,u)* -> product(z,y,w)*. % 86.91/87.10 15[0:Inp] || product(u,v,w)*+ product(x,y,v)* product(u,x,z)* -> product(z,y,w)*. % 86.91/87.10 16[0:Inp] defined(u) || -> product(multiplicative_identity,u,u)*. % 86.91/87.10 17[0:Inp] defined(u) || -> sum__dfg(additive_identity,u,additive_identity) product(multiplicative_inverse(u),u,multiplicative_identity)*. % 86.91/87.10 18[0:Inp] || product(u,v,w)*+ -> product(v,u,w)*. % 86.91/87.10 20[0:Inp] || sum__dfg(u,v,w)*+ product(x,y,v)* product(z,y,u)* sum__dfg(z,x,x1)* -> product(x1,y,w)*. % 86.91/87.10 22[0:Inp] || -> defined(additive_identity)*. % 86.91/87.10 37[0:Res:6.0,15.0] || product(b,u,v)*+ product(c,w,u)* -> product(u__dfg,w,v)*. % 86.91/87.10 40[0:Res:6.0,14.1] || product(u,c,v)*+ product(w,b,u)* -> product(w,u__dfg,v)*. % 86.91/87.10 50[0:Res:5.0,15.0] || product(a,u,v)*+ product(c,w,u)* -> product(u__dfg,w,v)*. % 86.91/87.10 53[0:Res:5.0,14.1] || product(u,c,v)*+ product(w,a,u)* -> product(w,u__dfg,v)*. % 86.91/87.10 61[0:Res:17.2,8.0] defined(c) || -> product(multiplicative_inverse(c),c,multiplicative_identity)*. % 86.91/87.10 69[0:MRR:61.0,3.0] || -> product(multiplicative_inverse(c),c,multiplicative_identity)*. % 86.91/87.10 89[0:Res:69.0,18.0] || -> product(c,multiplicative_inverse(c),multiplicative_identity)*. % 86.91/87.10 90[0:Res:16.1,18.0] defined(u) || -> product(u,multiplicative_identity,u)*. % 86.91/87.10 113[0:Res:90.1,50.0] defined(a) || product(c,u,multiplicative_identity)* -> product(u__dfg,u,a). % 86.91/87.10 116[0:SSi:113.0,1.0] || product(c,u,multiplicative_identity)* -> product(u__dfg,u,a). % 86.91/87.10 122[0:Res:11.1,9.0] defined(u) || sum__dfg(v,u,w)*+ sum__dfg(x,v,additive_identity)* -> sum__dfg(x,w,u)*. % 86.91/87.10 132[0:Res:89.0,116.0] || -> product(u__dfg,multiplicative_inverse(c),a)*. % 86.91/87.10 134[0:Res:132.0,18.0] || -> product(multiplicative_inverse(c),u__dfg,a)*. % 86.91/87.10 142[0:Res:17.2,15.0] defined(u) || product(v,w,u)* product(multiplicative_inverse(u),v,x)*+ -> sum__dfg(additive_identity,u,additive_identity) product(x,w,multiplicative_identity)*. % 86.91/87.10 145[0:Res:16.1,15.0] defined(u) || product(v,w,u)*+ product(multiplicative_identity,v,x)* -> product(x,w,u)*. % 86.91/87.10 166[0:Res:16.1,14.0] defined(u) || product(v,u,w)*+ product(x,v,multiplicative_identity)* -> product(x,w,u)*. % 86.91/87.10 303[0:Res:11.1,20.0] defined(u) || product(v,w,u)*+ product(x,w,additive_identity)* sum__dfg(x,v,y)* -> product(y,w,u)*. % 86.91/87.10 389[0:Res:90.1,37.0] defined(b) || product(c,u,multiplicative_identity)* -> product(u__dfg,u,b). % 86.91/87.10 396[0:SSi:389.0,2.0] || product(c,u,multiplicative_identity)* -> product(u__dfg,u,b). % 86.91/87.10 415[0:Res:89.0,396.0] || -> product(u__dfg,multiplicative_inverse(c),b)*. % 86.91/87.10 420[0:Res:415.0,18.0] || -> product(multiplicative_inverse(c),u__dfg,b)*. % 86.91/87.10 478[0:Res:16.1,53.0] defined(c) || product(u,a,multiplicative_identity)* -> product(u,u__dfg,c). % 86.91/87.10 487[0:SSi:478.0,3.0] || product(u,a,multiplicative_identity)* -> product(u,u__dfg,c). % 86.91/87.10 554[0:Res:16.1,40.0] defined(c) || product(u,b,multiplicative_identity)* -> product(u,u__dfg,c). % 86.91/87.10 563[0:SSi:554.0,3.0] || product(u,b,multiplicative_identity)* -> product(u,u__dfg,c). % 86.91/87.10 598[0:Res:17.2,487.0] defined(a) || -> sum__dfg(additive_identity,a,additive_identity) product(multiplicative_inverse(a),u__dfg,c)*. % 86.91/87.10 599[0:SSi:598.0,1.0] || -> sum__dfg(additive_identity,a,additive_identity) product(multiplicative_inverse(a),u__dfg,c)*. % 86.91/87.10 603[0:Res:599.1,18.0] || -> sum__dfg(additive_identity,a,additive_identity) product(u__dfg,multiplicative_inverse(a),c)*. % 86.91/87.10 608[1:Spt:603.0] || -> sum__dfg(additive_identity,a,additive_identity)*. % 86.91/87.10 661[0:Res:17.2,563.0] defined(b) || -> sum__dfg(additive_identity,b,additive_identity) product(multiplicative_inverse(b),u__dfg,c)*. % 86.91/87.10 662[0:SSi:661.0,2.0] || -> sum__dfg(additive_identity,b,additive_identity) product(multiplicative_inverse(b),u__dfg,c)*. % 86.91/87.10 672[0:Res:662.1,18.0] || -> sum__dfg(additive_identity,b,additive_identity) product(u__dfg,multiplicative_inverse(b),c)*. % 86.91/87.10 678[2:Spt:672.0] || -> sum__dfg(additive_identity,b,additive_identity)*. % 86.91/87.10 682[2:Res:678.0,13.0] || -> sum__dfg(b,additive_identity,additive_identity)*. % 86.91/87.10 809[1:Res:608.0,122.1] defined(a) || sum__dfg(u,additive_identity,additive_identity) -> sum__dfg(u,additive_identity,a)*. % 86.91/87.10 816[1:SSi:809.0,1.0] || sum__dfg(u,additive_identity,additive_identity) -> sum__dfg(u,additive_identity,a)*. % 86.91/87.10 901[0:Res:90.1,145.1] defined(u) defined(u) || product(multiplicative_identity,u,v)* -> product(v,multiplicative_identity,u)*. % 86.91/87.10 965[0:Obv:901.0] defined(u) || product(multiplicative_identity,u,v)*+ -> product(v,multiplicative_identity,u)*. % 86.91/87.10 1059[0:Res:17.2,166.1] defined(u) defined(u) || product(v,multiplicative_inverse(u),multiplicative_identity)* -> sum__dfg(additive_identity,u,additive_identity) product(v,multiplicative_identity,u). % 86.91/87.10 1135[0:Obv:1059.0] defined(u) || product(v,multiplicative_inverse(u),multiplicative_identity)* -> sum__dfg(additive_identity,u,additive_identity) product(v,multiplicative_identity,u). % 86.91/87.10 1422[1:Res:816.1,13.0] || sum__dfg(u,additive_identity,additive_identity)*+ -> sum__dfg(additive_identity,u,a)*. % 86.91/87.10 1831[2:Res:682.0,1422.0] || -> sum__dfg(additive_identity,b,a)*. % 86.91/87.10 2307[0:Res:134.0,142.2] defined(c) || product(u__dfg,u,c) -> sum__dfg(additive_identity,c,additive_identity)* product(a,u,multiplicative_identity)*. % 86.91/87.10 2309[0:Res:420.0,142.2] defined(c) || product(u__dfg,u,c) -> sum__dfg(additive_identity,c,additive_identity)* product(b,u,multiplicative_identity)*. % 86.91/87.10 2312[0:SSi:2307.0,3.0] || product(u__dfg,u,c) -> sum__dfg(additive_identity,c,additive_identity)* product(a,u,multiplicative_identity)*. % 86.91/87.10 2313[0:MRR:2312.1,8.0] || product(u__dfg,u,c) -> product(a,u,multiplicative_identity)*. % 86.91/87.10 2314[0:SSi:2309.0,3.0] || product(u__dfg,u,c) -> sum__dfg(additive_identity,c,additive_identity)* product(b,u,multiplicative_identity)*. % 86.91/87.10 2315[0:MRR:2314.1,8.0] || product(u__dfg,u,c) -> product(b,u,multiplicative_identity)*. % 86.91/87.10 3505[0:Res:90.1,303.1] defined(u) defined(u) || product(v,multiplicative_identity,additive_identity) sum__dfg(v,u,w)* -> product(w,multiplicative_identity,u). % 86.91/87.10 3569[0:Obv:3505.0] defined(u) || product(v,multiplicative_identity,additive_identity) sum__dfg(v,u,w)* -> product(w,multiplicative_identity,u). % 86.91/87.10 4889[0:Res:2313.1,18.0] || product(u__dfg,u,c)*+ -> product(u,a,multiplicative_identity)*. % 86.91/87.10 5627[0:Res:2315.1,18.0] || product(u__dfg,u,c)*+ -> product(u,b,multiplicative_identity)*. % 86.91/87.10 17670[2:Res:1831.0,3569.2] defined(b) || product(additive_identity,multiplicative_identity,additive_identity) -> product(a,multiplicative_identity,b)*. % 86.91/87.10 18059[2:SSi:17670.0,2.0] || product(additive_identity,multiplicative_identity,additive_identity) -> product(a,multiplicative_identity,b)*. % 86.91/87.10 18894[2:Res:18059.1,18.0] || product(additive_identity,multiplicative_identity,additive_identity) -> product(multiplicative_identity,a,b)*. % 86.91/87.10 18906[2:MRR:18894.1,7.0] || product(additive_identity,multiplicative_identity,additive_identity)* -> . % 86.91/87.10 18969[2:Res:90.1,18906.0] defined(additive_identity) || -> . % 86.91/87.10 18970[2:SSi:18969.0,22.0] || -> . % 86.91/87.10 18971[2:Spt:18970.0,672.0,678.0] || sum__dfg(additive_identity,b,additive_identity)* -> . % 86.91/87.10 18972[2:Spt:18970.0,672.1] || -> product(u__dfg,multiplicative_inverse(b),c)*. % 86.91/87.10 29664[2:Res:18972.0,4889.0] || -> product(multiplicative_inverse(b),a,multiplicative_identity)*. % 86.91/87.10 29827[2:Res:29664.0,18.0] || -> product(a,multiplicative_inverse(b),multiplicative_identity)*. % 86.91/87.10 29854[2:Res:29827.0,1135.1] defined(b) || -> sum__dfg(additive_identity,b,additive_identity)* product(a,multiplicative_identity,b). % 89.93/90.12 29872[2:SSi:29854.0,2.0] || -> sum__dfg(additive_identity,b,additive_identity)* product(a,multiplicative_identity,b). % 89.93/90.12 29873[2:MRR:29872.0,18971.0] || -> product(a,multiplicative_identity,b)*. % 89.93/90.12 29890[2:Res:29873.0,18.0] || -> product(multiplicative_identity,a,b)*. % 89.93/90.12 29904[2:MRR:29890.0,7.0] || -> . % 89.93/90.12 29914[1:Spt:29904.0,603.0,608.0] || sum__dfg(additive_identity,a,additive_identity)* -> . % 89.93/90.12 29915[1:Spt:29904.0,603.1] || -> product(u__dfg,multiplicative_inverse(a),c)*. % 89.93/90.12 42361[1:Res:29915.0,5627.0] || -> product(multiplicative_inverse(a),b,multiplicative_identity)*. % 89.93/90.12 42373[1:Res:42361.0,18.0] || -> product(b,multiplicative_inverse(a),multiplicative_identity)*. % 89.93/90.12 42411[1:Res:42373.0,1135.1] defined(a) || -> sum__dfg(additive_identity,a,additive_identity)* product(b,multiplicative_identity,a). % 89.93/90.12 42435[1:SSi:42411.0,1.0] || -> sum__dfg(additive_identity,a,additive_identity)* product(b,multiplicative_identity,a). % 89.93/90.12 42436[1:MRR:42435.0,29914.0] || -> product(b,multiplicative_identity,a)*. % 89.93/90.12 43024[1:Res:42436.0,18.0] || -> product(multiplicative_identity,b,a)*. % 89.93/90.12 43076[1:Res:43024.0,965.1] defined(b) || -> product(a,multiplicative_identity,b)*. % 89.93/90.12 43094[1:SSi:43076.0,2.0] || -> product(a,multiplicative_identity,b)*. % 89.93/90.12 43117[1:Res:43094.0,18.0] || -> product(multiplicative_identity,a,b)*. % 89.93/90.12 43140[1:MRR:43117.0,7.0] || -> . % 89.93/90.12 % SZS output end Refutation % 89.93/90.12 Formulae used in the proof : a_is_defined b_is_defined c_is_defined product_5 product_6 not_product_7 not_sum_8 associativity_addition_1 existence_of_identity_addition commutativity_addition associativity_multiplication_1 associativity_multiplication_2 existence_of_identity_multiplication existence_of_inverse_multiplication commutativity_multiplication distributivity_2 well_definedness_of_additive_identity % 89.93/90.12 %------------------------------------------------------------------------------