%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU156+3 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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 : Tue Jul 19 14:34:27 EDT 2022 % Result : Theorem 7.97s 8.16s % Output : Refutation 8.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU156+3 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n009.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 19 01:43:07 EDT 2022 % 0.12/0.34 % CPUTime : % 7.97/8.16 % 7.97/8.16 SPASS V 3.9 % 7.97/8.16 SPASS beiseite: Proof found. % 7.97/8.16 % SZS status Theorem % 7.97/8.16 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 7.97/8.16 SPASS derived 4223 clauses, backtracked 577 clauses, performed 2 splits and kept 2194 clauses. % 7.97/8.16 SPASS allocated 91666 KBytes. % 7.97/8.16 SPASS spent 0:00:07.81 on the problem. % 7.97/8.16 0:00:00.03 for the input. % 7.97/8.16 0:00:00.02 for the FLOTTER CNF translation. % 7.97/8.16 0:00:00.06 for inferences. % 7.97/8.16 0:00:00.02 for the backtracking. % 7.97/8.16 0:00:07.64 for the reduction. % 7.97/8.16 % 7.97/8.16 % 7.97/8.16 Here is a proof with depth 9, length 87 : % 7.97/8.16 % SZS output start Refutation % 7.97/8.16 3[0:Inp] || -> subset(u,u)*. % 7.97/8.16 5[0:Inp] || -> equal(unordered_pair(u,u),singleton(u))**. % 7.97/8.16 6[0:Inp] || -> equal(ordered_pair(skc8,skc9),ordered_pair(skc6,skc7))**. % 7.97/8.16 7[0:Inp] || -> equal(unordered_pair(u,v),unordered_pair(v,u))*. % 7.97/8.16 8[0:Inp] || equal(skc9,skc7)** equal(skc8,skc6) -> . % 7.97/8.16 9[0:Inp] || subset(singleton(u),singleton(v))* -> equal(u,v). % 7.97/8.16 10[0:Inp] || -> equal(unordered_pair(unordered_pair(u,v),singleton(u)),ordered_pair(u,v))**. % 7.97/8.16 12[0:Inp] || equal(singleton(u),unordered_pair(v,w))* -> equal(v,w). % 7.97/8.16 13[0:Inp] || equal(unordered_pair(u,v),unordered_pair(w,x))* -> equal(u,x) equal(u,w). % 7.97/8.16 14[0:Rew:7.0,10.0] || -> equal(unordered_pair(singleton(u),unordered_pair(u,v)),ordered_pair(u,v))**. % 7.97/8.16 25[0:SpR:14.0,14.0] || -> equal(unordered_pair(singleton(singleton(u)),ordered_pair(u,v)),ordered_pair(singleton(u),unordered_pair(u,v)))**. % 7.97/8.16 27[0:SpR:5.0,14.0] || -> equal(unordered_pair(singleton(u),singleton(u)),ordered_pair(u,u))**. % 7.97/8.16 28[0:SpR:7.0,14.0] || -> equal(unordered_pair(singleton(u),unordered_pair(v,u)),ordered_pair(u,v))**. % 7.97/8.16 30[0:Rew:5.0,27.0] || -> equal(ordered_pair(u,u),singleton(singleton(u)))**. % 7.97/8.16 36[0:SpL:14.0,12.0] || equal(singleton(u),ordered_pair(v,w))*+ -> equal(unordered_pair(v,w),singleton(v))**. % 7.97/8.16 43[0:SpL:7.0,13.0] || equal(unordered_pair(u,v),unordered_pair(w,x))* -> equal(v,x) equal(v,w). % 7.97/8.16 45[0:SpL:14.0,13.0] || equal(ordered_pair(u,v),unordered_pair(w,x))* -> equal(singleton(u),x) equal(singleton(u),w). % 7.97/8.16 53[0:SpR:28.0,14.0] || -> equal(unordered_pair(singleton(singleton(u)),ordered_pair(u,v)),ordered_pair(singleton(u),unordered_pair(v,u)))**. % 7.97/8.16 65[0:Rew:25.0,53.0] || -> equal(ordered_pair(singleton(u),unordered_pair(u,v)),ordered_pair(singleton(u),unordered_pair(v,u)))*. % 7.97/8.16 78[0:SpL:6.0,36.0] || equal(singleton(u),ordered_pair(skc6,skc7))* -> equal(unordered_pair(skc8,skc9),singleton(skc8))**. % 7.97/8.16 110[0:SpR:6.0,25.0] || -> equal(unordered_pair(singleton(singleton(skc8)),ordered_pair(skc6,skc7)),ordered_pair(singleton(skc8),unordered_pair(skc8,skc9)))**. % 7.97/8.16 144[0:SpL:14.0,43.0] || equal(unordered_pair(u,v),ordered_pair(w,x))*+ -> equal(v,unordered_pair(w,x))* equal(v,singleton(w)). % 7.97/8.16 201[0:SpL:14.0,45.0] || equal(ordered_pair(u,v),ordered_pair(w,x))*+ -> equal(singleton(u),unordered_pair(w,x))* equal(singleton(u),singleton(w)). % 7.97/8.16 204[0:SpL:110.0,45.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc8),unordered_pair(skc8,skc9)))* -> equal(singleton(u),ordered_pair(skc6,skc7)) equal(singleton(u),singleton(singleton(skc8))). % 7.97/8.16 329[0:SpL:28.0,144.0] || equal(ordered_pair(u,v),ordered_pair(w,x)) -> equal(unordered_pair(v,u),unordered_pair(w,x))* equal(unordered_pair(v,u),singleton(w)). % 7.97/8.16 579[0:SpL:6.0,201.0] || equal(ordered_pair(u,v),ordered_pair(skc6,skc7))* -> equal(singleton(u),unordered_pair(skc8,skc9))* equal(singleton(u),singleton(skc8)). % 7.97/8.16 581[0:SpL:65.0,201.0] || equal(ordered_pair(u,v),ordered_pair(singleton(w),unordered_pair(x,w)))* -> equal(singleton(u),unordered_pair(singleton(w),unordered_pair(w,x)))* equal(singleton(u),singleton(singleton(w))). % 7.97/8.16 582[0:Rew:14.0,581.1] || equal(ordered_pair(u,v),ordered_pair(singleton(w),unordered_pair(x,w)))* -> equal(singleton(u),ordered_pair(w,x)) equal(singleton(u),singleton(singleton(w))). % 7.97/8.16 584[0:EqR:579.0] || -> equal(unordered_pair(skc8,skc9),singleton(skc6))** equal(singleton(skc8),singleton(skc6)). % 7.97/8.16 589[1:Spt:584.1] || -> equal(singleton(skc8),singleton(skc6))**. % 7.97/8.16 689[1:SpL:589.0,9.0] || subset(singleton(skc6),singleton(u))* -> equal(skc8,u). % 7.97/8.16 705[1:Res:3.0,689.0] || -> equal(skc8,skc6)**. % 7.97/8.16 706[1:Rew:705.0,6.0] || -> equal(ordered_pair(skc6,skc9),ordered_pair(skc6,skc7))**. % 7.97/8.16 707[1:Rew:705.0,8.1] || equal(skc9,skc7)** equal(skc6,skc6) -> . % 7.97/8.16 746[1:Obv:707.1] || equal(skc9,skc7)** -> . % 7.97/8.16 1371[0:EqF:329.1,329.2] || equal(ordered_pair(u,v),ordered_pair(w,x))*+ equal(unordered_pair(w,x),singleton(w))** -> equal(unordered_pair(v,u),singleton(w))*. % 7.97/8.16 1380[0:SpR:329.1,7.0] || equal(ordered_pair(u,v),ordered_pair(w,x))+ -> equal(unordered_pair(v,u),singleton(w))* equal(unordered_pair(w,x),unordered_pair(u,v))*. % 7.97/8.16 1535[1:SpL:706.0,1371.0] || equal(ordered_pair(skc6,skc7),ordered_pair(u,v)) equal(unordered_pair(u,v),singleton(u))** -> equal(unordered_pair(skc9,skc6),singleton(u))*. % 7.97/8.16 1543[1:Rew:7.0,1535.2] || equal(ordered_pair(skc6,skc7),ordered_pair(u,v)) equal(unordered_pair(u,v),singleton(u))** -> equal(unordered_pair(skc6,skc9),singleton(u))*. % 7.97/8.16 1774[1:EqR:1543.0] || equal(unordered_pair(skc6,skc7),singleton(skc6)) -> equal(unordered_pair(skc6,skc9),singleton(skc6))**. % 7.97/8.16 1817[1:SpL:1774.1,12.0] || equal(unordered_pair(skc6,skc7),singleton(skc6))**+ equal(singleton(u),singleton(skc6))* -> equal(skc9,skc6). % 7.97/8.16 2951[1:SpL:706.0,1380.0] || equal(ordered_pair(u,v),ordered_pair(skc6,skc7)) -> equal(unordered_pair(v,u),singleton(skc6))** equal(unordered_pair(skc6,skc9),unordered_pair(u,v))*. % 7.97/8.16 3334[1:EqR:2951.0] || -> equal(unordered_pair(skc7,skc6),singleton(skc6))** equal(unordered_pair(skc6,skc9),unordered_pair(skc6,skc7)). % 7.97/8.16 3341[1:Rew:7.0,3334.0] || -> equal(unordered_pair(skc6,skc7),singleton(skc6)) equal(unordered_pair(skc6,skc9),unordered_pair(skc6,skc7))**. % 7.97/8.16 3426[2:Spt:3341.0] || -> equal(unordered_pair(skc6,skc7),singleton(skc6))**. % 7.97/8.16 3439[2:Rew:3426.0,1817.0] || equal(singleton(skc6),singleton(skc6))* equal(singleton(u),singleton(skc6))* -> equal(skc9,skc6). % 7.97/8.16 3922[2:Obv:3439.0] || equal(singleton(u),singleton(skc6))* -> equal(skc9,skc6). % 7.97/8.16 4663[2:SpL:3426.0,12.0] || equal(singleton(u),singleton(skc6))* -> equal(skc7,skc6). % 7.97/8.16 5103[2:EqR:3922.0] || -> equal(skc9,skc6)**. % 7.97/8.16 5104[2:Rew:5103.0,746.0] || equal(skc7,skc6)** -> . % 7.97/8.16 5204[2:MRR:4663.1,5104.0] || equal(singleton(u),singleton(skc6))* -> . % 7.97/8.16 5206[2:Obv:5204.0] || -> . % 7.97/8.16 5463[2:Spt:5206.0,3341.0,3426.0] || equal(unordered_pair(skc6,skc7),singleton(skc6))** -> . % 7.97/8.16 5464[2:Spt:5206.0,3341.1] || -> equal(unordered_pair(skc6,skc9),unordered_pair(skc6,skc7))**. % 7.97/8.16 5796[2:SpR:5464.0,28.0] || -> equal(unordered_pair(singleton(skc9),unordered_pair(skc6,skc7)),ordered_pair(skc9,skc6))**. % 7.97/8.16 5814[2:SpL:5464.0,43.0] || equal(unordered_pair(skc6,skc7),unordered_pair(u,v))* -> equal(skc9,v) equal(skc9,u). % 7.97/8.16 5983[2:SpL:5796.0,12.0] || equal(singleton(u),ordered_pair(skc9,skc6))*+ -> equal(unordered_pair(skc6,skc7),singleton(skc9))**. % 7.97/8.16 6064[2:SpL:5464.0,582.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc9),unordered_pair(skc6,skc7)))* -> equal(singleton(u),ordered_pair(skc9,skc6)) equal(singleton(u),singleton(singleton(skc9))). % 7.97/8.16 6069[2:EqR:5814.0] || -> equal(skc9,skc7)** equal(skc9,skc6). % 7.97/8.16 6100[2:MRR:6069.0,746.0] || -> equal(skc9,skc6)**. % 7.97/8.16 6104[2:Rew:6100.0,5983.0] || equal(singleton(u),ordered_pair(skc6,skc6))* -> equal(unordered_pair(skc6,skc7),singleton(skc9))**. % 7.97/8.16 6203[2:Rew:6100.0,6064.1] || equal(ordered_pair(u,v),ordered_pair(singleton(skc9),unordered_pair(skc6,skc7)))* -> equal(singleton(u),ordered_pair(skc6,skc6)) equal(singleton(u),singleton(singleton(skc9))). % 7.97/8.16 6291[2:Rew:30.0,6104.0] || equal(singleton(u),singleton(singleton(skc6)))* -> equal(unordered_pair(skc6,skc7),singleton(skc9))**. % 7.97/8.16 6292[2:Rew:6100.0,6291.1] || equal(singleton(u),singleton(singleton(skc6)))* -> equal(unordered_pair(skc6,skc7),singleton(skc6))**. % 7.97/8.16 6293[2:MRR:6292.1,5463.0] || equal(singleton(u),singleton(singleton(skc6)))* -> . % 7.97/8.16 6367[2:Rew:30.0,6203.1] || equal(ordered_pair(u,v),ordered_pair(singleton(skc9),unordered_pair(skc6,skc7)))* -> equal(singleton(u),singleton(singleton(skc6))) equal(singleton(u),singleton(singleton(skc9))). % 7.97/8.16 6368[2:Rew:6100.0,6367.2,6100.0,6367.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc6),unordered_pair(skc6,skc7)))* -> equal(singleton(u),singleton(singleton(skc6))) equal(singleton(u),singleton(singleton(skc6))). % 7.97/8.16 6369[2:Obv:6368.1] || equal(ordered_pair(u,v),ordered_pair(singleton(skc6),unordered_pair(skc6,skc7)))* -> equal(singleton(u),singleton(singleton(skc6))). % 8.02/8.19 6370[2:MRR:6369.1,6293.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc6),unordered_pair(skc6,skc7)))* -> . % 8.02/8.19 6371[2:UnC:6370.0,65.0] || -> . % 8.02/8.19 6617[1:Spt:6371.0,584.1,589.0] || equal(singleton(skc8),singleton(skc6))** -> . % 8.02/8.19 6618[1:Spt:6371.0,584.0] || -> equal(unordered_pair(skc8,skc9),singleton(skc6))**. % 8.02/8.19 6619[1:Rew:6618.0,78.1] || equal(singleton(u),ordered_pair(skc6,skc7))* -> equal(singleton(skc8),singleton(skc6)). % 8.02/8.19 6620[1:MRR:6619.1,6617.0] || equal(singleton(u),ordered_pair(skc6,skc7))* -> . % 8.02/8.19 6636[1:Rew:6618.0,204.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc8),singleton(skc6)))* -> equal(singleton(u),ordered_pair(skc6,skc7)) equal(singleton(u),singleton(singleton(skc8))). % 8.02/8.19 6637[1:MRR:6636.1,6620.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc8),singleton(skc6)))* -> equal(singleton(u),singleton(singleton(skc8))). % 8.02/8.19 6677[1:SpR:6618.0,28.0] || -> equal(unordered_pair(singleton(skc9),singleton(skc6)),ordered_pair(skc9,skc8))**. % 8.02/8.19 6708[1:SpL:6618.0,12.0] || equal(singleton(u),singleton(skc6))* -> equal(skc9,skc8). % 8.02/8.19 6732[1:Rew:7.0,6677.0] || -> equal(unordered_pair(singleton(skc6),singleton(skc9)),ordered_pair(skc9,skc8))**. % 8.02/8.19 6855[1:SpL:6732.0,12.0] || equal(singleton(u),ordered_pair(skc9,skc8))* -> equal(singleton(skc9),singleton(skc6)). % 8.02/8.19 6972[1:EqR:6708.0] || -> equal(skc9,skc8)**. % 8.02/8.19 6995[1:Rew:6972.0,6855.0] || equal(singleton(u),ordered_pair(skc8,skc8))* -> equal(singleton(skc9),singleton(skc6)). % 8.02/8.19 7040[1:Rew:30.0,6995.0] || equal(singleton(u),singleton(singleton(skc8)))* -> equal(singleton(skc9),singleton(skc6)). % 8.02/8.19 7041[1:Rew:6972.0,7040.1] || equal(singleton(u),singleton(singleton(skc8)))* -> equal(singleton(skc8),singleton(skc6)). % 8.02/8.19 7042[1:MRR:7041.1,6617.0] || equal(singleton(u),singleton(singleton(skc8)))* -> . % 8.02/8.19 7043[1:MRR:6637.1,7042.0] || equal(ordered_pair(u,v),ordered_pair(singleton(skc8),singleton(skc6)))* -> . % 8.02/8.19 7044[1:Obv:7043.0] || -> . % 8.02/8.19 % SZS output end Refutation % 8.02/8.19 Formulae used in the proof : reflexivity_r1_tarski t69_enumset1 t33_zfmisc_1 commutativity_k2_tarski t6_zfmisc_1 d5_tarski t9_zfmisc_1 t10_zfmisc_1 % 8.02/8.19 %------------------------------------------------------------------------------