%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET960+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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 05:30:04 EDT 2022 % Result : Theorem 0.18s 0.45s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET960+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n016.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 : Sun Jul 10 07:34:56 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.45 % 0.18/0.45 SPASS V 3.9 % 0.18/0.45 SPASS beiseite: Proof found. % 0.18/0.45 % SZS status Theorem % 0.18/0.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.45 SPASS derived 187 clauses, backtracked 20 clauses, performed 3 splits and kept 145 clauses. % 0.18/0.45 SPASS allocated 85299 KBytes. % 0.18/0.45 SPASS spent 0:00:00.11 on the problem. % 0.18/0.45 0:00:00.03 for the input. % 0.18/0.45 0:00:00.03 for the FLOTTER CNF translation. % 0.18/0.45 0:00:00.00 for inferences. % 0.18/0.45 0:00:00.00 for the backtracking. % 0.18/0.45 0:00:00.01 for the reduction. % 0.18/0.45 % 0.18/0.45 % 0.18/0.45 Here is a proof with depth 9, length 67 : % 0.18/0.45 % SZS output start Refutation % 0.18/0.45 6[0:Inp] || -> equal(u,empty_set) in(skf4(u),u)*. % 0.18/0.45 8[0:Inp] || in(u,v)* equal(v,empty_set) -> . % 0.18/0.45 9[0:Inp] || equal(empty_set,skc4) equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 10[0:Inp] || equal(empty_set,skc5) equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 12[0:Inp] || -> equal(empty_set,skc5) equal(empty_set,skc4) equal(cartesian_product2(skc4,skc5),empty_set)**. % 0.18/0.45 13[0:Inp] || SkP0(u,v,w)*+ -> in(skf7(w,x,y),w)*. % 0.18/0.45 14[0:Inp] || SkP0(u,v,w)*+ -> in(skf6(v,x,y),v)*. % 0.18/0.45 15[0:Inp] || in(u,v)* equal(v,cartesian_product2(w,x))*+ -> SkP0(u,x,w)*. % 0.18/0.45 16[0:Inp] || equal(u,cartesian_product2(v,w))*+ SkP0(x,w,v)* -> in(x,u)*. % 0.18/0.45 19[0:Inp] || -> equal(u,cartesian_product2(v,w)) in(skf5(v,w,u),u)* SkP0(skf5(v,w,u),w,v)*. % 0.18/0.45 20[0:Inp] || in(u,v)* in(w,x)* equal(y,ordered_pair(w,u))*+ -> SkP0(y,v,x)*. % 0.18/0.45 22[1:Spt:12.0] || -> equal(empty_set,skc5)**. % 0.18/0.45 23[1:Rew:22.0,6.0] || -> equal(u,skc5) in(skf4(u),u)*. % 0.18/0.45 24[1:Rew:22.0,10.0] || equal(skc5,skc5) equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 27[1:Rew:22.0,8.1] || in(u,v)* equal(v,skc5) -> . % 0.18/0.45 28[1:Obv:24.0] || equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 29[1:Rew:22.0,28.0] || equal(cartesian_product2(skc4,skc5),skc5)** -> . % 0.18/0.45 51[0:EqR:15.1] || in(u,cartesian_product2(v,w))* -> SkP0(u,w,v). % 0.18/0.45 52[1:Res:23.1,51.0] || -> equal(cartesian_product2(u,v),skc5) SkP0(skf4(cartesian_product2(u,v)),v,u)*. % 0.18/0.45 53[1:Res:52.1,13.0] || -> equal(cartesian_product2(u,v),skc5)** in(skf7(u,w,x),u)*. % 0.18/0.45 54[1:Res:52.1,14.0] || -> equal(cartesian_product2(u,v),skc5)** in(skf6(v,w,x),v)*. % 0.18/0.45 58[1:SpL:53.0,51.0] || in(u,skc5) -> in(skf7(v,w,x),v)* SkP0(u,y,v)*. % 0.18/0.45 62[1:MRR:58.2,13.0] || in(u,skc5)*+ -> in(skf7(v,w,x),v)*. % 0.18/0.45 70[0:EqR:16.0] || SkP0(u,v,w) -> in(u,cartesian_product2(w,v))*. % 0.18/0.45 75[1:Res:53.1,62.0] || -> equal(cartesian_product2(skc5,u),skc5)** in(skf7(v,w,x),v)*. % 0.18/0.45 81[2:Spt:75.1] || -> in(skf7(u,v,w),u)*. % 0.18/0.45 83[2:Res:81.0,27.0] || equal(u,skc5)* -> . % 0.18/0.45 85[2:Obv:83.0] || -> . % 0.18/0.45 86[2:Spt:85.0,75.0] || -> equal(cartesian_product2(skc5,u),skc5)**. % 0.18/0.45 92[2:SpL:86.0,51.0] || in(u,skc5) -> SkP0(u,v,skc5)*. % 0.18/0.45 93[2:SpL:86.0,16.0] || equal(u,skc5) SkP0(v,w,skc5)* -> in(v,u)*. % 0.18/0.45 94[2:MRR:93.2,27.0] || equal(u,skc5)* SkP0(v,w,skc5)*+ -> . % 0.18/0.45 100[2:Res:92.1,94.1] || in(u,skc5)* equal(v,skc5)* -> . % 0.18/0.45 102[2:AED:100.1] || in(u,skc5)* -> . % 0.18/0.45 120[2:Res:54.1,102.0] || -> equal(cartesian_product2(u,skc5),skc5)**. % 0.18/0.45 121[2:UnC:120.0,29.0] || -> . % 0.18/0.45 122[1:Spt:121.0,12.0,22.0] || equal(empty_set,skc5)** -> . % 0.18/0.45 123[1:Spt:121.0,12.1,12.2] || -> equal(empty_set,skc4) equal(cartesian_product2(skc4,skc5),empty_set)**. % 0.18/0.45 124[2:Spt:123.0] || -> equal(empty_set,skc4)**. % 0.18/0.45 127[2:Rew:124.0,6.0] || -> equal(u,skc4) in(skf4(u),u)*. % 0.18/0.45 128[2:Rew:124.0,8.1] || in(u,v)* equal(v,skc4) -> . % 0.18/0.45 129[2:Rew:124.0,9.0] || equal(skc4,skc4) equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 130[2:Obv:129.0] || equal(cartesian_product2(skc4,skc5),empty_set)** -> . % 0.18/0.45 131[2:Rew:124.0,130.0] || equal(cartesian_product2(skc4,skc5),skc4)** -> . % 0.18/0.45 134[2:Res:127.1,51.0] || -> equal(cartesian_product2(u,v),skc4) SkP0(skf4(cartesian_product2(u,v)),v,u)*. % 0.18/0.45 140[0:EqR:20.2] || in(u,v) in(w,x) -> SkP0(ordered_pair(w,u),v,x)*. % 0.18/0.45 144[2:Res:134.1,13.0] || -> equal(cartesian_product2(u,v),skc4)** in(skf7(u,w,x),u)*. % 0.18/0.45 154[2:Res:144.1,128.0] || equal(u,skc4) -> equal(cartesian_product2(u,v),skc4)**. % 0.18/0.45 167[2:SpL:154.1,131.0] || equal(skc4,skc4)* equal(skc4,skc4)* -> . % 0.18/0.45 168[2:Obv:167.1] || -> . % 0.18/0.45 170[2:Spt:168.0,123.0,124.0] || equal(empty_set,skc4)** -> . % 0.18/0.45 171[2:Spt:168.0,123.1] || -> equal(cartesian_product2(skc4,skc5),empty_set)**. % 0.18/0.45 172[2:SpR:171.0,70.1] || SkP0(u,skc5,skc4)* -> in(u,empty_set). % 0.18/0.45 175[2:SpL:171.0,51.0] || in(u,empty_set) -> SkP0(u,skc5,skc4)*. % 0.18/0.45 176[2:SpL:171.0,16.0] || equal(u,empty_set) SkP0(v,skc5,skc4)* -> in(v,u)*. % 0.18/0.45 178[2:MRR:176.2,8.0] || equal(u,empty_set)* SkP0(v,skc5,skc4)*+ -> . % 0.18/0.45 197[2:Res:19.2,172.0] || -> equal(u,cartesian_product2(skc4,skc5)) in(skf5(skc4,skc5,u),u)* in(skf5(skc4,skc5,u),empty_set)*. % 0.18/0.45 199[2:Rew:171.0,197.0] || -> equal(u,empty_set) in(skf5(skc4,skc5,u),u)* in(skf5(skc4,skc5,u),empty_set)*. % 0.18/0.45 201[2:Res:175.1,178.1] || in(u,empty_set)* equal(v,empty_set)* -> . % 0.18/0.45 203[2:AED:201.1] || in(u,empty_set)* -> . % 0.18/0.45 204[2:MRR:172.1,203.0] || SkP0(u,skc5,skc4)* -> . % 0.18/0.45 205[2:MRR:199.2,203.0] || -> equal(u,empty_set) in(skf5(skc4,skc5,u),u)*. % 0.18/0.45 236[2:Res:140.2,204.0] || in(u,skc5)*+ in(v,skc4)* -> . % 0.18/0.45 239[2:Res:6.1,236.0] || in(u,skc4)* -> equal(empty_set,skc5). % 0.18/0.45 241[2:MRR:239.1,122.0] || in(u,skc4)* -> . % 0.18/0.45 243[2:Res:205.1,241.0] || -> equal(empty_set,skc4)**. % 0.18/0.45 245[2:MRR:243.0,170.0] || -> . % 0.18/0.45 % SZS output end Refutation % 0.18/0.45 Formulae used in the proof : d1_xboole_0 t113_zfmisc_1 d2_zfmisc_1 antisymmetry_r2_hidden % 0.18/0.45 %------------------------------------------------------------------------------