%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV122+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:21 EDT 2022 % Result : Theorem 2.16s 2.41s % Output : Refutation 2.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.14 % Problem : SWV122+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.12/0.14 % Command : run_spass %d %s % 0.15/0.36 % Computer : n029.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Tue Jun 14 20:07:11 EDT 2022 % 0.15/0.36 % CPUTime : % 2.16/2.41 % 2.16/2.41 SPASS V 3.9 % 2.16/2.41 SPASS beiseite: Proof found. % 2.16/2.41 % SZS status Theorem % 2.16/2.41 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.16/2.41 SPASS derived 5739 clauses, backtracked 328 clauses, performed 4 splits and kept 3184 clauses. % 2.16/2.41 SPASS allocated 91056 KBytes. % 2.16/2.41 SPASS spent 0:00:01.99 on the problem. % 2.16/2.41 0:00:00.04 for the input. % 2.16/2.41 0:00:00.08 for the FLOTTER CNF translation. % 2.16/2.41 0:00:00.05 for inferences. % 2.16/2.41 0:00:00.03 for the backtracking. % 2.16/2.41 0:00:01.60 for the reduction. % 2.16/2.41 % 2.16/2.41 % 2.16/2.41 Here is a proof with depth 1, length 35 : % 2.16/2.41 % SZS output start Refutation % 2.16/2.41 1[0:Inp] || -> SkC0*. % 2.16/2.41 2[0:Inp] || -> SkC1*. % 2.16/2.41 6[0:Inp] || -> leq(n0,skc7)*r. % 2.16/2.41 36[0:Inp] || -> equal(succ(n0),n1)**. % 2.16/2.41 43[0:Inp] || -> leq(skc6,minus(n6,n1))*r. % 2.16/2.41 44[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 2.16/2.41 61[0:Inp] || -> equal(pred(succ(u)),u)**. % 2.16/2.41 63[0:Inp] || -> equal(succ(succ(succ(n0))),n3)**. % 2.16/2.41 68[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 2.16/2.41 70[0:Inp] || SkC0* SkC1 -> leq(n0,skc6). % 2.16/2.41 71[0:Inp] || -> equal(succ(succ(succ(succ(n0)))),n4)**. % 2.16/2.41 81[0:Inp] || -> equal(succ(succ(succ(succ(succ(n0))))),n5)**. % 2.16/2.41 97[0:Inp] || SkC0 SkC1 -> leq(skc7,minus(n6,n1))*r. % 2.16/2.41 98[0:Inp] || -> equal(succ(succ(succ(succ(succ(succ(n0)))))),n6)**. % 2.16/2.41 117[0:Inp] || equal(a_select3(pminus_ds1_filter,skc7,skc6),a_select3(pminus_ds1_filter,skc6,skc7))** SkC0 SkC1 -> . % 2.16/2.41 135[0:Inp] || leq(n0,u) leq(u,minus(n6,n1)) leq(v,minus(n6,n1)) leq(n0,v) -> equal(a_select3(pminus_ds1_filter,u,v),a_select3(pminus_ds1_filter,v,u))*. % 2.16/2.41 157[0:Rew:36.0,44.0] || -> equal(succ(n1),n2)**. % 2.16/2.41 160[0:Rew:157.0,63.0,36.0,63.0] || -> equal(succ(n2),n3)**. % 2.16/2.41 162[0:Rew:160.0,71.0,157.0,71.0,36.0,71.0] || -> equal(succ(n3),n4)**. % 2.16/2.41 165[0:Rew:162.0,81.0,160.0,81.0,157.0,81.0,36.0,81.0] || -> equal(succ(n4),n5)**. % 2.16/2.41 168[0:Rew:165.0,98.0,162.0,98.0,160.0,98.0,157.0,98.0,36.0,98.0] || -> equal(succ(n5),n6)**. % 2.16/2.41 171[0:Rew:68.0,43.0] || -> leq(skc6,pred(n6))*r. % 2.16/2.41 174[0:MRR:70.0,70.1,1.0,2.0] || -> leq(n0,skc6)*r. % 2.16/2.41 175[0:MRR:117.1,117.2,1.0,2.0] || equal(a_select3(pminus_ds1_filter,skc7,skc6),a_select3(pminus_ds1_filter,skc6,skc7))** -> . % 2.16/2.41 176[0:Rew:68.0,97.2] || SkC0 SkC1 -> leq(skc7,pred(n6))*r. % 2.16/2.41 177[0:MRR:176.0,176.1,1.0,2.0] || -> leq(skc7,pred(n6))*r. % 2.16/2.41 178[0:Rew:68.0,135.2,68.0,135.1] || leq(u,pred(n6)) leq(v,pred(n6)) leq(n0,u) leq(n0,v) -> equal(a_select3(pminus_ds1_filter,v,u),a_select3(pminus_ds1_filter,u,v))*. % 2.16/2.41 790[0:SpR:168.0,61.0] || -> equal(pred(n6),n5)**. % 2.16/2.41 797[0:Rew:790.0,178.0] || leq(u,n5) leq(v,pred(n6)) leq(n0,u) leq(n0,v) -> equal(a_select3(pminus_ds1_filter,v,u),a_select3(pminus_ds1_filter,u,v))*. % 2.16/2.41 799[0:Rew:790.0,171.0] || -> leq(skc6,n5)*l. % 2.16/2.41 805[0:Rew:790.0,797.1] || leq(u,n5) leq(v,n5) leq(n0,u) leq(n0,v) -> equal(a_select3(pminus_ds1_filter,v,u),a_select3(pminus_ds1_filter,u,v))*. % 2.16/2.41 7273[0:Rew:790.0,177.0] || -> leq(skc7,n5)*l. % 2.16/2.41 7819[0:SpL:805.4,175.0] || leq(skc7,n5) leq(skc6,n5) leq(n0,skc7) leq(n0,skc6) equal(a_select3(pminus_ds1_filter,skc6,skc7),a_select3(pminus_ds1_filter,skc6,skc7))* -> . % 2.16/2.41 7823[0:Obv:7819.4] || leq(skc7,n5)*l leq(skc6,n5) leq(n0,skc7) leq(n0,skc6) -> . % 2.16/2.41 7824[0:MRR:7823.0,7823.1,7823.2,7823.3,7273.0,799.0,6.0,174.0] || -> . % 2.16/2.41 % SZS output end Refutation % 2.16/2.41 Formulae used in the proof : quaternion_ds1_symm_0015 gt_succ leq_succ_gt_equiv successor_1 successor_2 pred_succ successor_3 pred_minus_1 successor_4 successor_5 successor_6 % 2.16/2.41 %------------------------------------------------------------------------------