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