%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU234+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n032.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 39.80s 40.06s % Output : Refutation 39.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SEU234+2 : TPTP v8.1.0. Released v3.3.0. % 0.00/0.10 % Command : run_spass %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Sun Jun 19 20:11:48 EDT 2022 % 0.09/0.29 % CPUTime : % 39.80/40.06 % 39.80/40.06 SPASS V 3.9 % 39.80/40.06 SPASS beiseite: Proof found. % 39.80/40.06 % SZS status Theorem % 39.80/40.06 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.80/40.06 SPASS derived 26911 clauses, backtracked 1712 clauses, performed 37 splits and kept 13963 clauses. % 39.80/40.06 SPASS allocated 125915 KBytes. % 39.80/40.06 SPASS spent 0:0:39.02 on the problem. % 39.80/40.06 0:00:00.03 for the input. % 39.80/40.06 0:00:05.71 for the FLOTTER CNF translation. % 39.80/40.06 0:00:00.50 for inferences. % 39.80/40.06 0:00:00.46 for the backtracking. % 39.80/40.06 0:0:31.84 for the reduction. % 39.80/40.06 % 39.80/40.06 % 39.80/40.06 Here is a proof with depth 2, length 33 : % 39.80/40.06 % SZS output start Refutation % 39.80/40.06 45[0:Inp] || ordinal(skc13)* -> . % 39.80/40.06 53[0:Inp] || -> subset(u,u)*. % 39.80/40.06 95[0:Inp] || in(u,skc13)* -> ordinal(u). % 39.80/40.06 97[0:Inp] || -> epsilon_transitive(u) in(skf112(u),u)*. % 39.80/40.06 98[0:Inp] || in(skf120(u),skf121(u))* -> . % 39.80/40.06 99[0:Inp] || -> epsilon_connected(u) in(skf121(u),u)*. % 39.80/40.06 100[0:Inp] || -> epsilon_connected(u) in(skf120(u),u)*. % 39.80/40.06 111[0:Inp] || in(u,skc13)* -> subset(u,skc13). % 39.80/40.06 119[0:Inp] || subset(skf112(u),u)*l -> epsilon_transitive(u). % 39.80/40.06 137[0:Inp] || in(skf121(u),skf120(u))* -> epsilon_connected(u). % 39.80/40.06 138[0:Inp] || equal(skf121(u),skf120(u))** -> epsilon_connected(u). % 39.80/40.06 140[0:Inp] epsilon_connected(u) epsilon_transitive(u) || -> ordinal(u)*. % 39.80/40.06 249[0:Inp] || subset(u,v)* subset(v,w)* -> subset(u,w)*. % 39.80/40.06 346[0:Inp] ordinal(u) ordinal(v) || -> in(u,v)* equal(v,u) in(v,u)*. % 39.80/40.06 567[0:Res:140.2,45.0] epsilon_connected(skc13) epsilon_transitive(skc13) || -> . % 39.80/40.06 642[0:Res:100.1,95.0] || -> epsilon_connected(skc13) ordinal(skf120(skc13))*. % 39.80/40.06 643[0:Res:99.1,95.0] || -> epsilon_connected(skc13) ordinal(skf121(skc13))*. % 39.80/40.06 644[1:Spt:643.0] || -> epsilon_connected(skc13)*. % 39.80/40.06 645[1:MRR:567.0,644.0] epsilon_transitive(skc13) || -> . % 39.80/40.06 2934[0:Res:97.1,111.0] || -> epsilon_transitive(skc13) subset(skf112(skc13),skc13)*l. % 39.80/40.06 2954[1:MRR:2934.0,645.0] || -> subset(skf112(skc13),skc13)*l. % 39.80/40.06 2972[1:NCh:249.2,249.0,119.0,2954.0] || subset(skc13,skc13) -> epsilon_transitive(skc13)*. % 39.80/40.06 2977[1:MRR:2972.0,2972.1,53.0,645.0] || -> . % 39.80/40.06 2978[1:Spt:2977.0,643.0,644.0] || epsilon_connected(skc13)* -> . % 39.80/40.06 2979[1:Spt:2977.0,643.1] || -> ordinal(skf121(skc13))*. % 39.80/40.06 2980[1:MRR:642.0,2978.0] || -> ordinal(skf120(skc13))*. % 39.80/40.06 2984[0:MRR:2934.1,119.0] || -> epsilon_transitive(skc13)*. % 39.80/40.06 2985[0:MRR:567.1,2984.0] epsilon_connected(skc13) || -> . % 39.80/40.06 9316[0:Res:346.4,137.0] ordinal(skf120(u)) ordinal(skf121(u)) || -> in(skf120(u),skf121(u))* equal(skf121(u),skf120(u)) epsilon_connected(u). % 39.80/40.06 9344[0:MRR:9316.2,9316.3,98.0,138.0] ordinal(skf120(u)) ordinal(skf121(u)) || -> epsilon_connected(u)*. % 39.80/40.06 32917[1:SoR:9344.0,2980.0] ordinal(skf121(skc13)) || -> epsilon_connected(skc13)*. % 39.80/40.06 32950[1:SSi:32917.0,2979.0] || -> epsilon_connected(skc13)*. % 39.80/40.06 32951[1:MRR:32950.0,2985.0] || -> . % 39.80/40.06 % SZS output end Refutation % 39.80/40.06 Formulae used in the proof : t31_ordinal1 reflexivity_r1_tarski d2_ordinal1 d3_ordinal1 rc2_ordinal1 t7_boole d4_ordinal1 t1_xboole_1 t24_ordinal1 % 39.80/40.06 %------------------------------------------------------------------------------