%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU216+3 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:35:06 EDT 2022 % Result : Theorem 7.27s 7.44s % Output : Refutation 7.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU216+3 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n018.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 Jun 19 17:44:04 EDT 2022 % 0.12/0.33 % CPUTime : % 7.27/7.44 % 7.27/7.44 SPASS V 3.9 % 7.27/7.44 SPASS beiseite: Proof found. % 7.27/7.44 % SZS status Theorem % 7.27/7.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 7.27/7.44 SPASS derived 10752 clauses, backtracked 266 clauses, performed 5 splits and kept 5429 clauses. % 7.27/7.44 SPASS allocated 110100 KBytes. % 7.27/7.44 SPASS spent 0:00:06.90 on the problem. % 7.27/7.44 0:00:00.04 for the input. % 7.27/7.44 0:00:00.04 for the FLOTTER CNF translation. % 7.27/7.44 0:00:00.16 for inferences. % 7.27/7.44 0:00:00.20 for the backtracking. % 7.27/7.44 0:00:06.38 for the reduction. % 7.27/7.44 % 7.27/7.44 % 7.27/7.44 Here is a proof with depth 4, length 73 : % 7.27/7.44 % SZS output start Refutation % 7.27/7.44 1[0:Inp] || -> function(skc9)*. % 7.27/7.44 2[0:Inp] || -> relation(skc9)*. % 7.27/7.44 18[0:Inp] || -> relation(identity_relation(u))*. % 7.27/7.44 19[0:Inp] || -> function(identity_relation(u))*. % 7.27/7.44 33[0:Inp] || -> equal(relation_dom(identity_relation(u)),u)**. % 7.27/7.44 44[0:Inp] || -> equal(identity_relation(skc10),skc9) equal(relation_dom(skc9),skc10)**. % 7.27/7.44 55[0:Inp] || in(u,skc10) -> equal(identity_relation(skc10),skc9) equal(apply(skc9,u),u)**. % 7.27/7.44 56[0:Inp] || equal(relation_dom(skc9),skc10) equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 7.27/7.44 57[0:Inp] || equal(relation_dom(skc9),skc10) equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 58[0:Inp] function(u) relation(u) || in(ordered_pair(v,w),u)* -> in(v,relation_dom(u)). % 7.27/7.44 61[0:Inp] function(u) relation(u) || in(ordered_pair(v,w),u)* -> equal(w,apply(u,v)). % 7.27/7.44 64[0:Inp] relation(u) || -> equal(u,identity_relation(v)) in(skf5(v,u),v) in(ordered_pair(skf5(v,u),skf6(v,u)),u)*. % 7.27/7.44 65[0:Inp] relation(u) || equal(v,w) in(v,x)* equal(u,identity_relation(x))*+ -> in(ordered_pair(v,w),u)*. % 7.27/7.44 66[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) equal(w,apply(u,v)) -> in(ordered_pair(v,w),u)*. % 7.27/7.44 69[0:Inp] relation(u) || -> equal(u,identity_relation(v)) equal(skf6(v,u),skf5(v,u)) in(ordered_pair(skf5(v,u),skf6(v,u)),u)*. % 7.27/7.44 70[0:Inp] || in(skf5(u,v),u) equal(skf6(u,v),skf5(u,v)) in(ordered_pair(skf5(u,v),skf6(u,v)),v)* -> . % 7.27/7.44 73[0:Res:2.0,66.0] function(skc9) || equal(u,apply(skc9,v)) in(v,relation_dom(skc9)) -> in(ordered_pair(v,u),skc9)*. % 7.27/7.44 81[0:Res:2.0,58.0] function(skc9) || in(ordered_pair(u,v),skc9)* -> in(u,relation_dom(skc9)). % 7.27/7.44 89[0:MRR:81.0,1.0] || in(ordered_pair(u,v),skc9)* -> in(u,relation_dom(skc9)). % 7.27/7.44 93[0:MRR:73.0,1.0] || in(u,relation_dom(skc9)) equal(v,apply(skc9,u)) -> in(ordered_pair(u,v),skc9)*. % 7.27/7.44 94[1:Spt:44.1] || -> equal(relation_dom(skc9),skc10)**. % 7.27/7.44 95[1:Rew:94.0,57.0] || equal(skc10,skc10) equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 96[1:Rew:94.0,56.0] || equal(skc10,skc10) equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 7.27/7.44 100[1:Rew:94.0,93.0] || in(u,skc10) equal(v,apply(skc9,u)) -> in(ordered_pair(u,v),skc9)*. % 7.27/7.44 101[1:Rew:94.0,89.1] || in(ordered_pair(u,v),skc9)* -> in(u,skc10). % 7.27/7.44 102[1:Obv:96.0] || equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 7.27/7.44 103[1:Obv:95.0] || equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 105[2:Spt:55.0,55.2] || in(u,skc10) -> equal(apply(skc9,u),u)**. % 7.27/7.44 106[2:Rew:105.1,100.1] || in(u,skc10) equal(v,u) -> in(ordered_pair(u,v),skc9)*. % 7.27/7.44 207[3:Spt:103.0] || equal(identity_relation(skc10),skc9)** -> . % 7.27/7.44 340[0:EqR:65.3] relation(identity_relation(u)) || equal(v,w) in(v,u) -> in(ordered_pair(v,w),identity_relation(u))*. % 7.27/7.44 342[0:SSi:340.0,19.0,18.0] || equal(u,v) in(u,w) -> in(ordered_pair(u,v),identity_relation(w))*. % 7.27/7.44 365[1:Res:64.3,101.0] relation(skc9) || -> equal(identity_relation(u),skc9) in(skf5(u,skc9),u)* in(skf5(u,skc9),skc10)*. % 7.27/7.44 368[1:SSi:365.0,1.0,2.0] || -> equal(identity_relation(u),skc9) in(skf5(u,skc9),u)* in(skf5(u,skc9),skc10)*. % 7.27/7.44 439[0:Res:69.3,61.2] relation(u) function(u) relation(u) || -> equal(u,identity_relation(v)) equal(skf6(v,u),skf5(v,u)) equal(apply(u,skf5(v,u)),skf6(v,u))**. % 7.27/7.44 443[1:Res:69.3,101.0] relation(skc9) || -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9)) in(skf5(u,skc9),skc10)*. % 7.27/7.44 446[1:SSi:443.0,1.0,2.0] || -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9)) in(skf5(u,skc9),skc10)*. % 7.27/7.44 450[0:Obv:439.0] function(u) relation(u) || -> equal(u,identity_relation(v)) equal(skf6(v,u),skf5(v,u)) equal(apply(u,skf5(v,u)),skf6(v,u))**. % 7.27/7.44 701[2:Res:106.2,70.2] || in(skf5(u,skc9),skc10)* equal(skf6(u,skc9),skf5(u,skc9)) in(skf5(u,skc9),u)* equal(skf6(u,skc9),skf5(u,skc9)) -> . % 7.27/7.44 711[2:Obv:701.1] || in(skf5(u,skc9),skc10)* in(skf5(u,skc9),u)* equal(skf6(u,skc9),skf5(u,skc9))+ -> . % 7.27/7.44 849[0:Res:342.2,61.2] function(identity_relation(u)) relation(identity_relation(u)) || equal(v,w) in(v,u) -> equal(w,apply(identity_relation(u),v))*. % 7.27/7.44 860[0:SSi:849.1,849.0,19.0,18.0,19.0,18.0] || equal(u,v) in(u,w) -> equal(v,apply(identity_relation(w),u))*. % 7.27/7.44 1597[2:SpR:450.4,105.1] function(skc9) relation(skc9) || in(skf5(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9)) equal(skf6(u,skc9),skf5(u,skc9)). % 7.27/7.44 1605[2:Obv:1597.4] function(skc9) relation(skc9) || in(skf5(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9)). % 7.27/7.44 1606[2:SSi:1605.1,1605.0,1.0,2.0,1.0,2.0] || in(skf5(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9)). % 7.27/7.44 1607[2:MRR:1606.0,446.2] || -> equal(identity_relation(u),skc9) equal(skf6(u,skc9),skf5(u,skc9))**. % 7.27/7.44 1822[1:Fac:368.1,368.2] || -> equal(identity_relation(skc10),skc9) in(skf5(skc10,skc9),skc10)*. % 7.27/7.44 1846[3:MRR:1822.0,207.0] || -> in(skf5(skc10,skc9),skc10)*. % 7.27/7.44 4009[2:SpL:1607.1,711.2] || in(skf5(u,skc9),skc10)* in(skf5(u,skc9),u)* equal(skf5(u,skc9),skf5(u,skc9)) -> equal(identity_relation(u),skc9). % 7.27/7.44 4014[2:Obv:4009.2] || in(skf5(u,skc9),skc10)*+ in(skf5(u,skc9),u)* -> equal(identity_relation(u),skc9). % 7.27/7.44 10575[3:Res:1846.0,4014.0] || in(skf5(skc10,skc9),skc10)* -> equal(identity_relation(skc10),skc9). % 7.27/7.44 10577[3:MRR:10575.0,10575.1,1846.0,207.0] || -> . % 7.27/7.44 10585[3:Spt:10577.0,103.0,207.0] || -> equal(identity_relation(skc10),skc9)**. % 7.27/7.44 10586[3:Spt:10577.0,103.1] || equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 10589[3:Rew:10585.0,102.0] || equal(skc9,skc9) -> in(skc11,skc10)*. % 7.27/7.44 10590[3:Obv:10589.0] || -> in(skc11,skc10)*. % 7.27/7.44 10690[3:SpL:105.1,10586.0] || in(skc11,skc10)* equal(skc11,skc11) -> . % 7.27/7.44 10695[3:Obv:10690.1] || in(skc11,skc10)* -> . % 7.27/7.44 10696[3:MRR:10695.0,10590.0] || -> . % 7.27/7.44 10698[2:Spt:10696.0,55.1] || -> equal(identity_relation(skc10),skc9)**. % 7.27/7.44 10701[2:Rew:10698.0,102.0] || equal(skc9,skc9) -> in(skc11,skc10)*. % 7.27/7.44 10702[2:Obv:10701.0] || -> in(skc11,skc10)*. % 7.27/7.44 10706[2:Rew:10698.0,103.0] || equal(skc9,skc9) equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 10707[2:Obv:10706.0] || equal(apply(skc9,skc11),skc11)** -> . % 7.27/7.44 10748[2:SpR:10698.0,860.2] || equal(u,v) in(u,skc10) -> equal(v,apply(skc9,u))*. % 7.27/7.44 13099[2:SpL:10748.2,10707.0] || equal(skc11,u)* in(skc11,skc10)* equal(u,skc11)* -> . % 7.27/7.44 13103[2:Obv:13099.0] || in(skc11,skc10)* equal(u,skc11)* -> . % 7.27/7.44 13104[2:AED:13103.1] || in(skc11,skc10)* -> . % 7.27/7.44 13105[2:MRR:13104.0,10702.0] || -> . % 7.27/7.44 13195[1:Spt:13105.0,44.1,94.0] || equal(relation_dom(skc9),skc10)** -> . % 7.27/7.44 13196[1:Spt:13105.0,44.0] || -> equal(identity_relation(skc10),skc9)**. % 7.27/7.44 13200[1:SpR:13196.0,33.0] || -> equal(relation_dom(skc9),skc10)**. % 7.27/7.44 13273[1:MRR:13200.0,13195.0] || -> . % 7.27/7.44 % SZS output end Refutation % 7.27/7.44 Formulae used in the proof : t34_funct_1 fc2_funct_1 t71_relat_1 t8_funct_1 d10_relat_1 antisymmetry_r2_hidden % 7.27/7.44 %------------------------------------------------------------------------------