%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV196+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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.08s 1.27s % Output : Refutation 1.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV196+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 11:50:10 EDT 2022 % 0.13/0.34 % CPUTime : % 1.08/1.27 % 1.08/1.27 SPASS V 3.9 % 1.08/1.27 SPASS beiseite: Proof found. % 1.08/1.27 % SZS status Theorem % 1.08/1.27 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.08/1.27 SPASS derived 3406 clauses, backtracked 517 clauses, performed 5 splits and kept 2189 clauses. % 1.08/1.27 SPASS allocated 88783 KBytes. % 1.08/1.27 SPASS spent 0:00:00.89 on the problem. % 1.08/1.27 0:00:00.04 for the input. % 1.08/1.27 0:00:00.08 for the FLOTTER CNF translation. % 1.08/1.27 0:00:00.02 for inferences. % 1.08/1.27 0:00:00.02 for the backtracking. % 1.08/1.27 0:00:00.64 for the reduction. % 1.08/1.27 % 1.08/1.27 % 1.08/1.27 Here is a proof with depth 3, length 64 : % 1.08/1.27 % SZS output start Refutation % 1.08/1.27 2[0:Inp] || -> leq(n0,skc3)*r. % 1.08/1.27 3[0:Inp] || -> leq(skc3,n2)*l. % 1.08/1.27 4[0:Inp] || -> leq(n0,pv5)*r. % 1.08/1.27 5[0:Inp] || -> leq(pv5,n0)*l. % 1.08/1.27 7[0:Inp] || -> gt(pv5,n0)*l. % 1.08/1.27 8[0:Inp] || -> leq(skc2,pv5)*l. % 1.08/1.27 9[0:Inp] || -> leq(n0,skc2)*r. % 1.08/1.27 39[0:Inp] || -> equal(succ(n0),n1)**. % 1.08/1.27 68[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 1.08/1.27 85[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.08/1.27 93[0:Inp] || -> equal(plus(u,n1),succ(u))**. % 1.08/1.27 97[0:Inp] || equal(a_select3(z_defuse,skc3,skc2),use)** -> . % 1.08/1.27 104[0:Inp] || -> equal(succ(succ(u)),plus(u,n2))**. % 1.08/1.27 105[0:Inp] || -> equal(succ(succ(u)),plus(n2,u))**. % 1.08/1.27 113[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.08/1.27 135[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.08/1.27 139[0:Inp] || leq(u,n0)* leq(n0,u)* -> equal(u,n0). % 1.08/1.27 141[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 1.08/1.27 145[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.08/1.27 155[0:Inp] || leq(u,n2) leq(v,pred(pv5)) leq(n0,v) leq(n0,u) -> equal(a_select3(z_defuse,u,v),use)**. % 1.08/1.27 182[0:Rew:39.0,68.0] || -> equal(succ(n1),n2)**. % 1.08/1.27 186[0:Rew:105.0,104.0] || -> equal(plus(n2,u),plus(u,n2))*. % 1.08/1.27 195[0:Res:155.4,97.0] || leq(n0,skc3) leq(skc3,n2) leq(skc2,pred(pv5))*r leq(n0,skc2) -> . % 1.08/1.27 224[0:Res:9.0,145.0] || leq(skc2,n1)*l -> equal(skc2,n1) equal(skc2,n0). % 1.08/1.27 225[0:Res:9.0,139.0] || leq(skc2,n0)*l -> equal(skc2,n0). % 1.08/1.27 257[0:Res:9.0,135.0] || -> gt(skc2,n0)*l equal(skc2,n0). % 1.08/1.27 337[0:Res:8.0,135.0] || -> gt(pv5,skc2)*r equal(skc2,pv5). % 1.08/1.27 384[0:MRR:195.0,195.1,195.3,2.0,3.0,9.0] || leq(skc2,pred(pv5))*r -> . % 1.08/1.27 439[1:Spt:224.1] || -> equal(skc2,n1)**. % 1.08/1.27 455[1:Rew:439.0,225.1] || leq(skc2,n0)*l -> equal(n1,n0). % 1.08/1.27 539[1:Rew:439.0,8.0] || -> leq(n1,pv5)*r. % 1.08/1.27 542[1:Rew:439.0,384.0] || leq(n1,pred(pv5))*r -> . % 1.08/1.27 572[1:Rew:439.0,455.0] || leq(n1,n0)*l -> equal(n1,n0). % 1.08/1.27 729[0:SpR:105.0,85.0] || -> equal(pred(plus(n2,u)),succ(u))**. % 1.08/1.27 753[0:SpR:186.0,729.0] || -> equal(pred(plus(u,n2)),succ(u))**. % 1.08/1.27 802[1:OCh:141.1,141.0,539.0,5.0] || -> leq(n1,n0)*l. % 1.08/1.27 803[1:MRR:572.0,802.0] || -> equal(n1,n0)**. % 1.08/1.27 807[1:Rew:803.0,39.0] || -> equal(succ(n0),n0)**. % 1.08/1.27 808[1:Rew:803.0,182.0] || -> equal(succ(n0),n2)**. % 1.08/1.27 818[1:Rew:803.0,93.0] || -> equal(plus(u,n0),succ(u))**. % 1.08/1.27 867[1:Rew:803.0,542.0] || leq(n0,pred(pv5))*r -> . % 1.08/1.27 950[1:Rew:807.0,808.0] || -> equal(n2,n0)**. % 1.08/1.27 958[1:Rew:950.0,753.0] || -> equal(pred(plus(u,n0)),succ(u))**. % 1.08/1.27 1032[1:Rew:818.0,958.0] || -> equal(pred(succ(u)),succ(u))**. % 1.08/1.27 1033[1:Rew:85.0,1032.0] || -> equal(succ(u),u)**. % 1.08/1.27 1034[1:Rew:1033.0,85.0] || -> equal(pred(u),u)**. % 1.08/1.27 1101[1:Rew:1034.0,867.0] || leq(n0,pv5)*r -> . % 1.08/1.27 1102[1:MRR:1101.0,4.0] || -> . % 1.08/1.27 1186[1:Spt:1102.0,224.1,439.0] || equal(skc2,n1)** -> . % 1.08/1.27 1187[1:Spt:1102.0,224.0,224.2] || leq(skc2,n1)*l -> equal(skc2,n0). % 1.08/1.27 1192[2:Spt:257.1] || -> equal(skc2,n0)**. % 1.08/1.27 1216[2:Rew:1192.0,384.0] || leq(n0,pred(pv5))*r -> . % 1.08/1.27 4673[0:Res:7.0,113.0] || -> leq(n0,pred(pv5))*r. % 1.08/1.27 4827[2:MRR:4673.0,1216.0] || -> . % 1.08/1.27 4935[2:Spt:4827.0,257.1,1192.0] || equal(skc2,n0)** -> . % 1.08/1.27 4936[2:Spt:4827.0,257.0] || -> gt(skc2,n0)*l. % 1.08/1.27 4938[2:MRR:225.1,4935.0] || leq(skc2,n0)*l -> . % 1.08/1.27 4951[3:Spt:337.1] || -> equal(skc2,pv5)**. % 1.08/1.27 4978[3:Rew:4951.0,4938.0] || leq(pv5,n0)*l -> . % 1.08/1.27 5093[3:MRR:4978.0,5.0] || -> . % 1.08/1.27 5166[3:Spt:5093.0,337.1,4951.0] || equal(skc2,pv5)** -> . % 1.08/1.27 5167[3:Spt:5093.0,337.0] || -> gt(pv5,skc2)*r. % 1.08/1.27 5168[3:Res:5167.0,113.0] || -> leq(skc2,pred(pv5))*r. % 1.08/1.27 5176[3:MRR:5168.0,384.0] || -> . % 1.08/1.27 % SZS output end Refutation % 1.08/1.27 Formulae used in the proof : quaternion_ds1_inuse_0007 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.08/1.27 %------------------------------------------------------------------------------