%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV209+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:38 EDT 2022 % Result : Theorem 1.05s 1.26s % Output : Refutation 1.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV209+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.32 % Computer : n011.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Tue Jun 14 18:20:04 EDT 2022 % 0.12/0.33 % CPUTime : % 1.05/1.26 % 1.05/1.26 SPASS V 3.9 % 1.05/1.26 SPASS beiseite: Proof found. % 1.05/1.26 % SZS status Theorem % 1.05/1.26 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.05/1.26 SPASS derived 1272 clauses, backtracked 659 clauses, performed 5 splits and kept 1676 clauses. % 1.05/1.26 SPASS allocated 87409 KBytes. % 1.05/1.26 SPASS spent 0:00:00.91 on the problem. % 1.05/1.26 0:00:00.04 for the input. % 1.05/1.26 0:00:00.09 for the FLOTTER CNF translation. % 1.05/1.26 0:00:00.00 for inferences. % 1.05/1.26 0:00:00.03 for the backtracking. % 1.05/1.26 0:00:00.61 for the reduction. % 1.05/1.26 % 1.05/1.26 % 1.05/1.26 Here is a proof with depth 3, length 60 : % 1.05/1.26 % SZS output start Refutation % 1.05/1.26 2[0:Inp] || -> leq(n0,skc1)*r. % 1.05/1.26 3[0:Inp] || -> leq(skc1,n5)*l. % 1.05/1.26 32[0:Inp] || -> leq(u,u)*. % 1.05/1.26 34[0:Inp] || gt(u,u)* -> . % 1.05/1.26 56[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n0),use)**. % 1.05/1.26 57[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n1),use)**. % 1.05/1.26 58[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n2),use)**. % 1.05/1.26 59[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n3),use)**. % 1.05/1.26 60[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n4),use)**. % 1.05/1.26 61[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n5),use)**. % 1.05/1.26 84[0:Inp] || equal(a_select2(xinit_noise_defuse,skc1),use)** -> . % 1.05/1.26 126[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.05/1.26 136[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.05/1.26 149[0:Inp] || leq(u,n5)* leq(n0,u) -> equal(u,n5) equal(u,n4) equal(u,n3) equal(u,n2) equal(u,n1) equal(u,n0). % 1.05/1.26 192[0:Res:126.1,84.0] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,skc1),use). % 1.05/1.26 210[0:Res:3.0,126.0] || -> gt(n5,skc1)*r equal(skc1,n5). % 1.05/1.26 269[0:Res:2.0,149.0] || leq(skc1,n5)*l -> equal(skc1,n0) equal(skc1,n1) equal(skc1,n2) equal(skc1,n3) equal(skc1,n4) equal(skc1,n5). % 1.05/1.26 273[0:Res:2.0,136.0] || leq(skc1,n1)*l -> equal(skc1,n1) equal(skc1,n0). % 1.05/1.26 306[0:Res:2.0,126.0] || -> gt(skc1,n0)*l equal(skc1,n0). % 1.05/1.26 373[0:MRR:269.0,3.0] || -> equal(skc1,n5)** equal(skc1,n4) equal(skc1,n3) equal(skc1,n2) equal(skc1,n1) equal(skc1,n0). % 1.05/1.26 431[1:Spt:273.1] || -> equal(skc1,n1)**. % 1.05/1.26 434[1:Rew:431.0,192.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,n1),use). % 1.05/1.26 576[1:Rew:57.0,434.1,57.0,434.0,431.0,434.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 577[1:MRR:576.0,576.1,32.0,34.0] || -> . % 1.05/1.26 641[1:Spt:577.0,273.1,431.0] || equal(skc1,n1)** -> . % 1.05/1.26 642[1:Spt:577.0,273.0,273.2] || leq(skc1,n1)*l -> equal(skc1,n0). % 1.05/1.26 643[1:MRR:373.4,641.0] || -> equal(skc1,n5)** equal(skc1,n4) equal(skc1,n3) equal(skc1,n2) equal(skc1,n0). % 1.05/1.26 647[2:Spt:306.1] || -> equal(skc1,n0)**. % 1.05/1.26 656[2:Rew:647.0,192.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,n0),use). % 1.05/1.26 786[2:Rew:56.0,656.1,56.0,656.0,647.0,656.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 787[2:MRR:786.0,786.1,32.0,34.0] || -> . % 1.05/1.26 849[2:Spt:787.0,306.1,647.0] || equal(skc1,n0)** -> . % 1.05/1.26 850[2:Spt:787.0,306.0] || -> gt(skc1,n0)*l. % 1.05/1.26 853[2:MRR:643.4,849.0] || -> equal(skc1,n5)** equal(skc1,n4) equal(skc1,n3) equal(skc1,n2). % 1.05/1.26 859[3:Spt:210.1] || -> equal(skc1,n5)**. % 1.05/1.26 870[3:Rew:859.0,192.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,n5),use). % 1.05/1.26 1004[3:Rew:61.0,870.1,61.0,870.0,859.0,870.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 1005[3:MRR:1004.0,1004.1,32.0,34.0] || -> . % 1.05/1.26 1067[3:Spt:1005.0,210.1,859.0] || equal(skc1,n5)** -> . % 1.05/1.26 1068[3:Spt:1005.0,210.0] || -> gt(n5,skc1)*r. % 1.05/1.26 1069[3:MRR:853.0,1067.0] || -> equal(skc1,n4)** equal(skc1,n3) equal(skc1,n2). % 1.05/1.26 1679[4:Spt:1069.0] || -> equal(skc1,n4)**. % 1.05/1.26 1701[4:Rew:1679.0,192.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,n4),use). % 1.05/1.26 1835[4:Rew:60.0,1701.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(use,use). % 1.05/1.26 1836[4:Rew:1679.0,1835.0] || leq(use,a_select2(xinit_noise_defuse,n4))*r -> gt(use,use). % 1.05/1.26 1837[4:Rew:60.0,1836.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 1838[4:MRR:1837.0,1837.1,32.0,34.0] || -> . % 1.05/1.26 1898[4:Spt:1838.0,1069.0,1679.0] || equal(skc1,n4)** -> . % 1.05/1.26 1899[4:Spt:1838.0,1069.1,1069.2] || -> equal(skc1,n3)** equal(skc1,n2). % 1.05/1.26 1901[5:Spt:1899.0] || -> equal(skc1,n3)**. % 1.05/1.26 1913[5:Rew:1901.0,192.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(a_select2(xinit_noise_defuse,n3),use). % 1.05/1.26 2055[5:Rew:59.0,1913.1] || leq(use,a_select2(xinit_noise_defuse,skc1))*r -> gt(use,use). % 1.05/1.26 2056[5:Rew:1901.0,2055.0] || leq(use,a_select2(xinit_noise_defuse,n3))*r -> gt(use,use). % 1.05/1.26 2057[5:Rew:59.0,2056.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 2058[5:MRR:2057.0,2057.1,32.0,34.0] || -> . % 1.05/1.26 2118[5:Spt:2058.0,1899.0,1901.0] || equal(skc1,n3)** -> . % 1.05/1.26 2119[5:Spt:2058.0,1899.1] || -> equal(skc1,n2)**. % 1.05/1.26 2169[5:Rew:2119.0,192.1,2119.0,192.0] || leq(use,a_select2(xinit_noise_defuse,n2))*r -> gt(a_select2(xinit_noise_defuse,n2),use). % 1.05/1.26 2170[5:Rew:58.0,2169.1,58.0,2169.0] || leq(use,use)* -> gt(use,use). % 1.05/1.26 2171[5:MRR:2170.0,2170.1,32.0,34.0] || -> . % 1.05/1.26 % SZS output end Refutation % 1.05/1.26 Formulae used in the proof : quaternion_ds1_inuse_0020 reflexivity_leq irreflexivity_gt leq_gt2 finite_domain_1 finite_domain_5 % 1.05/1.26 %------------------------------------------------------------------------------