%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV199+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:36 EDT 2022 % Result : Theorem 1.59s 1.80s % Output : Refutation 1.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV199+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.03/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n027.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Wed Jun 15 16:30:49 EDT 2022 % 0.14/0.36 % CPUTime : % 1.59/1.80 % 1.59/1.80 SPASS V 3.9 % 1.59/1.80 SPASS beiseite: Proof found. % 1.59/1.80 % SZS status Theorem % 1.59/1.80 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.59/1.80 SPASS derived 4751 clauses, backtracked 599 clauses, performed 5 splits and kept 2967 clauses. % 1.59/1.80 SPASS allocated 89629 KBytes. % 1.59/1.80 SPASS spent 0:00:01.40 on the problem. % 1.59/1.80 0:00:00.04 for the input. % 1.59/1.80 0:00:00.08 for the FLOTTER CNF translation. % 1.59/1.80 0:00:00.03 for inferences. % 1.59/1.80 0:00:00.02 for the backtracking. % 1.59/1.80 0:00:01.11 for the reduction. % 1.59/1.80 % 1.59/1.80 % 1.59/1.80 Here is a proof with depth 5, length 92 : % 1.59/1.80 % SZS output start Refutation % 1.59/1.80 2[0:Inp] || -> leq(n0,skc3)*r. % 1.59/1.80 3[0:Inp] || -> leq(skc3,n2)*l. % 1.59/1.80 4[0:Inp] || -> leq(n0,pv5)*r. % 1.59/1.80 5[0:Inp] || -> leq(pv5,n0)*l. % 1.59/1.80 7[0:Inp] || -> leq(skc2,pv5)*l. % 1.59/1.80 8[0:Inp] || -> leq(n0,skc2)*r. % 1.59/1.80 37[0:Inp] || -> leq(u,u)*. % 1.59/1.80 38[0:Inp] || -> equal(succ(n0),n1)**. % 1.59/1.80 67[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 1.59/1.80 84[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.59/1.80 92[0:Inp] || -> equal(plus(u,n1),succ(u))**. % 1.59/1.80 96[0:Inp] || equal(a_select3(z_defuse,skc3,skc2),use)** -> . % 1.59/1.80 103[0:Inp] || -> equal(succ(succ(u)),plus(u,n2))**. % 1.59/1.80 104[0:Inp] || -> equal(succ(succ(u)),plus(n2,u))**. % 1.59/1.80 107[0:Inp] || equal(skc2,pv5) equal(skc3,n0)** -> . % 1.59/1.80 108[0:Inp] || equal(skc2,pv5) equal(skc3,n1)** -> . % 1.59/1.80 109[0:Inp] || equal(skc2,pv5) equal(skc3,n2)** -> . % 1.59/1.80 112[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.59/1.80 134[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.59/1.80 138[0:Inp] || leq(u,n0)*+ leq(n0,u)* -> equal(u,n0). % 1.59/1.80 140[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 1.59/1.80 144[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.59/1.80 154[0:Inp] || leq(u,n2) leq(v,pred(pv5)) leq(n0,v) leq(n0,u) -> equal(a_select3(z_defuse,u,v),use)**. % 1.59/1.80 181[0:Rew:38.0,67.0] || -> equal(succ(n1),n2)**. % 1.59/1.80 185[0:Rew:104.0,103.0] || -> equal(plus(n2,u),plus(u,n2))*. % 1.59/1.80 194[0:Res:154.4,96.0] || leq(n0,skc3) leq(skc3,n2) leq(skc2,pred(pv5))*r leq(n0,skc2) -> . % 1.59/1.80 223[0:Res:8.0,144.0] || leq(skc2,n1)*l -> equal(skc2,n1) equal(skc2,n0). % 1.59/1.80 224[0:Res:8.0,138.0] || leq(skc2,n0)*l -> equal(skc2,n0). % 1.59/1.80 256[0:Res:8.0,134.0] || -> gt(skc2,n0)*l equal(skc2,n0). % 1.59/1.80 336[0:Res:7.0,134.0] || -> gt(pv5,skc2)*r equal(skc2,pv5). % 1.59/1.80 383[0:MRR:194.0,194.1,194.3,2.0,3.0,8.0] || leq(skc2,pred(pv5))*r -> . % 1.59/1.80 438[1:Spt:223.1] || -> equal(skc2,n1)**. % 1.59/1.80 454[1:Rew:438.0,224.1] || leq(skc2,n0)*l -> equal(n1,n0). % 1.59/1.80 538[1:Rew:438.0,7.0] || -> leq(n1,pv5)*r. % 1.59/1.80 541[1:Rew:438.0,383.0] || leq(n1,pred(pv5))*r -> . % 1.59/1.80 571[1:Rew:438.0,454.0] || leq(n1,n0)*l -> equal(n1,n0). % 1.59/1.80 676[0:SpR:38.0,84.0] || -> equal(pred(n1),n0)**. % 1.59/1.80 677[0:SpR:181.0,84.0] || -> equal(pred(n2),n1)**. % 1.59/1.80 728[0:SpR:104.0,84.0] || -> equal(pred(plus(n2,u)),succ(u))**. % 1.59/1.80 752[0:SpR:185.0,728.0] || -> equal(pred(plus(u,n2)),succ(u))**. % 1.59/1.80 801[1:OCh:140.1,140.0,538.0,5.0] || -> leq(n1,n0)*l. % 1.59/1.80 802[1:MRR:571.0,801.0] || -> equal(n1,n0)**. % 1.59/1.80 806[1:Rew:802.0,38.0] || -> equal(succ(n0),n0)**. % 1.59/1.80 807[1:Rew:802.0,181.0] || -> equal(succ(n0),n2)**. % 1.59/1.80 817[1:Rew:802.0,92.0] || -> equal(plus(u,n0),succ(u))**. % 1.59/1.80 866[1:Rew:802.0,541.0] || leq(n0,pred(pv5))*r -> . % 1.59/1.80 949[1:Rew:806.0,807.0] || -> equal(n2,n0)**. % 1.59/1.80 957[1:Rew:949.0,752.0] || -> equal(pred(plus(u,n0)),succ(u))**. % 1.59/1.80 1031[1:Rew:817.0,957.0] || -> equal(pred(succ(u)),succ(u))**. % 1.59/1.80 1032[1:Rew:84.0,1031.0] || -> equal(succ(u),u)**. % 1.59/1.80 1033[1:Rew:1032.0,84.0] || -> equal(pred(u),u)**. % 1.59/1.80 1100[1:Rew:1033.0,866.0] || leq(n0,pv5)*r -> . % 1.59/1.80 1101[1:MRR:1100.0,4.0] || -> . % 1.59/1.80 1185[1:Spt:1101.0,223.1,438.0] || equal(skc2,n1)** -> . % 1.59/1.80 1186[1:Spt:1101.0,223.0,223.2] || leq(skc2,n1)*l -> equal(skc2,n0). % 1.59/1.80 1191[2:Spt:256.1] || -> equal(skc2,n0)**. % 1.59/1.80 1203[2:Rew:1191.0,336.1] || -> gt(pv5,skc2)*r equal(pv5,n0). % 1.59/1.80 1204[2:Rew:1191.0,107.0] || equal(pv5,n0) equal(skc3,n0)** -> . % 1.59/1.80 1205[2:Rew:1191.0,108.0] || equal(pv5,n0) equal(skc3,n1)** -> . % 1.59/1.80 1206[2:Rew:1191.0,109.0] || equal(pv5,n0) equal(skc3,n2)** -> . % 1.59/1.80 1215[2:Rew:1191.0,383.0] || leq(n0,pred(pv5))*r -> . % 1.59/1.80 1320[2:Rew:1191.0,1203.0] || -> gt(pv5,n0)*l equal(pv5,n0). % 1.59/1.80 1542[3:Spt:1204.0] || equal(pv5,n0)** -> . % 1.59/1.80 1543[3:MRR:1320.1,1542.0] || -> gt(pv5,n0)*l. % 1.59/1.80 4676[3:Res:1543.0,112.0] || -> leq(n0,pred(pv5))*r. % 1.59/1.80 4830[3:MRR:4676.0,1215.0] || -> . % 1.59/1.80 4935[3:Spt:4830.0,1204.0,1542.0] || -> equal(pv5,n0)**. % 1.59/1.80 4936[3:Spt:4830.0,1204.1] || equal(skc3,n0)** -> . % 1.59/1.80 5017[3:Rew:4935.0,1205.0] || equal(n0,n0) equal(skc3,n1)** -> . % 1.59/1.80 5018[3:Obv:5017.0] || equal(skc3,n1)** -> . % 1.59/1.80 5019[3:Rew:4935.0,1206.0] || equal(n0,n0) equal(skc3,n2)** -> . % 1.59/1.80 5020[3:Obv:5019.0] || equal(skc3,n2)** -> . % 1.59/1.80 6055[0:Res:3.0,134.0] || -> gt(n2,skc3)*r equal(skc3,n2). % 1.59/1.80 6256[3:MRR:6055.1,5020.0] || -> gt(n2,skc3)*r. % 1.59/1.80 6268[3:Res:6256.0,112.0] || -> leq(skc3,pred(n2))*r. % 1.59/1.80 6279[3:Rew:677.0,6268.0] || -> leq(skc3,n1)*l. % 1.59/1.80 6280[3:Res:6279.0,134.0] || -> gt(n1,skc3)*r equal(skc3,n1). % 1.59/1.80 6292[3:MRR:6280.1,5018.0] || -> gt(n1,skc3)*r. % 1.59/1.80 6293[3:Res:6292.0,112.0] || -> leq(skc3,pred(n1))*r. % 1.59/1.80 6304[3:Rew:676.0,6293.0] || -> leq(skc3,n0)*l. % 1.59/1.80 6445[3:NCh:140.2,140.0,6304.0,138.0] || leq(n0,n0) leq(n0,skc3)*r -> equal(skc3,n0). % 1.59/1.80 6453[3:MRR:6445.0,6445.1,6445.2,37.0,2.0,4936.0] || -> . % 1.59/1.80 6454[2:Spt:6453.0,256.1,1191.0] || equal(skc2,n0)** -> . % 1.59/1.80 6455[2:Spt:6453.0,256.0] || -> gt(skc2,n0)*l. % 1.59/1.80 6458[2:MRR:224.1,6454.0] || leq(skc2,n0)*l -> . % 1.59/1.80 6481[3:Spt:336.1] || -> equal(skc2,pv5)**. % 1.59/1.80 6508[3:Rew:6481.0,6458.0] || leq(pv5,n0)*l -> . % 1.59/1.80 6633[3:MRR:6508.0,5.0] || -> . % 1.59/1.80 6707[3:Spt:6633.0,336.1,6481.0] || equal(skc2,pv5)** -> . % 1.59/1.80 6708[3:Spt:6633.0,336.0] || -> gt(pv5,skc2)*r. % 1.59/1.80 6709[3:Res:6708.0,112.0] || -> leq(skc2,pred(pv5))*r. % 1.59/1.80 6719[3:MRR:6709.0,383.0] || -> . % 1.59/1.80 % SZS output end Refutation % 1.59/1.80 Formulae used in the proof : quaternion_ds1_inuse_0010 reflexivity_leq successor_1 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.59/1.80 %------------------------------------------------------------------------------