%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV167+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:30 EDT 2022 % Result : Theorem 1.17s 1.32s % Output : Refutation 1.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWV167+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.10/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jun 15 13:43:37 EDT 2022 % 0.13/0.34 % CPUTime : % 1.17/1.32 % 1.17/1.32 SPASS V 3.9 % 1.17/1.32 SPASS beiseite: Proof found. % 1.17/1.32 % SZS status Theorem % 1.17/1.32 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.17/1.32 SPASS derived 2826 clauses, backtracked 615 clauses, performed 8 splits and kept 1989 clauses. % 1.17/1.32 SPASS allocated 88279 KBytes. % 1.17/1.32 SPASS spent 0:00:00.96 on the problem. % 1.17/1.32 0:00:00.04 for the input. % 1.17/1.32 0:00:00.08 for the FLOTTER CNF translation. % 1.17/1.32 0:00:00.02 for inferences. % 1.17/1.32 0:00:00.02 for the backtracking. % 1.17/1.32 0:00:00.66 for the reduction. % 1.17/1.32 % 1.17/1.32 % 1.17/1.32 Here is a proof with depth 3, length 69 : % 1.17/1.32 % SZS output start Refutation % 1.17/1.32 2[0:Inp] || -> leq(n0,skc1)*r. % 1.17/1.32 3[0:Inp] || -> leq(n0,pv40)*l. % 1.17/1.32 4[0:Inp] || -> leq(pv40,n4)*r. % 1.17/1.32 5[0:Inp] || -> leq(skc1,pv40)*l. % 1.17/1.32 34[0:Inp] || -> leq(u,u)*. % 1.17/1.32 35[0:Inp] || -> equal(succ(n0),n1)**. % 1.17/1.32 36[0:Inp] || gt(u,u)* -> . % 1.17/1.32 38[0:Inp] || -> equal(succ(tptp_minus_1),n0)**. % 1.17/1.32 40[0:Inp] || -> equal(a_select2(mu_init,pv40),init)**. % 1.17/1.32 42[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 1.17/1.32 59[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.17/1.32 61[0:Inp] || equal(a_select2(mu_init,skc1),init)** -> . % 1.17/1.32 62[0:Inp] || -> equal(succ(succ(succ(n0))),n3)**. % 1.17/1.32 69[0:Inp] || -> equal(succ(succ(succ(succ(n0)))),n4)**. % 1.17/1.32 81[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.17/1.32 103[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.17/1.32 114[0:Inp] || leq(u,pred(pv40)) leq(n0,u) -> equal(a_select2(mu_init,u),init)**. % 1.17/1.32 117[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.17/1.32 156[0:Rew:35.0,42.0] || -> equal(succ(n1),n2)**. % 1.17/1.32 159[0:Rew:156.0,62.0,35.0,62.0] || -> equal(succ(n2),n3)**. % 1.17/1.32 161[0:Rew:159.0,69.0,156.0,69.0,35.0,69.0] || -> equal(succ(n3),n4)**. % 1.17/1.32 169[0:Res:114.2,61.0] || leq(n0,skc1) leq(skc1,pred(pv40))*r -> . % 1.17/1.32 176[0:Res:103.1,61.0] || leq(init,a_select2(mu_init,skc1))*r -> gt(a_select2(mu_init,skc1),init). % 1.17/1.32 194[0:Res:5.0,103.0] || -> gt(pv40,skc1)*r equal(skc1,pv40). % 1.17/1.32 253[0:Res:4.0,103.0] || -> gt(n4,pv40)*l equal(n4,pv40). % 1.17/1.32 323[0:Res:3.0,117.0] || leq(pv40,n1)*r -> equal(n1,pv40) equal(n0,pv40). % 1.17/1.32 429[0:MRR:169.0,2.0] || leq(skc1,pred(pv40))*r -> . % 1.17/1.32 522[1:Spt:323.2] || -> equal(n0,pv40)**. % 1.17/1.32 681[1:Rew:522.0,38.0] || -> equal(succ(tptp_minus_1),pv40)**. % 1.17/1.32 815[2:Spt:194.1] || -> equal(skc1,pv40)**. % 1.17/1.32 818[2:Rew:815.0,176.1] || leq(init,a_select2(mu_init,skc1))*r -> gt(a_select2(mu_init,pv40),init). % 1.17/1.32 875[2:Rew:40.0,818.1,40.0,818.0,815.0,818.0] || leq(init,init)* -> gt(init,init). % 1.17/1.32 876[2:MRR:875.0,875.1,34.0,36.0] || -> . % 1.17/1.32 879[2:Spt:876.0,194.1,815.0] || equal(skc1,pv40)** -> . % 1.17/1.32 880[2:Spt:876.0,194.0] || -> gt(pv40,skc1)*r. % 1.17/1.32 896[0:SpR:161.0,59.0] || -> equal(pred(n4),n3)**. % 1.17/1.32 898[1:SpR:681.0,59.0] || -> equal(pred(pv40),tptp_minus_1)**. % 1.17/1.32 903[1:Rew:898.0,429.0] || leq(skc1,tptp_minus_1)*l -> . % 1.17/1.32 3463[2:Res:880.0,81.0] || -> leq(skc1,pred(pv40))*r. % 1.17/1.32 3603[2:Rew:898.0,3463.0] || -> leq(skc1,tptp_minus_1)*l. % 1.17/1.32 3604[2:MRR:3603.0,903.0] || -> . % 1.17/1.32 3694[1:Spt:3604.0,323.2,522.0] || equal(n0,pv40)** -> . % 1.17/1.32 3695[1:Spt:3604.0,323.0,323.1] || leq(pv40,n1)*r -> equal(n1,pv40). % 1.17/1.32 3707[2:Spt:253.1] || -> equal(n4,pv40)**. % 1.17/1.32 3711[2:Rew:3707.0,896.0] || -> equal(pred(pv40),n3)**. % 1.17/1.32 3944[2:Rew:3711.0,429.0] || leq(skc1,n3)*l -> . % 1.17/1.32 3983[3:Spt:194.1] || -> equal(skc1,pv40)**. % 1.17/1.32 3991[3:Rew:3983.0,176.1] || leq(init,a_select2(mu_init,skc1))*r -> gt(a_select2(mu_init,pv40),init). % 1.17/1.32 4051[3:Rew:40.0,3991.1] || leq(init,a_select2(mu_init,skc1))*r -> gt(init,init). % 1.17/1.32 4052[3:Rew:3983.0,4051.0] || leq(init,a_select2(mu_init,pv40))*r -> gt(init,init). % 1.17/1.32 4053[3:Rew:40.0,4052.0] || leq(init,init)* -> gt(init,init). % 1.17/1.32 4054[3:MRR:4053.0,4053.1,34.0,36.0] || -> . % 1.17/1.32 4057[3:Spt:4054.0,194.1,3983.0] || equal(skc1,pv40)** -> . % 1.17/1.32 4058[3:Spt:4054.0,194.0] || -> gt(pv40,skc1)*r. % 1.17/1.32 4059[3:Res:4058.0,81.0] || -> leq(skc1,pred(pv40))*r. % 1.17/1.32 4067[3:Rew:3711.0,4059.0] || -> leq(skc1,n3)*l. % 1.17/1.32 4068[3:MRR:4067.0,3944.0] || -> . % 1.17/1.32 4069[2:Spt:4068.0,253.1,3707.0] || equal(n4,pv40)** -> . % 1.17/1.32 4070[2:Spt:4068.0,253.0] || -> gt(n4,pv40)*l. % 1.17/1.32 4081[3:Spt:194.1] || -> equal(skc1,pv40)**. % 1.17/1.32 4088[3:Rew:4081.0,176.1] || leq(init,a_select2(mu_init,skc1))*r -> gt(a_select2(mu_init,pv40),init). % 1.17/1.32 4148[3:Rew:40.0,4088.1] || leq(init,a_select2(mu_init,skc1))*r -> gt(init,init). % 1.17/1.32 4149[3:Rew:4081.0,4148.0] || leq(init,a_select2(mu_init,pv40))*r -> gt(init,init). % 1.17/1.32 4150[3:Rew:40.0,4149.0] || leq(init,init)* -> gt(init,init). % 1.17/1.32 4151[3:MRR:4150.0,4150.1,34.0,36.0] || -> . % 1.17/1.32 4154[3:Spt:4151.0,194.1,4081.0] || equal(skc1,pv40)** -> . % 1.17/1.32 4155[3:Spt:4151.0,194.0] || -> gt(pv40,skc1)*r. % 1.17/1.32 4156[3:Res:4155.0,81.0] || -> leq(skc1,pred(pv40))*r. % 1.17/1.32 4164[3:MRR:4156.0,429.0] || -> . % 1.17/1.32 % SZS output end Refutation % 1.17/1.32 Formulae used in the proof : cl5_nebula_init_0011 reflexivity_leq successor_1 irreflexivity_gt succ_tptp_minus_1 successor_2 pred_succ successor_3 successor_4 leq_gt_pred leq_gt2 finite_domain_1 % 1.17/1.32 %------------------------------------------------------------------------------