%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU216+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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 1.97s 2.17s % Output : Refutation 1.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU216+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n025.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 07:00:58 EDT 2022 % 0.12/0.34 % CPUTime : % 1.97/2.17 % 1.97/2.17 SPASS V 3.9 % 1.97/2.17 SPASS beiseite: Proof found. % 1.97/2.17 % SZS status Theorem % 1.97/2.17 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.97/2.17 SPASS derived 5331 clauses, backtracked 251 clauses, performed 4 splits and kept 2095 clauses. % 1.97/2.17 SPASS allocated 104210 KBytes. % 1.97/2.17 SPASS spent 0:00:01.77 on the problem. % 1.97/2.17 0:00:00.03 for the input. % 1.97/2.17 0:00:00.04 for the FLOTTER CNF translation. % 1.97/2.17 0:00:00.09 for inferences. % 1.97/2.17 0:00:00.03 for the backtracking. % 1.97/2.17 0:00:01.54 for the reduction. % 1.97/2.17 % 1.97/2.17 % 1.97/2.17 Here is a proof with depth 4, length 73 : % 1.97/2.17 % SZS output start Refutation % 1.97/2.17 1[0:Inp] || -> function(skc9)*. % 1.97/2.17 2[0:Inp] || -> relation(skc9)*. % 1.97/2.17 18[0:Inp] || -> relation(identity_relation(u))*. % 1.97/2.17 19[0:Inp] || -> function(identity_relation(u))*. % 1.97/2.17 28[0:Inp] || -> equal(relation_dom(identity_relation(u)),u)**. % 1.97/2.17 38[0:Inp] || -> equal(identity_relation(skc10),skc9) equal(relation_dom(skc9),skc10)**. % 1.97/2.17 45[0:Inp] || in(u,skc10) -> equal(identity_relation(skc10),skc9) equal(apply(skc9,u),u)**. % 1.97/2.17 46[0:Inp] || equal(relation_dom(skc9),skc10) equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 1.97/2.17 47[0:Inp] || equal(relation_dom(skc9),skc10) equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 48[0:Inp] function(u) relation(u) || in(ordered_pair(v,w),u)* -> in(v,relation_dom(u)). % 1.97/2.17 51[0:Inp] function(u) relation(u) || in(ordered_pair(v,w),u)* -> equal(w,apply(u,v)). % 1.97/2.17 54[0:Inp] relation(u) || -> equal(u,identity_relation(v)) in(skf3(v,u),v) in(ordered_pair(skf3(v,u),skf4(v,u)),u)*. % 1.97/2.17 55[0:Inp] relation(u) || equal(v,w) in(v,x)* equal(u,identity_relation(x))*+ -> in(ordered_pair(v,w),u)*. % 1.97/2.17 56[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) equal(w,apply(u,v)) -> in(ordered_pair(v,w),u)*. % 1.97/2.17 59[0:Inp] relation(u) || -> equal(u,identity_relation(v)) equal(skf4(v,u),skf3(v,u)) in(ordered_pair(skf3(v,u),skf4(v,u)),u)*. % 1.97/2.17 60[0:Inp] || in(skf3(u,v),u) equal(skf4(u,v),skf3(u,v)) in(ordered_pair(skf3(u,v),skf4(u,v)),v)* -> . % 1.97/2.17 63[0:Res:2.0,56.0] function(skc9) || equal(u,apply(skc9,v)) in(v,relation_dom(skc9)) -> in(ordered_pair(v,u),skc9)*. % 1.97/2.17 71[0:Res:2.0,48.0] function(skc9) || in(ordered_pair(u,v),skc9)* -> in(u,relation_dom(skc9)). % 1.97/2.17 79[0:MRR:71.0,1.0] || in(ordered_pair(u,v),skc9)* -> in(u,relation_dom(skc9)). % 1.97/2.17 83[0:MRR:63.0,1.0] || in(u,relation_dom(skc9)) equal(v,apply(skc9,u)) -> in(ordered_pair(u,v),skc9)*. % 1.97/2.17 84[1:Spt:38.1] || -> equal(relation_dom(skc9),skc10)**. % 1.97/2.17 85[1:Rew:84.0,47.0] || equal(skc10,skc10) equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 86[1:Rew:84.0,46.0] || equal(skc10,skc10) equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 1.97/2.17 90[1:Rew:84.0,83.0] || in(u,skc10) equal(v,apply(skc9,u)) -> in(ordered_pair(u,v),skc9)*. % 1.97/2.17 91[1:Rew:84.0,79.1] || in(ordered_pair(u,v),skc9)* -> in(u,skc10). % 1.97/2.17 92[1:Obv:86.0] || equal(identity_relation(skc10),skc9) -> in(skc11,skc10)*. % 1.97/2.17 93[1:Obv:85.0] || equal(identity_relation(skc10),skc9) equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 95[2:Spt:45.0,45.2] || in(u,skc10) -> equal(apply(skc9,u),u)**. % 1.97/2.17 96[2:Rew:95.1,90.1] || in(u,skc10) equal(v,u) -> in(ordered_pair(u,v),skc9)*. % 1.97/2.17 187[3:Spt:93.0] || equal(identity_relation(skc10),skc9)** -> . % 1.97/2.17 287[0:EqR:55.3] relation(identity_relation(u)) || equal(v,w) in(v,u) -> in(ordered_pair(v,w),identity_relation(u))*. % 1.97/2.17 289[0:SSi:287.0,19.0,18.0] || equal(u,v) in(u,w) -> in(ordered_pair(u,v),identity_relation(w))*. % 1.97/2.17 296[0:Res:289.2,51.2] function(identity_relation(u)) relation(identity_relation(u)) || equal(v,w) in(v,u) -> equal(w,apply(identity_relation(u),v))*. % 1.97/2.17 305[0:SSi:296.1,296.0,19.0,18.0,19.0,18.0] || equal(u,v) in(u,w) -> equal(v,apply(identity_relation(w),u))*. % 1.97/2.17 316[1:Res:54.3,91.0] relation(skc9) || -> equal(identity_relation(u),skc9) in(skf3(u,skc9),u)* in(skf3(u,skc9),skc10)*. % 1.97/2.17 320[1:SSi:316.0,1.0,2.0] || -> equal(identity_relation(u),skc9) in(skf3(u,skc9),u)* in(skf3(u,skc9),skc10)*. % 1.97/2.17 593[0:Res:59.3,51.2] relation(u) function(u) relation(u) || -> equal(u,identity_relation(v)) equal(skf4(v,u),skf3(v,u)) equal(apply(u,skf3(v,u)),skf4(v,u))**. % 1.97/2.17 598[1:Res:59.3,91.0] relation(skc9) || -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9)) in(skf3(u,skc9),skc10)*. % 1.97/2.17 603[1:SSi:598.0,1.0,2.0] || -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9)) in(skf3(u,skc9),skc10)*. % 1.97/2.17 611[0:Obv:593.0] function(u) relation(u) || -> equal(u,identity_relation(v)) equal(skf4(v,u),skf3(v,u)) equal(apply(u,skf3(v,u)),skf4(v,u))**. % 1.97/2.17 658[2:Res:96.2,60.2] || in(skf3(u,skc9),skc10)* equal(skf4(u,skc9),skf3(u,skc9)) in(skf3(u,skc9),u)* equal(skf4(u,skc9),skf3(u,skc9)) -> . % 1.97/2.17 663[2:Obv:658.1] || in(skf3(u,skc9),skc10)* in(skf3(u,skc9),u)* equal(skf4(u,skc9),skf3(u,skc9))+ -> . % 1.97/2.17 1461[2:SpR:611.4,95.1] function(skc9) relation(skc9) || in(skf3(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9)) equal(skf4(u,skc9),skf3(u,skc9)). % 1.97/2.17 1469[2:Obv:1461.4] function(skc9) relation(skc9) || in(skf3(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9)). % 1.97/2.17 1470[2:SSi:1469.1,1469.0,1.0,2.0,1.0,2.0] || in(skf3(u,skc9),skc10)* -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9)). % 1.97/2.17 1471[2:MRR:1470.0,603.2] || -> equal(identity_relation(u),skc9) equal(skf4(u,skc9),skf3(u,skc9))**. % 1.97/2.17 1533[1:Fac:320.1,320.2] || -> equal(identity_relation(skc10),skc9) in(skf3(skc10,skc9),skc10)*. % 1.97/2.17 1547[3:MRR:1533.0,187.0] || -> in(skf3(skc10,skc9),skc10)*. % 1.97/2.17 2713[2:SpL:1471.1,663.2] || in(skf3(u,skc9),skc10)* in(skf3(u,skc9),u)* equal(skf3(u,skc9),skf3(u,skc9)) -> equal(identity_relation(u),skc9). % 1.97/2.17 2716[2:Obv:2713.2] || in(skf3(u,skc9),skc10)*+ in(skf3(u,skc9),u)* -> equal(identity_relation(u),skc9). % 1.97/2.17 5314[3:Res:1547.0,2716.0] || in(skf3(skc10,skc9),skc10)* -> equal(identity_relation(skc10),skc9). % 1.97/2.17 5317[3:MRR:5314.0,5314.1,1547.0,187.0] || -> . % 1.97/2.17 5325[3:Spt:5317.0,93.0,187.0] || -> equal(identity_relation(skc10),skc9)**. % 1.97/2.17 5326[3:Spt:5317.0,93.1] || equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 5328[3:Rew:5325.0,92.0] || equal(skc9,skc9) -> in(skc11,skc10)*. % 1.97/2.17 5329[3:Obv:5328.0] || -> in(skc11,skc10)*. % 1.97/2.17 5401[3:SpL:95.1,5326.0] || in(skc11,skc10)* equal(skc11,skc11) -> . % 1.97/2.17 5408[3:Obv:5401.1] || in(skc11,skc10)* -> . % 1.97/2.17 5409[3:MRR:5408.0,5329.0] || -> . % 1.97/2.17 5412[2:Spt:5409.0,45.1] || -> equal(identity_relation(skc10),skc9)**. % 1.97/2.17 5416[2:Rew:5412.0,92.0] || equal(skc9,skc9) -> in(skc11,skc10)*. % 1.97/2.17 5417[2:Obv:5416.0] || -> in(skc11,skc10)*. % 1.97/2.17 5422[2:Rew:5412.0,93.0] || equal(skc9,skc9) equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 5423[2:Obv:5422.0] || equal(apply(skc9,skc11),skc11)** -> . % 1.97/2.17 5473[2:SpR:5412.0,305.2] || equal(u,v) in(u,skc10) -> equal(v,apply(skc9,u))*. % 1.97/2.17 7046[2:SpL:5473.2,5423.0] || equal(skc11,u)* in(skc11,skc10)* equal(u,skc11)* -> . % 1.97/2.17 7047[2:Obv:7046.0] || in(skc11,skc10)* equal(u,skc11)* -> . % 1.97/2.17 7048[2:AED:7047.1] || in(skc11,skc10)* -> . % 1.97/2.17 7049[2:MRR:7048.0,5417.0] || -> . % 1.97/2.17 7113[1:Spt:7049.0,38.1,84.0] || equal(relation_dom(skc9),skc10)** -> . % 1.97/2.17 7114[1:Spt:7049.0,38.0] || -> equal(identity_relation(skc10),skc9)**. % 1.97/2.17 7121[1:SpR:7114.0,28.0] || -> equal(relation_dom(skc9),skc10)**. % 1.97/2.17 7193[1:MRR:7121.0,7113.0] || -> . % 1.97/2.17 % SZS output end Refutation % 1.97/2.17 Formulae used in the proof : t34_funct_1 fc2_funct_1 t71_relat_1 t8_funct_1 d10_relat_1 antisymmetry_r2_hidden % 1.97/2.17 %------------------------------------------------------------------------------