%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO072-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:59:44 PM UTC 2026
% Result : Unsatisfiable 5.85s 1.22s
% Output : CNFRefutation 5.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 2
% Syntax : Number of clauses : 88 ( 88 unt; 0 nHn; 3 RR)
% Number of literals : 88 ( 87 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 162 ( 34 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
inverse(add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,inverse(add(inverse(X3),inverse(add(X3,X4)))))))) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
inverse(add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,inverse(add(inverse(X3),inverse(add(X3,X4)))))))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t4,plain,
inverse(X1) = inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(X1)),X2)),X1)),X3)),inverse(X1))),X1)),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t7,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(X1)),X2)),X1)),X3)),inverse(X1))),X1)) = inverse(X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t8,plain,
inverse(X1) = inverse(add(inverse(add(X1,inverse(X1))),X1)),
inference(cp,[status(thm)],[t7,t1]) ).
cnf(t18,plain,
inverse(add(inverse(add(X1,inverse(X1))),X1)) = inverse(X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t22,plain,
X1 = inverse(add(inverse(X1),inverse(add(X1,inverse(add(inverse(X1),inverse(add(X1,X2)))))))),
inference(cp,[status(thm)],[t1,t18]) ).
cnf(t29,plain,
inverse(add(inverse(X1),inverse(add(X1,inverse(add(inverse(X1),inverse(add(X1,X2)))))))) = X1,
inference(orient,[status(thm)],[t22]) ).
cnf(t42,plain,
X1 = inverse(add(inverse(add(inverse(add(X2,X3)),X1)),inverse(add(X2,X1)))),
inference(cp,[status(thm)],[t1,t29]) ).
cnf(t72,plain,
inverse(add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,X3)))) = X3,
inference(orient,[status(thm)],[t42]) ).
cnf(t77,plain,
X1 = inverse(add(inverse(add(X2,X1)),inverse(add(inverse(X2),X1)))),
inference(cp,[status(thm)],[t72,t29]) ).
cnf(t102,plain,
inverse(add(inverse(add(X1,X2)),inverse(add(inverse(X1),X2)))) = X2,
inference(orient,[status(thm)],[t77]) ).
cnf(t46,plain,
X1 = inverse(add(inverse(X1),inverse(add(X1,X1)))),
inference(cp,[status(thm)],[t29,t29]) ).
cnf(t53,plain,
inverse(add(inverse(X1),inverse(add(X1,X1)))) = X1,
inference(orient,[status(thm)],[t46]) ).
cnf(t110,plain,
inverse(add(X1,X1)) = inverse(add(inverse(add(X1,inverse(add(X1,X1)))),X1)),
inference(cp,[status(thm)],[t102,t53]) ).
cnf(t174,plain,
inverse(add(inverse(add(X1,inverse(add(X1,X1)))),X1)) = inverse(add(X1,X1)),
inference(orient,[status(thm)],[t110]) ).
cnf(t180,plain,
X1 = inverse(add(inverse(add(X1,X1)),inverse(add(X1,X1)))),
inference(cp,[status(thm)],[t72,t174]) ).
cnf(t195,plain,
inverse(add(inverse(add(X1,X1)),inverse(add(X1,X1)))) = X1,
inference(orient,[status(thm)],[t180]) ).
cnf(t126,plain,
inverse(add(inverse(X1),X2)) = inverse(add(X2,inverse(add(X1,inverse(add(inverse(X1),X2)))))),
inference(cp,[status(thm)],[t72,t102]) ).
cnf(t977,plain,
inverse(add(X1,inverse(add(X2,inverse(add(inverse(X2),X1)))))) = inverse(add(inverse(X2),X1)),
inference(orient,[status(thm)],[t126]) ).
cnf(t1058,plain,
X1 = inverse(add(inverse(X1),inverse(add(X1,inverse(add(inverse(X1),inverse(X1))))))),
inference(cp,[status(thm)],[t29,t977]) ).
cnf(t3009,plain,
X1 = inverse(add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t1058,t977]) ).
cnf(t1065,plain,
inverse(add(inverse(X1),inverse(X1))) = X1,
inference(orient,[status(thm)],[t3009]) ).
cnf(t3010,plain,
add(X1,X1) = X1,
inference(step,[status(thm)],[t195,t1065]) ).
cnf(t1163,plain,
add(X1,X1) = X1,
inference(rw,[status(thm)],[t3010]) ).
cnf(t1164,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t1163]) ).
cnf(t1175,plain,
X1 = inverse(add(inverse(X1),inverse(add(X1,inverse(add(inverse(X1),inverse(X1))))))),
inference(cp,[status(thm)],[t29,t1164]) ).
cnf(t3021,plain,
X1 = inverse(add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t1175,t977]) ).
cnf(t3022,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t3021,t1164]) ).
cnf(t1184,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t3022]) ).
cnf(t111,plain,
X1 = inverse(add(inverse(add(add(X1,inverse(X1)),X1)),inverse(X1))),
inference(cp,[status(thm)],[t102,t18]) ).
cnf(t139,plain,
inverse(add(inverse(add(add(X1,inverse(X1)),X1)),inverse(X1))) = X1,
inference(orient,[status(thm)],[t111]) ).
cnf(t159,plain,
inverse(X1) = inverse(add(X1,inverse(add(add(X1,inverse(X1)),inverse(X1))))),
inference(cp,[status(thm)],[t72,t139]) ).
cnf(t251,plain,
inverse(add(X1,inverse(add(add(X1,inverse(X1)),inverse(X1))))) = inverse(X1),
inference(orient,[status(thm)],[t159]) ).
cnf(t282,plain,
X1 = inverse(add(inverse(add(inverse(X2),X1)),inverse(add(X2,X1)))),
inference(cp,[status(thm)],[t72,t251]) ).
cnf(t299,plain,
inverse(add(inverse(add(inverse(X1),X2)),inverse(add(X1,X2)))) = X2,
inference(orient,[status(thm)],[t282]) ).
cnf(t346,plain,
inverse(add(X1,X2)) = inverse(add(X2,inverse(add(inverse(X1),inverse(add(X1,X2)))))),
inference(cp,[status(thm)],[t72,t299]) ).
cnf(t419,plain,
inverse(add(X1,inverse(add(inverse(X2),inverse(add(X2,X1)))))) = inverse(add(X2,X1)),
inference(orient,[status(thm)],[t346]) ).
cnf(t1186,plain,
add(X1,inverse(add(inverse(X2),inverse(add(X2,X1))))) = inverse(inverse(add(X2,X1))),
inference(cp,[status(thm)],[t1184,t419]) ).
cnf(t3035,plain,
add(X1,inverse(add(inverse(X2),inverse(add(X2,X1))))) = add(X2,X1),
inference(step,[status(thm)],[t1186,t1184]) ).
cnf(t1565,plain,
add(X1,inverse(add(inverse(X2),inverse(add(X2,X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t3035]) ).
cnf(t1196,plain,
add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,X3))) = inverse(X3),
inference(cp,[status(thm)],[t1184,t72]) ).
cnf(t2245,plain,
add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,X3))) = inverse(X3),
inference(orient,[status(thm)],[t1196]) ).
cnf(t2286,plain,
inverse(inverse(add(X1,X2))) = add(inverse(inverse(X2)),inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2))))),
inference(cp,[status(thm)],[t2245,t2245]) ).
cnf(t3069,plain,
add(X1,X2) = add(inverse(inverse(X2)),inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2))))),
inference(step,[status(thm)],[t2286,t1184]) ).
cnf(t3070,plain,
add(X1,X2) = add(X2,inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2))))),
inference(step,[status(thm)],[t3069,t1184]) ).
cnf(t2582,plain,
add(X1,inverse(add(inverse(add(X2,X3)),inverse(add(X2,X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t3070]) ).
cnf(t1185,plain,
add(X1,inverse(add(X2,inverse(add(inverse(X2),X1))))) = inverse(inverse(add(inverse(X2),X1))),
inference(cp,[status(thm)],[t1184,t977]) ).
cnf(t3055,plain,
add(X1,inverse(add(X2,inverse(add(inverse(X2),X1))))) = add(inverse(X2),X1),
inference(step,[status(thm)],[t1185,t1184]) ).
cnf(t2166,plain,
add(X1,inverse(add(X2,inverse(add(inverse(X2),X1))))) = add(inverse(X2),X1),
inference(orient,[status(thm)],[t3055]) ).
cnf(t2586,plain,
add(X1,inverse(add(inverse(X1),inverse(add(X1,X2))))) = add(inverse(add(inverse(X1),inverse(add(X1,X2)))),inverse(add(inverse(X1),inverse(add(X1,X2))))),
inference(cp,[status(thm)],[t2582,t2166]) ).
cnf(t3079,plain,
add(X1,inverse(add(inverse(X1),inverse(add(X1,X2))))) = inverse(add(inverse(X1),inverse(add(X1,X2)))),
inference(step,[status(thm)],[t2586,t1164]) ).
cnf(t2883,plain,
add(X1,inverse(add(inverse(X1),inverse(add(X1,X2))))) = inverse(add(inverse(X1),inverse(add(X1,X2)))),
inference(orient,[status(thm)],[t3079]) ).
cnf(t3080,plain,
inverse(add(inverse(X1),inverse(inverse(add(inverse(X1),inverse(add(X1,X2))))))) = X1,
inference(step,[status(thm)],[t29,t2883]) ).
cnf(t3081,plain,
inverse(add(inverse(X1),add(inverse(X1),inverse(add(X1,X2))))) = X1,
inference(step,[status(thm)],[t3080,t1184]) ).
cnf(t1170,plain,
X1 = inverse(add(inverse(add(inverse(add(X1,X2)),X1)),inverse(X1))),
inference(cp,[status(thm)],[t72,t1164]) ).
cnf(t1642,plain,
inverse(add(inverse(add(inverse(add(X1,X2)),X1)),inverse(X1))) = X1,
inference(orient,[status(thm)],[t1170]) ).
cnf(t1644,plain,
inverse(add(X1,X2)) = inverse(add(X2,inverse(inverse(add(X1,X2))))),
inference(cp,[status(thm)],[t1642,t72]) ).
cnf(t3042,plain,
inverse(add(X1,X2)) = inverse(add(X2,add(X1,X2))),
inference(step,[status(thm)],[t1644,t1184]) ).
cnf(t1708,plain,
inverse(add(X1,add(X2,X1))) = inverse(add(X2,X1)),
inference(orient,[status(thm)],[t3042]) ).
cnf(t1712,plain,
add(X1,add(X2,X1)) = inverse(inverse(add(X2,X1))),
inference(cp,[status(thm)],[t1184,t1708]) ).
cnf(t3043,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(step,[status(thm)],[t1712,t1184]) ).
cnf(t1757,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(orient,[status(thm)],[t3043]) ).
cnf(t1188,plain,
add(inverse(add(inverse(X1),X2)),inverse(add(X1,X2))) = inverse(X2),
inference(cp,[status(thm)],[t1184,t299]) ).
cnf(t1394,plain,
add(inverse(add(inverse(X1),X2)),inverse(add(X1,X2))) = inverse(X2),
inference(orient,[status(thm)],[t1188]) ).
cnf(t1760,plain,
add(inverse(add(inverse(X1),X2)),inverse(add(X1,X2))) = add(inverse(add(X1,X2)),inverse(X2)),
inference(cp,[status(thm)],[t1757,t1394]) ).
cnf(t3044,plain,
inverse(X2) = add(inverse(add(X1,X2)),inverse(X2)),
inference(step,[status(thm)],[t1760,t1394]) ).
cnf(t1775,plain,
add(inverse(add(X1,X2)),inverse(X2)) = inverse(X2),
inference(orient,[status(thm)],[t3044]) ).
cnf(t1778,plain,
inverse(inverse(X1)) = add(inverse(add(X2,inverse(X1))),X1),
inference(cp,[status(thm)],[t1775,t1184]) ).
cnf(t3045,plain,
X1 = add(inverse(add(X2,inverse(X1))),X1),
inference(step,[status(thm)],[t1778,t1184]) ).
cnf(t1794,plain,
add(inverse(add(X1,inverse(X2))),X2) = X2,
inference(orient,[status(thm)],[t3045]) ).
cnf(t1804,plain,
X1 = inverse(add(inverse(X1),inverse(add(X2,X1)))),
inference(cp,[status(thm)],[t72,t1794]) ).
cnf(t1812,plain,
inverse(add(inverse(X1),inverse(add(X2,X1)))) = X1,
inference(orient,[status(thm)],[t1804]) ).
cnf(t1831,plain,
add(inverse(X1),inverse(add(X2,X1))) = inverse(X1),
inference(cp,[status(thm)],[t1184,t1812]) ).
cnf(t2058,plain,
add(inverse(X1),inverse(add(X2,X1))) = inverse(X1),
inference(orient,[status(thm)],[t1831]) ).
cnf(t2584,plain,
add(X1,add(X1,X2)) = add(add(X1,X2),inverse(inverse(add(X1,X2)))),
inference(cp,[status(thm)],[t2582,t2058]) ).
cnf(t3071,plain,
add(X1,add(X1,X2)) = add(add(X1,X2),add(X1,X2)),
inference(step,[status(thm)],[t2584,t1184]) ).
cnf(t3072,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(step,[status(thm)],[t3071,t1164]) ).
cnf(t2662,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(orient,[status(thm)],[t3072]) ).
cnf(t3082,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(step,[status(thm)],[t3081,t2662]) ).
cnf(t2906,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(rw,[status(thm)],[t3082]) ).
cnf(t2907,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(orient,[status(thm)],[t2906]) ).
cnf(t3083,plain,
add(X1,X2) = add(X2,X1),
inference(step,[status(thm)],[t1565,t2907]) ).
cnf(t2946,plain,
add(X1,X2) = add(X2,X1),
inference(rw,[status(thm)],[t3083]) ).
cnf(t2969,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2946]) ).
cnf(goal_0,negated_conjecture,
add(b,a) != add(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(b,a) != add(b,a),
inference(rw,[status(thm)],[goal_0,t2969]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO072-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 06:42:32 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.85/1.22 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.85/1.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------