%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV370+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:42:33 EDT 2022 % Result : Theorem 0.20s 0.56s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWV370+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.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.35 % DateTime : Wed Jun 15 00:51:11 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.56 % 0.20/0.56 SPASS V 3.9 % 0.20/0.56 SPASS beiseite: Proof found. % 0.20/0.56 % SZS status Theorem % 0.20/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.56 SPASS derived 733 clauses, backtracked 14 clauses, performed 3 splits and kept 360 clauses. % 0.20/0.56 SPASS allocated 98421 KBytes. % 0.20/0.56 SPASS spent 0:00:00.20 on the problem. % 0.20/0.56 0:00:00.04 for the input. % 0.20/0.56 0:00:00.05 for the FLOTTER CNF translation. % 0.20/0.56 0:00:00.01 for inferences. % 0.20/0.56 0:00:00.00 for the backtracking. % 0.20/0.56 0:00:00.08 for the reduction. % 0.20/0.56 % 0.20/0.56 % 0.20/0.56 Here is a proof with depth 5, length 44 : % 0.20/0.56 % SZS output start Refutation % 0.20/0.56 41[0:Inp] || contains_pq(u,v) -> contains_pq(insert_pq(u,w),v)*. % 0.20/0.56 42[0:Inp] || equal(u,v) -> contains_pq(insert_pq(w,u),v)*. % 0.20/0.56 49[0:Inp] || contains_cpq(triple(u,v,w),x)* -> contains_slb(v,x). % 0.20/0.56 50[0:Inp] || contains_slb(u,v) -> contains_cpq(triple(w,u,x),v)*. % 0.20/0.56 55[0:Inp] || contains_slb(u,v) -> contains_slb(insert_slb(u,pair(w,x)),v)*. % 0.20/0.56 56[0:Inp] || equal(u,v) -> contains_slb(insert_slb(w,pair(u,x)),v)*. % 0.20/0.56 60[0:Inp] || contains_pq(insert_pq(u,v),w)* -> contains_pq(u,w) equal(v,w). % 0.20/0.56 66[0:Inp] || contains_cpq(triple(u,skc6,v),w) -> contains_pq(i(triple(u,skc6,v)),w)*. % 0.20/0.56 67[0:Inp] || contains_pq(i(triple(u,skc6,v)),w)* -> contains_cpq(triple(u,skc6,v),w). % 0.20/0.56 68[0:Inp] || contains_slb(insert_slb(u,pair(v,w)),x)* -> contains_slb(u,x) equal(v,x). % 0.20/0.56 76[0:Inp] || -> equal(i(triple(u,insert_slb(v,pair(w,x)),y)),insert_pq(i(triple(u,v,y)),w))**. % 0.20/0.56 84[0:Inp] || -> contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11) contains_pq(i(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8)),skc11)*. % 0.20/0.56 86[0:Inp] || contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11) contains_pq(i(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8)),skc11)* -> . % 0.20/0.56 95[0:Rew:76.0,84.1] || -> contains_pq(insert_pq(i(triple(skc7,skc6,skc8)),skc9),skc11) contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11)*. % 0.20/0.56 96[0:Rew:76.0,86.1] || contains_pq(insert_pq(i(triple(skc7,skc6,skc8)),skc9),skc11) contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11)* -> . % 0.20/0.56 823[1:Spt:95.0] || -> contains_pq(insert_pq(i(triple(skc7,skc6,skc8)),skc9),skc11)*. % 0.20/0.56 824[1:MRR:96.0,823.0] || contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11)* -> . % 0.20/0.56 827[1:Res:823.0,60.0] || -> contains_pq(i(triple(skc7,skc6,skc8)),skc11)* equal(skc11,skc9). % 0.20/0.56 828[2:Spt:827.1] || -> equal(skc11,skc9)**. % 0.20/0.56 830[2:Rew:828.0,824.0] || contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc9)* -> . % 0.20/0.56 836[2:Res:50.1,830.0] || contains_slb(insert_slb(skc6,pair(skc9,skc10)),skc9)* -> . % 0.20/0.56 837[2:Res:56.1,836.0] || equal(skc9,skc9)* -> . % 0.20/0.56 839[2:Obv:837.0] || -> . % 0.20/0.56 840[2:Spt:839.0,827.1,828.0] || equal(skc11,skc9)** -> . % 0.20/0.56 841[2:Spt:839.0,827.0] || -> contains_pq(i(triple(skc7,skc6,skc8)),skc11)*. % 0.20/0.56 845[2:Res:841.0,67.0] || -> contains_cpq(triple(skc7,skc6,skc8),skc11)*. % 0.20/0.56 855[2:Res:845.0,49.0] || -> contains_slb(skc6,skc11)*. % 0.20/0.56 863[1:Res:50.1,824.0] || contains_slb(insert_slb(skc6,pair(skc9,skc10)),skc11)* -> . % 0.20/0.56 865[1:Res:55.1,863.0] || contains_slb(skc6,skc11)* -> . % 0.20/0.56 866[2:MRR:865.0,855.0] || -> . % 0.20/0.56 867[1:Spt:866.0,95.0,823.0] || contains_pq(insert_pq(i(triple(skc7,skc6,skc8)),skc9),skc11)* -> . % 0.20/0.56 868[1:Spt:866.0,95.1] || -> contains_cpq(triple(skc7,insert_slb(skc6,pair(skc9,skc10)),skc8),skc11)*. % 0.20/0.56 869[1:Res:868.0,49.0] || -> contains_slb(insert_slb(skc6,pair(skc9,skc10)),skc11)*. % 0.20/0.56 870[1:Res:869.0,68.0] || -> contains_slb(skc6,skc11)* equal(skc11,skc9). % 0.20/0.56 871[2:Spt:870.1] || -> equal(skc11,skc9)**. % 0.20/0.56 874[2:Rew:871.0,867.0] || contains_pq(insert_pq(i(triple(skc7,skc6,skc8)),skc9),skc9)* -> . % 0.20/0.56 877[2:Res:42.1,874.0] || equal(skc9,skc9)* -> . % 0.20/0.56 879[2:Obv:877.0] || -> . % 0.20/0.56 880[2:Spt:879.0,870.1,871.0] || equal(skc11,skc9)** -> . % 0.20/0.56 881[2:Spt:879.0,870.0] || -> contains_slb(skc6,skc11)*. % 0.20/0.56 890[1:Res:41.1,867.0] || contains_pq(i(triple(skc7,skc6,skc8)),skc11)* -> . % 0.20/0.56 892[1:Res:66.1,890.0] || contains_cpq(triple(skc7,skc6,skc8),skc11)* -> . % 0.20/0.56 894[1:Res:50.1,892.0] || contains_slb(skc6,skc11)* -> . % 0.20/0.56 895[2:MRR:894.0,881.0] || -> . % 0.20/0.56 % SZS output end Refutation % 0.20/0.56 Formulae used in the proof : ax9 ax39 ax21 l6_co ax55 % 0.20/0.56 %------------------------------------------------------------------------------