%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV194+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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 : Wed Jul 20 21:41:35 EDT 2022 % Result : Theorem 1.09s 1.25s % Output : Refutation 1.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV194+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.12/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n009.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 15 16:55:38 EDT 2022 % 0.12/0.33 % CPUTime : % 1.09/1.25 % 1.09/1.25 SPASS V 3.9 % 1.09/1.25 SPASS beiseite: Proof found. % 1.09/1.25 % SZS status Theorem % 1.09/1.25 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.09/1.25 SPASS derived 3509 clauses, backtracked 509 clauses, performed 3 splits and kept 2240 clauses. % 1.09/1.25 SPASS allocated 88814 KBytes. % 1.09/1.25 SPASS spent 0:00:00.88 on the problem. % 1.09/1.25 0:00:00.04 for the input. % 1.09/1.25 0:00:00.08 for the FLOTTER CNF translation. % 1.09/1.25 0:00:00.02 for inferences. % 1.09/1.25 0:00:00.01 for the backtracking. % 1.09/1.25 0:00:00.63 for the reduction. % 1.09/1.25 % 1.09/1.25 % 1.09/1.25 Here is a proof with depth 3, length 60 : % 1.09/1.25 % SZS output start Refutation % 1.09/1.25 2[0:Inp] || -> leq(n0,skc3)*r. % 1.09/1.25 3[0:Inp] || -> leq(skc3,n2)*l. % 1.09/1.25 4[0:Inp] || -> leq(n0,pv5)*r. % 1.09/1.25 5[0:Inp] || -> leq(pv5,n0)*l. % 1.09/1.25 7[0:Inp] || -> gt(pv5,n0)*l. % 1.09/1.25 8[0:Inp] || -> leq(skc2,pv5)*l. % 1.09/1.25 9[0:Inp] || -> leq(n0,skc2)*r. % 1.09/1.25 39[0:Inp] || -> equal(succ(n0),n1)**. % 1.09/1.25 40[0:Inp] || gt(u,u)* -> . % 1.09/1.25 68[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 1.09/1.25 85[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.09/1.25 93[0:Inp] || -> equal(plus(u,n1),succ(u))**. % 1.09/1.25 97[0:Inp] || equal(a_select3(u_defuse,skc3,skc2),use)** -> . % 1.09/1.25 104[0:Inp] || -> equal(succ(succ(u)),plus(u,n2))**. % 1.09/1.25 105[0:Inp] || -> equal(succ(succ(u)),plus(n2,u))**. % 1.09/1.25 110[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.09/1.25 132[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.09/1.25 136[0:Inp] || leq(u,n0)* leq(n0,u)* -> equal(u,n0). % 1.09/1.25 138[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 1.09/1.25 142[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.09/1.25 153[0:Inp] || leq(u,n2) leq(v,pred(pv5)) leq(n0,v) leq(n0,u) -> equal(a_select3(u_defuse,u,v),use)**. % 1.09/1.25 179[0:Rew:39.0,68.0] || -> equal(succ(n1),n2)**. % 1.09/1.25 183[0:Rew:105.0,104.0] || -> equal(plus(n2,u),plus(u,n2))*. % 1.09/1.25 192[0:Res:153.4,97.0] || leq(n0,skc3) leq(skc3,n2) leq(skc2,pred(pv5))*r leq(n0,skc2) -> . % 1.09/1.25 221[0:Res:9.0,142.0] || leq(skc2,n1)*l -> equal(skc2,n1) equal(skc2,n0). % 1.09/1.25 222[0:Res:9.0,136.0] || leq(skc2,n0)*l -> equal(skc2,n0). % 1.09/1.25 334[0:Res:8.0,132.0] || -> gt(pv5,skc2)*r equal(skc2,pv5). % 1.09/1.25 381[0:MRR:192.0,192.1,192.3,2.0,3.0,9.0] || leq(skc2,pred(pv5))*r -> . % 1.09/1.25 436[1:Spt:221.1] || -> equal(skc2,n1)**. % 1.09/1.25 448[1:Rew:436.0,222.1] || leq(skc2,n0)*l -> equal(n1,n0). % 1.09/1.25 532[1:Rew:436.0,8.0] || -> leq(n1,pv5)*r. % 1.09/1.25 535[1:Rew:436.0,381.0] || leq(n1,pred(pv5))*r -> . % 1.09/1.25 566[1:Rew:436.0,448.0] || leq(n1,n0)*l -> equal(n1,n0). % 1.09/1.25 723[0:SpR:105.0,85.0] || -> equal(pred(plus(n2,u)),succ(u))**. % 1.09/1.25 747[0:SpR:183.0,723.0] || -> equal(pred(plus(u,n2)),succ(u))**. % 1.09/1.25 794[1:OCh:138.1,138.0,532.0,5.0] || -> leq(n1,n0)*l. % 1.09/1.25 795[1:MRR:566.0,794.0] || -> equal(n1,n0)**. % 1.09/1.25 799[1:Rew:795.0,39.0] || -> equal(succ(n0),n0)**. % 1.09/1.25 800[1:Rew:795.0,179.0] || -> equal(succ(n0),n2)**. % 1.09/1.25 810[1:Rew:795.0,93.0] || -> equal(plus(u,n0),succ(u))**. % 1.09/1.25 858[1:Rew:795.0,535.0] || leq(n0,pred(pv5))*r -> . % 1.09/1.25 941[1:Rew:799.0,800.0] || -> equal(n2,n0)**. % 1.09/1.25 949[1:Rew:941.0,747.0] || -> equal(pred(plus(u,n0)),succ(u))**. % 1.09/1.25 1023[1:Rew:810.0,949.0] || -> equal(pred(succ(u)),succ(u))**. % 1.09/1.25 1024[1:Rew:85.0,1023.0] || -> equal(succ(u),u)**. % 1.09/1.25 1025[1:Rew:1024.0,85.0] || -> equal(pred(u),u)**. % 1.09/1.25 1092[1:Rew:1025.0,858.0] || leq(n0,pv5)*r -> . % 1.09/1.25 1093[1:MRR:1092.0,4.0] || -> . % 1.09/1.25 1177[1:Spt:1093.0,221.1,436.0] || equal(skc2,n1)** -> . % 1.09/1.25 1178[1:Spt:1093.0,221.0,221.2] || leq(skc2,n1)*l -> equal(skc2,n0). % 1.09/1.25 1183[2:Spt:334.1] || -> equal(skc2,pv5)**. % 1.09/1.25 1210[2:Rew:1183.0,222.1] || leq(skc2,n0)*l -> equal(pv5,n0). % 1.09/1.25 1313[2:Rew:1183.0,1210.0] || leq(pv5,n0)*l -> equal(pv5,n0). % 1.09/1.25 1314[2:MRR:1313.0,5.0] || -> equal(pv5,n0)**. % 1.09/1.25 1315[2:Rew:1314.0,7.0] || -> gt(n0,n0)*. % 1.09/1.25 1333[2:MRR:1315.0,40.0] || -> . % 1.09/1.25 1446[2:Spt:1333.0,334.1,1183.0] || equal(skc2,pv5)** -> . % 1.09/1.25 1447[2:Spt:1333.0,334.0] || -> gt(pv5,skc2)*r. % 1.09/1.25 5298[2:Res:1447.0,110.0] || -> leq(skc2,pred(pv5))*r. % 1.09/1.25 5307[2:MRR:5298.0,381.0] || -> . % 1.09/1.25 % SZS output end Refutation % 1.09/1.25 Formulae used in the proof : quaternion_ds1_inuse_0005 successor_1 irreflexivity_gt successor_2 pred_succ succ_plus_1_r succ_plus_2_r succ_plus_2_l leq_gt_pred leq_gt2 finite_domain_0 transitivity_leq finite_domain_1 % 1.09/1.25 %------------------------------------------------------------------------------