%------------------------------------------------------------------------------ % File : hopCoP---0.1 % Problem : SYN213-1 : TPTP v9.0.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 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 : 300s % DateTime : Fri Jul 25 09:27:08 PM UTC 2025 % Result : Unsatisfiable 0.12s 0.37s % Output : CNFRefutation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN213-1 : TPTP v9.0.0. Released v1.1.0. % 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 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 : 300 % 0.12/0.33 % DateTime : Tue Jul 22 15:42:49 EDT 2025 % 0.12/0.34 % CPUTime : % 0.12/0.34 % launching worker at depth: 4 % 0.12/0.34 % launching worker at depth: 6 % 0.12/0.34 % launching worker at depth: 1 % 0.12/0.34 % launching worker at depth: 3 % 0.12/0.34 % launching worker at depth: 8 % 0.12/0.34 % launching worker at depth: 2 % 0.12/0.34 % launching worker at depth: 5 % 0.12/0.34 % launching worker at depth: 7 % 0.12/0.34 % launching worker at depth: 9 % 0.12/0.34 % launching worker at depth: 10 % 0.12/0.34 % launching worker at depth: 11 % 0.12/0.37 % SZS status Theorem for theBenchmark % 0.12/0.37 % SZS output start CNFRefutation % 0.12/0.37 cnf(361, plain, ~s5(b), inference(cnf, [status(esa)], [prove_this])). % 0.12/0.37 cnf(l0, plain, ~s5(b), inference(instantiation, [status(thm)], [361])). % 0.12/0.37 cnf(359, plain, ~l4(X0) | ~r4(X1) | s5(X0), inference(cnf, [status(esa)], [rule_329])). % 0.12/0.37 cnf(l1, plain, ~l4(b) | ~r4(c) | s5(b), inference(instantiation, [status(thm)], [359])). % 0.12/0.37 cnf(328, plain, ~p0(X0,X1) | ~n3(X1) | ~q3(X2,X3) | r4(X1), inference(cnf, [status(esa)], [rule_298])). % 0.12/0.37 cnf(l4, plain, ~p0(b,c) | ~n3(c) | ~q3(c,c) | r4(c), inference(instantiation, [status(thm)], [328])). % 0.12/0.37 cnf(21, plain, p0(b,c), inference(cnf, [status(esa)], [axiom_22])). % 0.12/0.37 cnf(l9, plain, p0(b,c), inference(instantiation, [status(thm)], [21])). % 0.12/0.37 cnf(308, plain, ~p3(X0,X1,X2) | l4(X2), inference(cnf, [status(esa)], [rule_277])). % 0.12/0.37 cnf(l2, plain, ~p3(b,b,b) | l4(b), inference(instantiation, [status(thm)], [308])). % 0.12/0.37 cnf(272, plain, ~p2(X0,X1,X2) | n3(X2), inference(cnf, [status(esa)], [rule_240])). % 0.12/0.37 cnf(l10, plain, ~p2(c,e,c) | n3(c), inference(instantiation, [status(thm)], [272])). % 0.12/0.37 cnf(290, plain, ~s1(X0) | ~l2(X1,X1) | ~r2(X2) | q3(X2,X2), inference(cnf, [status(esa)], [rule_258])). % 0.12/0.37 cnf(l11, plain, ~s1(b) | ~l2(e,e) | ~r2(c) | q3(c,c), inference(instantiation, [status(thm)], [290])). % 0.12/0.37 cnf(280, plain, ~p2(X0,X1,X1) | ~n3(X1) | p3(X1,X1,X1), inference(cnf, [status(esa)], [rule_248])). % 0.12/0.37 cnf(l6, plain, ~p2(b,b,b) | ~n3(b) | p3(b,b,b), inference(instantiation, [status(thm)], [280])). % 0.12/0.37 cnf(160, plain, ~p0(X0,X0) | s1(X0), inference(cnf, [status(esa)], [rule_125])). % 0.12/0.37 cnf(l12, plain, ~p0(b,b) | s1(b), inference(instantiation, [status(thm)], [160])). % 0.12/0.37 cnf(167, plain, ~p0(X0,X0) | ~m0(X1,X2,X3) | ~s1(X2) | l2(X3,X3), inference(cnf, [status(esa)], [rule_133])). % 0.12/0.37 cnf(l13, plain, ~p0(b,b) | ~m0(e,d,e) | ~s1(d) | l2(e,e), inference(instantiation, [status(thm)], [167])). % 0.12/0.37 cnf(13, plain, p0(b,X0), inference(cnf, [status(esa)], [axiom_14])). % 0.12/0.37 cnf(l14, plain, p0(b,b), inference(instantiation, [status(thm)], [13])). % 0.12/0.37 cnf(l15, plain, ~p2(b,b,b) | n3(b), inference(instantiation, [status(thm)], [272])). % 0.12/0.37 cnf(199, plain, ~q1(X0,X1,X0) | ~p2(X0,X0,X1) | p2(X2,X2,X2), inference(cnf, [status(esa)], [rule_165])). % 0.12/0.37 cnf(l16, plain, ~q1(c,c,c) | ~p2(c,c,c) | p2(b,b,b), inference(instantiation, [status(thm)], [199])). % 0.12/0.37 cnf(l17, plain, p0(b,b), inference(instantiation, [status(thm)], [13])). % 0.12/0.37 cnf(208, plain, ~k1(e) | ~n2(X0) | p2(X0,X0,X0), inference(cnf, [status(esa)], [rule_174])). % 0.12/0.37 cnf(l18, plain, ~k1(e) | ~n2(b) | p2(b,b,b), inference(instantiation, [status(thm)], [208])). % 0.12/0.37 cnf(204, plain, ~n1(X0,e,e) | p2(X0,e,X0), inference(cnf, [status(esa)], [rule_170])). % 0.12/0.37 cnf(l19, plain, ~n1(c,e,e) | p2(c,e,c), inference(instantiation, [status(thm)], [204])). % 0.12/0.37 cnf(189, plain, ~k1(X0) | ~p2(e,X1,X2) | p2(X1,X2,X2), inference(cnf, [status(esa)], [rule_155])). % 0.12/0.37 cnf(l20, plain, ~k1(a) | ~p2(e,c,c) | p2(c,c,c), inference(instantiation, [status(thm)], [189])). % 0.12/0.37 cnf(128, plain, ~q0(X0,X1) | q1(X1,X1,X1), inference(cnf, [status(esa)], [rule_093])). % 0.12/0.37 cnf(l21, plain, ~q0(d,c) | q1(c,c,c), inference(instantiation, [status(thm)], [128])). % 0.12/0.37 cnf(222, plain, ~l0(X0) | ~r1(X0) | r2(X0), inference(cnf, [status(esa)], [rule_188])). % 0.12/0.37 cnf(l22, plain, ~l0(c) | ~r1(c) | r2(c), inference(instantiation, [status(thm)], [222])). % 0.12/0.37 cnf(7, plain, m0(e,d,e), inference(cnf, [status(esa)], [axiom_8])). % 0.12/0.37 cnf(l23, plain, m0(e,d,e), inference(instantiation, [status(thm)], [7])). % 0.12/0.37 % launching worker at depth: cnf(90, plain, ~l0(X0) | ~l1(X0,X1) | ~n1(X1,X2,X1) | n1(X1,X2,X2), inference(cnf, [status(esa)], [rule_054])). % 0.12/0.37 12 % 0.12/0.37 cnf(l24, plain, ~l0(c) | ~l1(c,c) | ~n1(c,e,c) | n1(c,e,e), inference(instantiation, [status(thm)], [90])). % 0.12/0.37 cnf(38, plain, ~n0(X0,X1) | k1(X1), inference(cnf, [status(esa)], [rule_001])). % 0.12/0.37 cnf(l25, plain, ~n0(d,e) | k1(e), inference(instantiation, [status(thm)], [38])). % 0.12/0.37 cnf(159, plain, ~s0(d) | ~q0(X0,X1) | ~q1(d,X1,d) | r1(X0), inference(cnf, [status(esa)], [rule_124])). % 0.12/0.37 cnf(l26, plain, ~s0(d) | ~q0(c,d) | ~q1(d,d,d) | r1(c), inference(instantiation, [status(thm)], [159])). % 0.12/0.37 cnf(l27, plain, ~n0(b,a) | k1(a), inference(instantiation, [status(thm)], [38])). % 0.12/0.37 cnf(171, plain, ~p1(X0,X1,X2) | n2(X2), inference(cnf, [status(esa)], [rule_137])). % 0.12/0.37 cnf(l28, plain, ~p1(c,c,b) | n2(b), inference(instantiation, [status(thm)], [171])). % 0.12/0.37 cnf(135, plain, ~n0(X0,X1) | q1(X1,X1,X1), inference(cnf, [status(esa)], [rule_100])). % 0.12/0.37 cnf(l37, plain, ~n0(c,d) | q1(d,d,d), inference(instantiation, [status(thm)], [135])). % 0.12/0.37 cnf(86, plain, ~s0(b) | ~p0(b,X0) | ~l0(X1) | n1(X1,X0,X1), inference(cnf, [status(esa)], [rule_050])). % 0.12/0.37 cnf(l42, plain, ~s0(b) | ~p0(b,e) | ~l0(c) | n1(c,e,c), inference(instantiation, [status(thm)], [86])). % 0.12/0.37 cnf(0, plain, s0(d), inference(cnf, [status(esa)], [axiom_1])). % 0.12/0.37 cnf(l39, plain, s0(d), inference(instantiation, [status(thm)], [0])). % 0.12/0.37 cnf(23, plain, l0(c), inference(cnf, [status(esa)], [axiom_24])). % 0.12/0.37 cnf(l60, plain, l0(c), inference(instantiation, [status(thm)], [23])). % 0.12/0.37 cnf(105, plain, ~p0(X0,X1) | p1(X1,X1,X0), inference(cnf, [status(esa)], [rule_069])). % 0.12/0.37 cnf(l33, plain, ~p0(b,c) | p1(c,c,b), inference(instantiation, [status(thm)], [105])). % 0.12/0.37 cnf(l35, plain, p0(b,c), inference(instantiation, [status(thm)], [21])). % 0.12/0.37 cnf(l62, plain, p0(b,e), inference(instantiation, [status(thm)], [13])). % 0.12/0.37 cnf(l36, plain, l0(c), inference(instantiation, [status(thm)], [23])). % 0.12/0.37 cnf(16, plain, q0(X0,d), inference(cnf, [status(esa)], [axiom_17])). % 0.12/0.37 cnf(l32, plain, q0(c,d), inference(instantiation, [status(thm)], [16])). % 0.12/0.37 cnf(36, plain, n0(b,a), inference(cnf, [status(esa)], [axiom_37])). % 0.12/0.37 cnf(l61, plain, n0(b,a), inference(instantiation, [status(thm)], [36])). % 0.12/0.37 cnf(33, plain, n0(c,d), inference(cnf, [status(esa)], [axiom_34])). % 0.12/0.37 cnf(l47, plain, n0(c,d), inference(instantiation, [status(thm)], [33])). % 0.12/0.37 cnf(4, plain, s0(b), inference(cnf, [status(esa)], [axiom_5])). % 0.12/0.37 cnf(l45, plain, s0(b), inference(instantiation, [status(thm)], [4])). % 0.12/0.37 cnf(39, plain, ~n0(X0,X1) | l1(X1,X1), inference(cnf, [status(esa)], [rule_002])). % 0.12/0.37 cnf(l30, plain, ~n0(d,c) | l1(c,c), inference(instantiation, [status(thm)], [39])). % 0.12/0.37 cnf(l44, plain, l0(c), inference(instantiation, [status(thm)], [23])). % 0.12/0.37 cnf(32, plain, q0(d,c), inference(cnf, [status(esa)], [axiom_33])). % 0.12/0.37 cnf(l53, plain, q0(d,c), inference(instantiation, [status(thm)], [32])). % 0.12/0.37 cnf(2, plain, n0(d,e), inference(cnf, [status(esa)], [axiom_3])). % 0.12/0.37 cnf(l41, plain, n0(d,e), inference(instantiation, [status(thm)], [2])). % 0.12/0.37 cnf(161, plain, ~q0(X0,X1) | ~s1(X2) | s1(X0), inference(cnf, [status(esa)], [rule_126])). % 0.12/0.37 cnf(l55, plain, ~q0(d,c) | ~s1(e) | s1(d), inference(instantiation, [status(thm)], [161])). % 0.12/0.37 cnf(l65, plain, ~q0(e,d) | ~s1(b) | s1(e), inference(instantiation, [status(thm)], [161])). % 0.12/0.37 cnf(1, plain, q0(e,d), inference(cnf, [status(esa)], [axiom_2])). % 0.12/0.37 cnf(l67, plain, q0(e,d), inference(instantiation, [status(thm)], [1])). % 0.12/0.37 cnf(l64, plain, q0(d,c), inference(instantiation, [status(thm)], [32])). % 0.12/0.37 cnf(179, plain, ~r0(e) | ~p1(X0,X1,e) | p2(e,X0,X1), inference(cnf, [status(esa)], [rule_145])). % 0.12/0.37 cnf(l29, plain, ~r0(e) | ~p1(c,c,e) | p2(e,c,c), inference(instantiation, [status(thm)], [179])). % 0.12/0.37 cnf(12, plain, r0(e), inference(cnf, [status(esa)], [axiom_13])). % 0.12/0.37 cnf(l49, plain, r0(e), inference(instantiation, [status(thm)], [12])). % 0.12/0.37 cnf(99, plain, ~n0(d,X0) | ~k0(X1) | p1(X0,X0,X1), inference(cnf, [status(esa)], [rule_063])). % 0.12/0.37 cnf(l34, plain, ~n0(d,c) | ~k0(e) | p1(c,c,e), inference(instantiation, [status(thm)], [99])). % 0.12/0.37 cnf(25, plain, n0(d,c), inference(cnf, [status(esa)], [axiom_26])). % 0.12/0.37 cnf(l56, plain, n0(d,c), inference(instantiation, [status(thm)], [25])). % 0.12/0.37 cnf(l52, plain, n0(d,c), inference(instantiation, [status(thm)], [25])). % 0.12/0.37 cnf(l68, plain, ~p0(b,b) | s1(b), inference(instantiation, [status(thm)], [160])). % 0.12/0.37 cnf(l73, plain, p0(b,b), inference(instantiation, [status(thm)], [13])). % 0.12/0.37 cnf(27, plain, k0(e), inference(cnf, [status(esa)], [axiom_28])). % 0.12/0.37 cnf(l48, plain, k0(e), inference(instantiation, [status(thm)], [27])). % 0.12/0.37 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l4, l9, l2, l10, l11, l6, l12, l13, l14, l15, l16, l17, l18, l19, l20, l21, l22, l23, l24, l25, l26, l27, l28, l37, l42, l39, l60, l33, l35, l62, l36, l32, l61, l47, l45, l30, l44, l53, l41, l55, l65, l67, l64, l29, l49, l34, l56, l52, l68, l73, l48])). % 0.12/0.37 % SZS output end CNFRefutation %------------------------------------------------------------------------------