%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU234+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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:21 EDT 2022 % Result : Theorem 0.18s 0.49s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SEU234+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n021.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 19:15:33 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.49 % 0.18/0.49 SPASS V 3.9 % 0.18/0.49 SPASS beiseite: Proof found. % 0.18/0.49 % SZS status Theorem % 0.18/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.49 SPASS derived 498 clauses, backtracked 109 clauses, performed 12 splits and kept 378 clauses. % 0.18/0.49 SPASS allocated 98134 KBytes. % 0.18/0.49 SPASS spent 0:00:00.15 on the problem. % 0.18/0.49 0:00:00.03 for the input. % 0.18/0.49 0:00:00.04 for the FLOTTER CNF translation. % 0.18/0.49 0:00:00.01 for inferences. % 0.18/0.49 0:00:00.00 for the backtracking. % 0.18/0.49 0:00:00.04 for the reduction. % 0.18/0.49 % 0.18/0.49 % 0.18/0.49 Here is a proof with depth 8, length 112 : % 0.18/0.49 % SZS output start Refutation % 0.18/0.49 6[0:Inp] || -> relation_empty_yielding(empty_set)*. % 0.18/0.49 7[0:Inp] || -> function(empty_set)*. % 0.18/0.49 8[0:Inp] || -> one_to_one(empty_set)*. % 0.18/0.49 10[0:Inp] || -> epsilon_transitive(empty_set)*. % 0.18/0.49 11[0:Inp] || -> epsilon_connected(empty_set)*. % 0.18/0.49 12[0:Inp] || -> ordinal(empty_set)*. % 0.18/0.49 13[0:Inp] || -> empty(empty_set)*. % 0.18/0.49 14[0:Inp] || -> relation(empty_set)*. % 0.18/0.49 45[0:Inp] || ordinal(skc13)* -> . % 0.18/0.49 50[0:Inp] || -> element(skf7(u),u)*. % 0.18/0.49 57[0:Inp] empty(u) || -> ordinal(u)*. % 0.18/0.49 59[0:Inp] ordinal(u) || -> epsilon_connected(u)*. % 0.18/0.49 60[0:Inp] || in(u,skc13)* -> ordinal(u). % 0.18/0.49 61[0:Inp] || -> epsilon_transitive(u) in(skf4(u),u)*. % 0.18/0.49 62[0:Inp] || in(skf6(u),skf5(u))* -> . % 0.18/0.49 63[0:Inp] || -> epsilon_connected(u) in(skf6(u),u)*. % 0.18/0.49 64[0:Inp] || -> epsilon_connected(u) in(skf5(u),u)*. % 0.18/0.49 65[0:Inp] empty(u) || -> equal(u,empty_set)*. % 0.18/0.49 66[0:Inp] || in(u,skc13) -> subset(u,skc13)*. % 0.18/0.49 67[0:Inp] || subset(skf4(u),u)* -> epsilon_transitive(u). % 0.18/0.49 69[0:Inp] empty(u) || in(v,u)* -> . % 0.18/0.49 72[0:Inp] || equal(skf6(u),skf5(u))** -> epsilon_connected(u). % 0.18/0.49 73[0:Inp] || in(skf5(u),skf6(u))* -> epsilon_connected(u). % 0.18/0.49 74[0:Inp] epsilon_connected(u) epsilon_transitive(u) || -> ordinal(u)*. % 0.18/0.49 76[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 0.18/0.49 77[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 0.18/0.49 81[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 0.18/0.49 82[0:Inp] empty(u) || in(v,w)* element(w,powerset(u))*+ -> . % 0.18/0.49 83[0:Inp] ordinal(u) ordinal(v) || -> in(u,v)* equal(v,u) in(v,u)*. % 0.18/0.49 86[0:Res:74.2,45.0] epsilon_connected(skc13) epsilon_transitive(skc13) || -> . % 0.18/0.49 88[0:Res:57.1,45.0] empty(skc13) || -> . % 0.18/0.49 123[0:Res:64.1,60.0] || -> epsilon_connected(skc13) ordinal(skf5(skc13))*. % 0.18/0.49 124[0:Res:63.1,60.0] || -> epsilon_connected(skc13) ordinal(skf6(skc13))*. % 0.18/0.49 125[1:Spt:124.0] || -> epsilon_connected(skc13)*. % 0.18/0.49 126[1:MRR:86.0,125.0] epsilon_transitive(skc13) || -> . % 0.18/0.49 130[0:Res:66.1,67.0] || in(skf4(skc13),skc13)* -> epsilon_transitive(skc13). % 0.18/0.49 131[1:MRR:130.0,130.1,61.1,126.0] || -> . % 0.18/0.49 132[1:Spt:131.0,124.0,125.0] || epsilon_connected(skc13)* -> . % 0.18/0.49 133[1:Spt:131.0,124.1] || -> ordinal(skf6(skc13))*. % 0.18/0.49 134[1:MRR:123.0,132.0] || -> ordinal(skf5(skc13))*. % 0.18/0.49 135[0:MRR:130.0,61.1] || -> epsilon_transitive(skc13)*. % 0.18/0.49 136[0:MRR:86.1,135.0] epsilon_connected(skc13) || -> . % 0.18/0.49 156[0:Res:50.0,77.0] || -> empty(u) in(skf7(u),u)*. % 0.18/0.49 165[0:Res:50.0,82.2] empty(u) || in(v,skf7(powerset(u)))* -> . % 0.18/0.49 171[0:Res:156.1,165.1] empty(u) || -> empty(skf7(powerset(u)))*. % 0.18/0.49 173[0:EmS:65.0,171.1] empty(u) || -> equal(skf7(powerset(u)),empty_set)**. % 0.18/0.49 175[0:Rew:173.1,165.1] empty(u) || in(v,empty_set)* -> . % 0.18/0.49 185[0:Res:76.1,81.1] || subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.18/0.49 186[0:EmS:175.0,13.0] || in(u,empty_set)* -> . % 0.18/0.49 198[0:Res:83.2,62.0] ordinal(skf6(u)) ordinal(skf5(u)) || -> equal(skf6(u),skf5(u)) in(skf5(u),skf6(u))*. % 0.18/0.49 199[0:Res:83.2,69.1] ordinal(u) ordinal(v) empty(v) || -> equal(v,u) in(v,u)*. % 0.18/0.49 202[0:Res:83.2,186.0] ordinal(u) ordinal(empty_set) || -> equal(empty_set,u) in(empty_set,u)*. % 0.18/0.49 209[0:SSi:202.1,6.0,8.0,7.0,14.0,10.0,12.0,11.0,13.0] ordinal(u) || -> equal(empty_set,u) in(empty_set,u)*. % 0.18/0.49 210[0:SSi:199.1,57.1] ordinal(u) empty(v) || -> equal(v,u) in(v,u)*. % 0.18/0.49 292[0:Res:66.1,185.0] || in(u,skc13)*+ in(v,u)* -> element(v,skc13)*. % 0.18/0.49 300[0:Res:64.1,292.0] || in(u,skf5(skc13))* -> epsilon_connected(skc13) element(u,skc13). % 0.18/0.49 301[0:Res:63.1,292.0] || in(u,skf6(skc13))* -> epsilon_connected(skc13) element(u,skc13). % 0.18/0.49 306[0:MRR:300.1,136.0] || in(u,skf5(skc13))* -> element(u,skc13). % 0.18/0.49 307[0:MRR:301.1,136.0] || in(u,skf6(skc13))* -> element(u,skc13). % 0.18/0.49 322[0:Res:63.1,306.0] || -> epsilon_connected(skf5(skc13)) element(skf6(skf5(skc13)),skc13)*. % 0.18/0.49 324[0:Res:156.1,306.0] || -> empty(skf5(skc13)) element(skf7(skf5(skc13)),skc13)*. % 0.18/0.49 325[0:Res:209.2,306.0] ordinal(skf5(skc13)) || -> equal(skf5(skc13),empty_set) element(empty_set,skc13)*. % 0.18/0.49 327[1:SSi:325.0,134.0] || -> equal(skf5(skc13),empty_set) element(empty_set,skc13)*. % 0.18/0.49 329[2:Spt:327.0] || -> equal(skf5(skc13),empty_set)**. % 0.18/0.49 341[2:SpL:329.0,73.0] || in(empty_set,skf6(skc13))* -> epsilon_connected(skc13). % 0.18/0.49 344[2:MRR:341.1,136.0] || in(empty_set,skf6(skc13))* -> . % 0.18/0.49 350[2:Res:209.2,344.0] ordinal(skf6(skc13)) || -> equal(skf6(skc13),empty_set)**. % 0.18/0.49 351[2:SSi:350.0,133.0] || -> equal(skf6(skc13),empty_set)**. % 0.18/0.49 367[2:SpL:351.0,72.0] || equal(skf5(skc13),empty_set)** -> epsilon_connected(skc13). % 0.18/0.49 371[2:Rew:329.0,367.0] || equal(empty_set,empty_set) -> epsilon_connected(skc13)*. % 0.18/0.49 372[2:Obv:371.0] || -> epsilon_connected(skc13)*. % 0.18/0.49 373[2:MRR:372.0,136.0] || -> . % 0.18/0.49 374[2:Spt:373.0,327.0,329.0] || equal(skf5(skc13),empty_set)** -> . % 0.18/0.49 375[2:Spt:373.0,327.1] || -> element(empty_set,skc13)*. % 0.18/0.49 383[0:Res:324.1,77.0] || -> empty(skf5(skc13)) empty(skc13) in(skf7(skf5(skc13)),skc13)*. % 0.18/0.49 384[0:MRR:383.1,88.0] || -> empty(skf5(skc13)) in(skf7(skf5(skc13)),skc13)*. % 0.18/0.49 387[3:Spt:322.0] || -> epsilon_connected(skf5(skc13))*. % 0.18/0.49 393[0:Res:210.3,62.0] ordinal(skf5(u)) empty(skf6(u)) || -> equal(skf6(u),skf5(u))**. % 0.18/0.49 405[0:Res:210.3,73.0] ordinal(skf6(u)) empty(skf5(u)) || -> equal(skf6(u),skf5(u))** epsilon_connected(u). % 0.18/0.49 407[0:MRR:405.2,72.0] ordinal(skf6(u)) empty(skf5(u)) || -> epsilon_connected(u)*. % 0.18/0.49 411[0:Res:384.1,60.0] || -> empty(skf5(skc13)) ordinal(skf7(skf5(skc13)))*. % 0.18/0.49 415[4:Spt:411.0] || -> empty(skf5(skc13))*. % 0.18/0.49 417[4:EmS:65.0,415.0] || -> equal(skf5(skc13),empty_set)**. % 0.18/0.49 419[4:MRR:417.0,374.0] || -> . % 0.18/0.49 421[4:Spt:419.0,411.0,415.0] || empty(skf5(skc13))* -> . % 0.18/0.49 422[4:Spt:419.0,411.1] || -> ordinal(skf7(skf5(skc13)))*. % 0.18/0.49 428[1:SoR:198.0,133.0] ordinal(skf5(skc13)) || -> equal(skf6(skc13),skf5(skc13)) in(skf5(skc13),skf6(skc13))*. % 0.18/0.49 431[3:SSi:428.0,134.0,387.0] || -> equal(skf6(skc13),skf5(skc13)) in(skf5(skc13),skf6(skc13))*. % 0.18/0.49 510[1:SoR:407.0,133.0] empty(skf5(skc13)) || -> epsilon_connected(skc13)*. % 0.18/0.49 513[1:MRR:510.1,136.0] empty(skf5(skc13)) || -> . % 0.18/0.49 550[0:Res:156.1,307.0] || -> empty(skf6(skc13)) element(skf7(skf6(skc13)),skc13)*. % 0.18/0.49 560[1:SoR:393.0,134.0] empty(skf6(skc13)) || -> equal(skf6(skc13),skf5(skc13))**. % 0.18/0.49 563[0:Res:550.1,77.0] || -> empty(skf6(skc13)) empty(skc13) in(skf7(skf6(skc13)),skc13)*. % 0.18/0.49 564[0:MRR:563.1,88.0] || -> empty(skf6(skc13)) in(skf7(skf6(skc13)),skc13)*. % 0.18/0.49 573[5:Spt:564.0] || -> empty(skf6(skc13))*. % 0.18/0.49 574[5:MRR:560.0,573.0] || -> equal(skf6(skc13),skf5(skc13))**. % 0.18/0.49 581[5:Rew:574.0,573.0] || -> empty(skf5(skc13))*. % 0.18/0.49 582[5:MRR:581.0,513.0] || -> . % 0.18/0.49 584[5:Spt:582.0,564.0,573.0] || empty(skf6(skc13))* -> . % 0.18/0.49 585[5:Spt:582.0,564.1] || -> in(skf7(skf6(skc13)),skc13)*. % 0.18/0.49 642[6:Spt:431.0] || -> equal(skf6(skc13),skf5(skc13))**. % 0.18/0.49 670[6:SpL:642.0,72.0] || equal(skf5(skc13),skf5(skc13))* -> epsilon_connected(skc13). % 0.18/0.49 673[6:Obv:670.0] || -> epsilon_connected(skc13)*. % 0.18/0.49 674[6:MRR:673.0,136.0] || -> . % 0.18/0.49 675[6:Spt:674.0,431.0,642.0] || equal(skf6(skc13),skf5(skc13))** -> . % 0.18/0.49 676[6:Spt:674.0,431.1] || -> in(skf5(skc13),skf6(skc13))*. % 0.18/0.49 683[6:Res:676.0,73.0] || -> epsilon_connected(skc13)*. % 0.18/0.49 685[6:MRR:683.0,136.0] || -> . % 0.18/0.49 689[3:Spt:685.0,322.0,387.0] || epsilon_connected(skf5(skc13))* -> . % 0.18/0.49 690[3:Spt:685.0,322.1] || -> element(skf6(skf5(skc13)),skc13)*. % 0.18/0.49 705[3:Res:59.1,689.0] ordinal(skf5(skc13)) || -> . % 0.18/0.49 706[3:SSi:705.0,134.0] || -> . % 0.18/0.49 % SZS output end Refutation % 0.18/0.49 Formulae used in the proof : fc2_ordinal1 fc4_relat_1 t31_ordinal1 existence_m1_subset_1 cc3_ordinal1 d4_ordinal1 d2_ordinal1 d3_ordinal1 antisymmetry_r2_hidden t6_boole t7_boole t3_subset t2_subset t4_subset t5_subset t24_ordinal1 % 0.18/0.49 %------------------------------------------------------------------------------