%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG002-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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 14 18:01:55 EDT 2022 % Result : Unsatisfiable 52.62s 52.78s % Output : Refutation 53.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG002-1 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.12/0.33 % Computer : n022.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 : Wed Jun 8 11:19:35 EDT 2022 % 0.12/0.34 % CPUTime : % 52.62/52.78 % 52.62/52.78 SPASS V 3.9 % 52.62/52.78 SPASS beiseite: Proof found. % 52.62/52.78 % SZS status Theorem % 52.62/52.78 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.62/52.78 SPASS derived 28048 clauses, backtracked 4500 clauses, performed 8 splits and kept 13065 clauses. % 52.62/52.78 SPASS allocated 94904 KBytes. % 52.62/52.78 SPASS spent 0:0:52.42 on the problem. % 52.62/52.78 0:00:00.04 for the input. % 52.62/52.78 0:00:00.00 for the FLOTTER CNF translation. % 52.62/52.78 0:00:00.32 for inferences. % 52.62/52.78 0:00:01.33 for the backtracking. % 52.62/52.78 0:0:50.52 for the reduction. % 52.62/52.78 % 52.62/52.78 % 52.62/52.78 Here is a proof with depth 6, length 85 : % 52.62/52.78 % SZS output start Refutation % 52.62/52.78 1[0:Inp] || -> product(u,multiplicative_identity,u)*. % 52.62/52.78 2[0:Inp] || product(multiplicative_identity,multiplicative_identity,additive_identity)* -> . % 52.62/52.78 3[0:Inp] || product(u,v,w) -> product(additive_inverse(u),additive_inverse(v),w)*. % 52.62/52.78 4[0:Inp] || product(additive_inverse(u),additive_inverse(v),w)* -> product(u,v,w). % 52.62/52.78 5[0:Inp] || product(u,v,w) -> product(u,additive_inverse(v),additive_inverse(w))*. % 52.62/52.78 6[0:Inp] || -> product(u,u,additive_identity) product(u,multiplicative_inverse(u),multiplicative_identity)*. % 52.62/52.78 7[0:Inp] greater_than_0(u) || greater_than_0(additive_inverse(u))* -> . % 52.62/52.78 8[0:Inp] greater_than_0(u) || product(u,u,additive_identity)* -> . % 52.62/52.78 9[0:Inp] || product(u,v,w)*+ -> product(v,u,w)*. % 52.62/52.78 10[0:Inp] || -> greater_than_0(u) greater_than_0(additive_inverse(u)) product(u,u,additive_identity)*. % 52.62/52.78 11[0:Inp] || product(u,v,w)*+ product(u,u,additive_identity)* -> product(w,w,additive_identity)*. % 52.62/52.78 12[0:Inp] greater_than_0(u) greater_than_0(v) || product(v,u,w)* -> greater_than_0(w). % 52.62/52.78 13[0:Inp] || -> greater_than_0(a)*. % 52.62/52.78 14[0:Inp] || greater_than_0(multiplicative_inverse(a))* -> . % 52.62/52.78 16[0:Res:12.3,14.0] greater_than_0(u) greater_than_0(v) || product(v,u,multiplicative_inverse(a))* -> . % 52.62/52.78 21[0:Res:10.2,2.0] || -> greater_than_0(multiplicative_identity) greater_than_0(additive_inverse(multiplicative_identity))*. % 52.62/52.78 24[0:Res:1.0,9.0] || -> product(multiplicative_identity,u,u)*. % 52.62/52.78 26[0:Res:6.1,9.0] || -> product(u,u,additive_identity) product(multiplicative_inverse(u),u,multiplicative_identity)*. % 52.62/52.78 29[0:Res:3.1,8.1] greater_than_0(additive_inverse(u)) || product(u,u,additive_identity)* -> . % 52.62/52.79 33[0:Res:10.2,4.0] || -> greater_than_0(additive_inverse(u)) greater_than_0(additive_inverse(additive_inverse(u)))* product(u,u,additive_identity)*. % 52.62/52.79 38[0:Res:33.2,8.1] greater_than_0(u) || -> greater_than_0(additive_inverse(u)) greater_than_0(additive_inverse(additive_inverse(u)))*. % 52.62/52.79 41[0:MRR:38.1,7.1] greater_than_0(u) || -> greater_than_0(additive_inverse(additive_inverse(u)))*. % 52.62/52.79 43[0:Res:41.1,7.1] greater_than_0(u) greater_than_0(additive_inverse(u)) || -> . % 52.62/52.79 50[0:Res:6.1,12.2] greater_than_0(multiplicative_inverse(u)) greater_than_0(u) || -> product(u,u,additive_identity)* greater_than_0(multiplicative_identity). % 52.62/52.79 51[0:Res:5.1,12.2] greater_than_0(additive_inverse(u)) greater_than_0(v) || product(v,u,w)* -> greater_than_0(additive_inverse(w)). % 52.62/52.79 55[0:MRR:50.2,8.1] greater_than_0(multiplicative_inverse(u)) greater_than_0(u) || -> greater_than_0(multiplicative_identity)*. % 52.62/52.79 70[0:Res:10.2,11.0] || product(u,u,additive_identity)* -> greater_than_0(u) greater_than_0(additive_inverse(u)) product(additive_identity,additive_identity,additive_identity)*. % 52.62/52.79 72[0:Res:5.1,11.0] || product(u,v,w)*+ product(u,u,additive_identity)* -> product(additive_inverse(w),additive_inverse(w),additive_identity)*. % 52.62/52.79 74[0:Res:26.1,11.0] || product(multiplicative_inverse(u),multiplicative_inverse(u),additive_identity)* -> product(u,u,additive_identity) product(multiplicative_identity,multiplicative_identity,additive_identity). % 52.62/52.79 76[0:Res:3.1,11.0] || product(u,v,w)* product(additive_inverse(u),additive_inverse(u),additive_identity)*+ -> product(w,w,additive_identity)*. % 52.62/52.79 78[0:MRR:70.0,10.2] || -> greater_than_0(u) greater_than_0(additive_inverse(u))* product(additive_identity,additive_identity,additive_identity)*. % 52.62/52.79 79[0:MRR:74.2,2.0] || product(multiplicative_inverse(u),multiplicative_inverse(u),additive_identity)* -> product(u,u,additive_identity). % 52.62/52.79 80[1:Spt:78.0,78.1] || -> greater_than_0(u) greater_than_0(additive_inverse(u))*. % 52.62/52.79 82[1:SoR:29.0,80.1] || product(u,u,additive_identity)* -> greater_than_0(u). % 52.62/52.79 84[1:MRR:82.1,8.0] || product(u,u,additive_identity)* -> . % 52.62/52.79 85[1:MRR:6.0,84.0] || -> product(u,multiplicative_inverse(u),multiplicative_identity)*. % 52.62/52.79 111[0:Res:3.1,16.2] greater_than_0(additive_inverse(u)) greater_than_0(additive_inverse(v)) || product(v,u,multiplicative_inverse(a))* -> . % 52.62/52.79 122[1:SoR:51.0,80.1] greater_than_0(u) || product(u,v,w)* -> greater_than_0(additive_inverse(w)) greater_than_0(v). % 52.62/52.79 217[1:SoR:111.0,80.1] greater_than_0(additive_inverse(u)) || product(u,v,multiplicative_inverse(a))* -> greater_than_0(v). % 52.62/52.79 219[1:SoR:217.0,80.1] || product(u,v,multiplicative_inverse(a))* -> greater_than_0(v) greater_than_0(u). % 52.62/52.79 220[1:Res:1.0,219.0] || -> greater_than_0(multiplicative_identity) greater_than_0(multiplicative_inverse(a))*. % 52.62/52.79 224[1:MRR:220.1,14.0] || -> greater_than_0(multiplicative_identity)*. % 52.62/52.79 240[1:Res:85.0,122.1] greater_than_0(u) || -> greater_than_0(additive_inverse(multiplicative_identity))* greater_than_0(multiplicative_inverse(u))*. % 52.62/52.79 280[2:Spt:240.0,240.2] greater_than_0(u) || -> greater_than_0(multiplicative_inverse(u))*. % 52.62/52.79 284[2:Res:280.1,14.0] greater_than_0(a) || -> . % 52.62/52.79 286[2:SSi:284.0,13.0] || -> . % 52.62/52.79 288[2:Spt:286.0,240.1] || -> greater_than_0(additive_inverse(multiplicative_identity))*. % 52.62/52.79 296[2:Res:288.0,7.1] greater_than_0(multiplicative_identity) || -> . % 52.62/52.79 298[2:SSi:296.0,224.0] || -> . % 52.62/52.79 299[1:Spt:298.0,78.2] || -> product(additive_identity,additive_identity,additive_identity)*. % 52.62/52.79 302[2:Spt:21.0] || -> greater_than_0(multiplicative_identity)*. % 52.62/52.79 398[0:Res:10.2,79.0] || -> greater_than_0(multiplicative_inverse(u)) greater_than_0(additive_inverse(multiplicative_inverse(u)))* product(u,u,additive_identity)*. % 52.62/52.79 402[0:SoR:51.0,398.1] greater_than_0(u) || product(u,multiplicative_inverse(v),w)*+ -> greater_than_0(additive_inverse(w)) product(v,v,additive_identity)* greater_than_0(multiplicative_inverse(v)). % 52.62/52.79 415[0:Res:398.2,8.1] greater_than_0(u) || -> greater_than_0(multiplicative_inverse(u)) greater_than_0(additive_inverse(multiplicative_inverse(u)))*. % 52.62/52.79 455[0:Res:10.2,72.0] || product(u,u,additive_identity)* -> greater_than_0(u) greater_than_0(additive_inverse(u)) product(additive_inverse(additive_identity),additive_inverse(additive_identity),additive_identity)*. % 52.62/52.79 456[0:MRR:455.0,10.2] || -> greater_than_0(u) greater_than_0(additive_inverse(u))* product(additive_inverse(additive_identity),additive_inverse(additive_identity),additive_identity)*. % 52.62/52.79 457[3:Spt:456.0,456.1] || -> greater_than_0(u) greater_than_0(additive_inverse(u))*. % 52.62/52.79 458[3:SoR:29.0,457.1] || product(u,u,additive_identity)* -> greater_than_0(u). % 52.62/52.79 468[3:MRR:458.1,8.0] || product(u,u,additive_identity)* -> . % 52.62/52.79 469[3:UnC:468.0,299.0] || -> . % 52.62/52.79 470[3:Spt:469.0,456.2] || -> product(additive_inverse(additive_identity),additive_inverse(additive_identity),additive_identity)*. % 52.62/52.79 572[0:Res:10.2,76.1] || product(u,v,w)*+ -> greater_than_0(additive_inverse(u)) greater_than_0(additive_inverse(additive_inverse(u)))* product(w,w,additive_identity)*. % 52.62/52.79 734[0:Res:24.0,572.0] || -> greater_than_0(additive_inverse(multiplicative_identity)) greater_than_0(additive_inverse(additive_inverse(multiplicative_identity)))* product(u,u,additive_identity)*. % 52.62/52.79 1110[4:Spt:734.2] || -> product(u,u,additive_identity)*. % 52.62/52.79 1111[4:UnC:1110.0,2.0] || -> . % 52.62/52.79 1112[4:Spt:1111.0,734.0,734.1] || -> greater_than_0(additive_inverse(multiplicative_identity)) greater_than_0(additive_inverse(additive_inverse(multiplicative_identity)))*. % 52.62/52.79 1113[5:Spt:1112.0] || -> greater_than_0(additive_inverse(multiplicative_identity))*. % 52.62/52.79 1122[5:Res:1113.0,7.1] greater_than_0(multiplicative_identity) || -> . % 52.62/52.79 1124[5:SSi:1122.0,302.0] || -> . % 52.62/52.79 1125[5:Spt:1124.0,1112.0,1113.0] || greater_than_0(additive_inverse(multiplicative_identity))* -> . % 52.62/52.79 1126[5:Spt:1124.0,1112.1] || -> greater_than_0(additive_inverse(additive_inverse(multiplicative_identity)))*. % 52.62/52.79 1133[5:SoR:43.1,1126.0] greater_than_0(additive_inverse(multiplicative_identity)) || -> . % 52.62/52.79 27659[0:Res:6.1,402.1] greater_than_0(u) || -> product(u,u,additive_identity)* greater_than_0(additive_inverse(multiplicative_identity)) product(u,u,additive_identity)* greater_than_0(multiplicative_inverse(u)). % 53.66/53.89 27719[0:Obv:27659.1] greater_than_0(u) || -> greater_than_0(additive_inverse(multiplicative_identity)) product(u,u,additive_identity)* greater_than_0(multiplicative_inverse(u)). % 53.66/53.89 27720[5:MRR:27719.1,27719.2,1133.0,8.1] greater_than_0(u) || -> greater_than_0(multiplicative_inverse(u))*. % 53.66/53.89 27742[5:Res:27720.1,14.0] greater_than_0(a) || -> . % 53.66/53.89 27744[5:SSi:27742.0,13.0] || -> . % 53.66/53.89 27745[2:Spt:27744.0,21.0,302.0] || greater_than_0(multiplicative_identity)* -> . % 53.66/53.89 27746[2:Spt:27744.0,21.1] || -> greater_than_0(additive_inverse(multiplicative_identity))*. % 53.66/53.89 27747[2:MRR:55.2,27745.0] greater_than_0(multiplicative_inverse(u)) greater_than_0(u) || -> . % 53.66/53.89 27748[2:MRR:415.1,27747.0] greater_than_0(u) || -> greater_than_0(additive_inverse(multiplicative_inverse(u)))*. % 53.66/53.89 27839[2:SoR:111.0,27746.0] greater_than_0(additive_inverse(u)) || product(u,multiplicative_identity,multiplicative_inverse(a))* -> . % 53.66/53.89 29767[2:SoR:27839.0,27748.1] greater_than_0(u) || product(multiplicative_inverse(u),multiplicative_identity,multiplicative_inverse(a))* -> . % 53.66/53.89 29803[2:Res:1.0,29767.1] greater_than_0(a) || -> . % 53.66/53.89 29804[2:SSi:29803.0,13.0] || -> . % 53.66/53.89 % SZS output end Refutation % 53.66/53.89 Formulae used in the proof : right_identity not_abelian product_of_inverses1 product_of_inverses2 product_to_inverse inverse_and_identity inverse_greater_than_0 greater_than_0_square commutativity_of_product product_and_inverse square_to_0 product_and_greater_than_0 a_greater_than_0 prove_a_inverse_greater_than_0 % 53.66/53.89 %------------------------------------------------------------------------------