%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET997+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:18 EDT 2022 % Result : Theorem 0.47s 0.66s % Output : Refutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SET997+1 : TPTP v8.1.0. Released v3.2.0. % 0.12/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n013.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 : Sat Jul 9 19:07:14 EDT 2022 % 0.18/0.33 % CPUTime : % 0.47/0.66 % 0.47/0.66 SPASS V 3.9 % 0.47/0.66 SPASS beiseite: Proof found. % 0.47/0.66 % SZS status Theorem % 0.47/0.66 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.47/0.66 SPASS derived 1840 clauses, backtracked 61 clauses, performed 5 splits and kept 849 clauses. % 0.47/0.66 SPASS allocated 99239 KBytes. % 0.47/0.66 SPASS spent 0:00:00.31 on the problem. % 0.47/0.66 0:00:00.04 for the input. % 0.47/0.66 0:00:00.05 for the FLOTTER CNF translation. % 0.47/0.66 0:00:00.02 for inferences. % 0.47/0.66 0:00:00.00 for the backtracking. % 0.47/0.66 0:00:00.16 for the reduction. % 0.47/0.66 % 0.47/0.66 % 0.47/0.66 Here is a proof with depth 6, length 54 : % 0.47/0.66 % SZS output start Refutation % 0.47/0.66 1[0:Inp] || -> function(skc8)*. % 0.47/0.66 2[0:Inp] || -> relation(skc8)*. % 0.47/0.66 5[0:Inp] || -> relation_empty_yielding(empty_set)*. % 0.47/0.66 7[0:Inp] || -> empty(empty_set)*. % 0.47/0.66 8[0:Inp] || -> relation(empty_set)*. % 0.47/0.66 23[0:Inp] || subset(skc9,relation_rng(skc8))* -> . % 0.47/0.66 28[0:Inp] empty(u) || -> empty(relation_dom(u))*. % 0.47/0.66 30[0:Inp] empty(u) || -> empty(relation_rng(u))*. % 0.47/0.66 33[0:Inp] empty(u) || -> equal(u,empty_set)*. % 0.47/0.66 35[0:Inp] empty(u) || in(v,u)* -> . % 0.47/0.66 37[0:Inp] || -> subset(u,v) in(skf9(v,u),u)*. % 0.47/0.66 40[0:Inp] || in(u,skc9)*+ -> in(skf8(v),relation_dom(skc8))*. % 0.47/0.66 41[0:Inp] || in(skf9(u,v),u)*+ -> subset(w,u)*. % 0.47/0.66 43[0:Inp] relation(u) || empty(relation_rng(u))* -> empty(u). % 0.47/0.66 46[0:Inp] || in(u,skc9) -> equal(apply(skc8,skf8(u)),u)**. % 0.47/0.66 50[0:Inp] function(u) relation(u) || -> equal(v,relation_rng(u)) in(skf12(u,v),v)* in(skf13(u,w),relation_dom(u))*. % 0.47/0.66 54[0:Inp] function(u) relation(u) || in(v,relation_dom(u))* equal(w,relation_rng(u))* equal(x,apply(u,v))*+ -> in(x,w)*. % 0.47/0.66 61[0:Res:2.0,50.0] function(skc8) || -> in(skf13(skc8,u),relation_dom(skc8))* in(skf12(skc8,v),v)* equal(v,relation_rng(skc8)). % 0.47/0.66 63[0:Res:2.0,43.0] || empty(relation_rng(skc8))* -> empty(skc8). % 0.47/0.66 74[0:MRR:61.0,1.0] || -> equal(u,relation_rng(skc8)) in(skf12(skc8,u),u)* in(skf13(skc8,v),relation_dom(skc8))*. % 0.47/0.66 79[1:Spt:74.0,74.1] || -> equal(u,relation_rng(skc8)) in(skf12(skc8,u),u)*. % 0.47/0.66 93[0:EmS:33.0,30.1] empty(u) || -> equal(relation_rng(u),empty_set)**. % 0.47/0.66 97[0:EmS:33.0,28.1] empty(u) || -> equal(relation_dom(u),empty_set)**. % 0.47/0.66 102[0:SpL:93.1,23.0] empty(skc8) || subset(skc9,empty_set)* -> . % 0.47/0.66 106[1:Res:79.1,35.1] empty(u) || -> equal(u,relation_rng(skc8))*. % 0.47/0.66 124[1:SpL:106.1,63.0] empty(u) || empty(u)* -> empty(skc8)*. % 0.47/0.66 125[1:Obv:124.0] || empty(u)*+ -> empty(skc8)*. % 0.47/0.66 129[1:Res:7.0,125.0] || -> empty(skc8)*. % 0.47/0.66 130[1:MRR:102.0,129.0] || subset(skc9,empty_set)* -> . % 0.47/0.66 131[1:EmS:33.0,129.0] || -> equal(skc8,empty_set)**. % 0.47/0.66 135[1:Rew:131.0,1.0] || -> function(empty_set)*. % 0.47/0.66 152[1:Rew:131.0,40.1] || in(u,skc9)*+ -> in(skf8(v),relation_dom(empty_set))*. % 0.47/0.66 192[1:Res:37.1,152.0] || -> subset(skc9,u)* in(skf8(v),relation_dom(empty_set))*. % 0.47/0.66 197[2:Spt:192.0] || -> subset(skc9,u)*. % 0.47/0.66 198[2:UnC:197.0,130.0] || -> . % 0.47/0.66 199[2:Spt:198.0,192.1] || -> in(skf8(u),relation_dom(empty_set))*. % 0.47/0.66 201[2:SpR:97.1,199.0] empty(empty_set) || -> in(skf8(u),empty_set)*. % 0.47/0.66 205[2:SSi:201.0,5.0,8.0,7.0,135.0] || -> in(skf8(u),empty_set)*. % 0.47/0.66 207[2:Res:205.0,35.1] empty(empty_set) || -> . % 0.47/0.66 209[2:SSi:207.0,5.0,8.0,7.0,135.0] || -> . % 0.47/0.66 210[1:Spt:209.0,74.2] || -> in(skf13(skc8,u),relation_dom(skc8))*. % 0.47/0.66 216[0:Res:37.1,40.0] || -> subset(skc9,u)* in(skf8(v),relation_dom(skc8))*. % 0.47/0.66 221[2:Spt:216.0] || -> subset(skc9,u)*. % 0.47/0.66 222[2:UnC:221.0,23.0] || -> . % 0.47/0.66 223[2:Spt:222.0,216.1] || -> in(skf8(u),relation_dom(skc8))*. % 0.47/0.66 401[0:EqR:54.4] function(u) relation(u) || in(v,relation_dom(u)) equal(w,relation_rng(u)) -> in(apply(u,v),w)*. % 0.47/0.66 1090[0:SpR:46.1,401.4] function(skc8) relation(skc8) || in(u,skc9) in(skf8(u),relation_dom(skc8))* equal(v,relation_rng(skc8)) -> in(u,v)*. % 0.47/0.66 1110[0:SSi:1090.1,1090.0,2.0,1.0,2.0,1.0] || in(u,skc9) in(skf8(u),relation_dom(skc8))* equal(v,relation_rng(skc8)) -> in(u,v)*. % 0.47/0.66 1111[2:MRR:1110.1,223.0] || in(u,skc9)* equal(v,relation_rng(skc8))+ -> in(u,v)*. % 0.47/0.66 1697[2:EqR:1111.1] || in(u,skc9) -> in(u,relation_rng(skc8))*. % 0.47/0.66 1701[2:Res:1697.1,41.0] || in(skf9(relation_rng(skc8),u),skc9)*+ -> subset(v,relation_rng(skc8))*. % 0.47/0.66 2232[2:Res:37.1,1701.0] || -> subset(skc9,relation_rng(skc8))* subset(u,relation_rng(skc8))*. % 0.47/0.66 2234[2:Con:2232.1] || -> subset(skc9,relation_rng(skc8))*. % 0.47/0.66 2235[2:MRR:2234.0,23.0] || -> . % 0.47/0.66 % SZS output end Refutation % 0.47/0.66 Formulae used in the proof : t19_funct_1 fc12_relat_1 fc4_relat_1 fc7_relat_1 fc8_relat_1 t6_boole t7_boole d3_tarski fc6_relat_1 d5_funct_1 % 0.47/0.66 %------------------------------------------------------------------------------