%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO073-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 : n007.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 14.33s 2.28s
% Output : CNFRefutation 14.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 126
% Number of leaves : 2
% Syntax : Number of clauses : 245 ( 245 unt; 0 nHn; 7 RR)
% Number of literals : 245 ( 244 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 556 ( 123 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(t15317,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)],[t15317]) ).
cnf(t15318,plain,
add(X1,X1) = X1,
inference(step,[status(thm)],[t195,t1065]) ).
cnf(t1163,plain,
add(X1,X1) = X1,
inference(rw,[status(thm)],[t15318]) ).
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(t15329,plain,
X1 = inverse(add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t1175,t977]) ).
cnf(t15330,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t15329,t1164]) ).
cnf(t1184,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t15330]) ).
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(t15343,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)],[t15343]) ).
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(t15377,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(t15378,plain,
add(X1,X2) = add(X2,inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2))))),
inference(step,[status(thm)],[t15377,t1184]) ).
cnf(t2582,plain,
add(X1,inverse(add(inverse(add(X2,X3)),inverse(add(X2,X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t15378]) ).
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(t15363,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)],[t15363]) ).
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(t15387,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)],[t15387]) ).
cnf(t15388,plain,
inverse(add(inverse(X1),inverse(inverse(add(inverse(X1),inverse(add(X1,X2))))))) = X1,
inference(step,[status(thm)],[t29,t2883]) ).
cnf(t15389,plain,
inverse(add(inverse(X1),add(inverse(X1),inverse(add(X1,X2))))) = X1,
inference(step,[status(thm)],[t15388,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(t15350,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)],[t15350]) ).
cnf(t1712,plain,
add(X1,add(X2,X1)) = inverse(inverse(add(X2,X1))),
inference(cp,[status(thm)],[t1184,t1708]) ).
cnf(t15351,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)],[t15351]) ).
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(t15352,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)],[t15352]) ).
cnf(t1778,plain,
inverse(inverse(X1)) = add(inverse(add(X2,inverse(X1))),X1),
inference(cp,[status(thm)],[t1775,t1184]) ).
cnf(t15353,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)],[t15353]) ).
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(t15379,plain,
add(X1,add(X1,X2)) = add(add(X1,X2),add(X1,X2)),
inference(step,[status(thm)],[t2584,t1184]) ).
cnf(t15380,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(step,[status(thm)],[t15379,t1164]) ).
cnf(t2662,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(orient,[status(thm)],[t15380]) ).
cnf(t15390,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(step,[status(thm)],[t15389,t2662]) ).
cnf(t2906,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(rw,[status(thm)],[t15390]) ).
cnf(t2907,plain,
inverse(add(inverse(X1),inverse(add(X1,X2)))) = X1,
inference(orient,[status(thm)],[t2906]) ).
cnf(t15391,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)],[t15391]) ).
cnf(t2969,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2946]) ).
cnf(t2285,plain,
add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X1,X3))) = add(inverse(add(X1,X3)),inverse(add(inverse(inverse(add(inverse(add(X1,X2)),X3))),inverse(inverse(X3))))),
inference(cp,[status(thm)],[t1565,t2245]) ).
cnf(t15368,plain,
inverse(X3) = add(inverse(add(X1,X3)),inverse(add(inverse(inverse(add(inverse(add(X1,X2)),X3))),inverse(inverse(X3))))),
inference(step,[status(thm)],[t2285,t2245]) ).
cnf(t15369,plain,
inverse(X3) = add(inverse(add(X1,X3)),inverse(add(add(inverse(add(X1,X2)),X3),inverse(inverse(X3))))),
inference(step,[status(thm)],[t15368,t1184]) ).
cnf(t15370,plain,
inverse(X3) = add(inverse(add(X1,X3)),inverse(add(add(inverse(add(X1,X2)),X3),X3))),
inference(step,[status(thm)],[t15369,t1184]) ).
cnf(t1821,plain,
inverse(add(X1,X2)) = inverse(add(inverse(inverse(add(X1,X2))),X2)),
inference(cp,[status(thm)],[t1812,t72]) ).
cnf(t15354,plain,
inverse(add(X1,X2)) = inverse(add(add(X1,X2),X2)),
inference(step,[status(thm)],[t1821,t1184]) ).
cnf(t1864,plain,
inverse(add(add(X1,X2),X2)) = inverse(add(X1,X2)),
inference(orient,[status(thm)],[t15354]) ).
cnf(t1866,plain,
add(add(X1,X2),X2) = inverse(inverse(add(X1,X2))),
inference(cp,[status(thm)],[t1184,t1864]) ).
cnf(t15355,plain,
add(add(X1,X2),X2) = add(X1,X2),
inference(step,[status(thm)],[t1866,t1184]) ).
cnf(t1890,plain,
add(add(X1,X2),X2) = add(X1,X2),
inference(orient,[status(thm)],[t15355]) ).
cnf(t15371,plain,
inverse(X3) = add(inverse(add(X1,X3)),inverse(add(inverse(add(X1,X2)),X3))),
inference(step,[status(thm)],[t15370,t1890]) ).
cnf(t2417,plain,
add(inverse(add(X1,X2)),inverse(add(inverse(add(X1,X3)),X2))) = inverse(X2),
inference(orient,[status(thm)],[t15371]) ).
cnf(t2439,plain,
inverse(inverse(add(X1,X2))) = add(inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2)))),inverse(inverse(X2))),
inference(cp,[status(thm)],[t2417,t2245]) ).
cnf(t15383,plain,
add(X1,X2) = add(inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2)))),inverse(inverse(X2))),
inference(step,[status(thm)],[t2439,t1184]) ).
cnf(t15384,plain,
add(X1,X2) = add(inverse(add(inverse(add(X1,X3)),inverse(add(X1,X2)))),X2),
inference(step,[status(thm)],[t15383,t1184]) ).
cnf(t2735,plain,
add(inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3)))),X3) = add(X1,X3),
inference(orient,[status(thm)],[t15384]) ).
cnf(t2982,plain,
add(inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3)))),X3) = add(X1,X3),
inference(rw,[status(thm)],[t2735]) ).
cnf(t15415,plain,
add(X3,inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3))))) = add(X1,X3),
inference(step,[status(thm)],[t2982,t2969]) ).
cnf(t3382,plain,
add(X1,inverse(add(inverse(add(X2,X3)),inverse(add(X2,X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t15415]) ).
cnf(t2909,plain,
add(inverse(X1),inverse(add(X1,X2))) = inverse(X1),
inference(cp,[status(thm)],[t1184,t2907]) ).
cnf(t2999,plain,
add(inverse(X1),inverse(add(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t2909]) ).
cnf(t2974,plain,
add(add(X1,X2),X2) = add(X1,X2),
inference(rw,[status(thm)],[t1890]) ).
cnf(t15395,plain,
add(X2,add(X1,X2)) = add(X1,X2),
inference(step,[status(thm)],[t2974,t2969]) ).
cnf(t2995,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(orient,[status(thm)],[t15395]) ).
cnf(t1194,plain,
add(inverse(add(X1,X2)),inverse(add(inverse(X1),X2))) = inverse(X2),
inference(cp,[status(thm)],[t1184,t102]) ).
cnf(t1499,plain,
add(inverse(add(X1,X2)),inverse(add(inverse(X1),X2))) = inverse(X2),
inference(orient,[status(thm)],[t1194]) ).
cnf(t2068,plain,
inverse(inverse(add(X1,X2))) = add(inverse(inverse(X2)),inverse(add(inverse(inverse(X2)),inverse(add(X1,X2))))),
inference(cp,[status(thm)],[t1499,t2058]) ).
cnf(t15358,plain,
add(X1,X2) = add(inverse(inverse(X2)),inverse(add(inverse(inverse(X2)),inverse(add(X1,X2))))),
inference(step,[status(thm)],[t2068,t1184]) ).
cnf(t15359,plain,
add(X1,X2) = add(X2,inverse(add(inverse(inverse(X2)),inverse(add(X1,X2))))),
inference(step,[status(thm)],[t15358,t1184]) ).
cnf(t15360,plain,
add(X1,X2) = add(X2,inverse(add(X2,inverse(add(X1,X2))))),
inference(step,[status(thm)],[t15359,t1184]) ).
cnf(t2112,plain,
add(X1,inverse(add(X1,inverse(add(X2,X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t15360]) ).
cnf(t2256,plain,
inverse(X1) = add(inverse(add(inverse(add(X2,X3)),X1)),inverse(add(X3,X1))),
inference(cp,[status(thm)],[t2245,t2112]) ).
cnf(t2315,plain,
add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X2,X3))) = inverse(X3),
inference(orient,[status(thm)],[t2256]) ).
cnf(t2440,plain,
inverse(inverse(add(X1,X2))) = add(inverse(add(inverse(add(X3,X1)),inverse(add(X1,X2)))),inverse(inverse(X2))),
inference(cp,[status(thm)],[t2417,t2315]) ).
cnf(t15385,plain,
add(X1,X2) = add(inverse(add(inverse(add(X3,X1)),inverse(add(X1,X2)))),inverse(inverse(X2))),
inference(step,[status(thm)],[t2440,t1184]) ).
cnf(t15386,plain,
add(X1,X2) = add(inverse(add(inverse(add(X3,X1)),inverse(add(X1,X2)))),X2),
inference(step,[status(thm)],[t15385,t1184]) ).
cnf(t2813,plain,
add(inverse(add(inverse(add(X1,X2)),inverse(add(X2,X3)))),X3) = add(X2,X3),
inference(orient,[status(thm)],[t15386]) ).
cnf(t2981,plain,
add(inverse(add(inverse(add(X1,X2)),inverse(add(X2,X3)))),X3) = add(X2,X3),
inference(rw,[status(thm)],[t2813]) ).
cnf(t15414,plain,
add(X3,inverse(add(inverse(add(X1,X2)),inverse(add(X2,X3))))) = add(X2,X3),
inference(step,[status(thm)],[t2981,t2969]) ).
cnf(t3322,plain,
add(X1,inverse(add(inverse(add(X2,X3)),inverse(add(X3,X1))))) = add(X3,X1),
inference(orient,[status(thm)],[t15414]) ).
cnf(t3344,plain,
add(inverse(add(X1,X2)),X3) = add(X3,inverse(add(inverse(inverse(X1)),inverse(add(inverse(add(X1,X2)),X3))))),
inference(cp,[status(thm)],[t3322,t2999]) ).
cnf(t15446,plain,
add(X3,inverse(add(X1,X2))) = add(X3,inverse(add(inverse(inverse(X1)),inverse(add(inverse(add(X1,X2)),X3))))),
inference(step,[status(thm)],[t3344,t2969]) ).
cnf(t15447,plain,
add(X3,inverse(add(X1,X2))) = add(X3,inverse(add(X1,inverse(add(inverse(add(X1,X2)),X3))))),
inference(step,[status(thm)],[t15446,t1184]) ).
cnf(t15448,plain,
add(X3,inverse(add(X1,X2))) = add(X3,inverse(add(X1,inverse(add(X3,inverse(add(X1,X2))))))),
inference(step,[status(thm)],[t15447,t2969]) ).
cnf(t4093,plain,
add(X1,inverse(add(X2,inverse(add(X1,inverse(add(X2,X3))))))) = add(X1,inverse(add(X2,X3))),
inference(orient,[status(thm)],[t15448]) ).
cnf(t2989,plain,
add(inverse(add(inverse(add(X1,X2)),X3)),inverse(add(X2,X3))) = inverse(X3),
inference(rw,[status(thm)],[t2315]) ).
cnf(t15406,plain,
add(inverse(add(X2,X3)),inverse(add(inverse(add(X1,X2)),X3))) = inverse(X3),
inference(step,[status(thm)],[t2989,t2969]) ).
cnf(t15407,plain,
add(inverse(add(X2,X3)),inverse(add(X3,inverse(add(X1,X2))))) = inverse(X3),
inference(step,[status(thm)],[t15406,t2969]) ).
cnf(t3130,plain,
add(inverse(add(X1,X2)),inverse(add(X2,inverse(add(X3,X1))))) = inverse(X2),
inference(orient,[status(thm)],[t15407]) ).
cnf(t4100,plain,
add(X1,inverse(add(inverse(add(X2,X1)),X2))) = add(X1,inverse(inverse(X1))),
inference(cp,[status(thm)],[t4093,t3130]) ).
cnf(t15449,plain,
add(X1,inverse(add(X2,inverse(add(X2,X1))))) = add(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t4100,t2969]) ).
cnf(t15450,plain,
add(X1,inverse(add(X2,inverse(add(X1,X2))))) = add(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t15449,t2969]) ).
cnf(t15451,plain,
add(X1,inverse(add(X2,inverse(add(X1,X2))))) = add(X1,X1),
inference(step,[status(thm)],[t15450,t1184]) ).
cnf(t15452,plain,
add(X1,inverse(add(X2,inverse(add(X1,X2))))) = X1,
inference(step,[status(thm)],[t15451,t1164]) ).
cnf(t4160,plain,
add(X1,inverse(add(X2,inverse(add(X1,X2))))) = X1,
inference(orient,[status(thm)],[t15452]) ).
cnf(t4214,plain,
add(X1,inverse(add(X2,X1))) = add(X1,inverse(X2)),
inference(cp,[status(thm)],[t4093,t4160]) ).
cnf(t15455,plain,
add(X1,inverse(add(X1,X2))) = add(X1,inverse(X2)),
inference(step,[status(thm)],[t4214,t2969]) ).
cnf(t4293,plain,
add(X1,inverse(add(X1,X2))) = add(X1,inverse(X2)),
inference(orient,[status(thm)],[t15455]) ).
cnf(t2987,plain,
add(inverse(add(X1,X2)),inverse(add(inverse(add(X1,X3)),X2))) = inverse(X2),
inference(rw,[status(thm)],[t2417]) ).
cnf(t15405,plain,
add(inverse(add(X1,X2)),inverse(add(X2,inverse(add(X1,X3))))) = inverse(X2),
inference(step,[status(thm)],[t2987,t2969]) ).
cnf(t3092,plain,
add(inverse(add(X1,X2)),inverse(add(X2,inverse(add(X1,X3))))) = inverse(X2),
inference(orient,[status(thm)],[t15405]) ).
cnf(t4312,plain,
add(inverse(add(X1,X2)),inverse(inverse(add(X2,inverse(add(X1,X3)))))) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t4293,t3092]) ).
cnf(t15592,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(step,[status(thm)],[t4312,t1184]) ).
cnf(t15593,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(inverse(inverse(X2)),inverse(add(X1,X2))),
inference(step,[status(thm)],[t15592,t2969]) ).
cnf(t15594,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(X2,inverse(add(X1,X2))),
inference(step,[status(thm)],[t15593,t1184]) ).
cnf(t2979,plain,
add(inverse(add(X1,X2)),inverse(add(inverse(X1),X2))) = inverse(X2),
inference(rw,[status(thm)],[t1499]) ).
cnf(t15401,plain,
add(inverse(add(X1,X2)),inverse(add(X2,inverse(X1)))) = inverse(X2),
inference(step,[status(thm)],[t2979,t2969]) ).
cnf(t3028,plain,
add(inverse(add(X1,X2)),inverse(add(X2,inverse(X1)))) = inverse(X2),
inference(orient,[status(thm)],[t15401]) ).
cnf(t4311,plain,
add(inverse(add(X1,X2)),inverse(inverse(add(X2,inverse(X1))))) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t4293,t3028]) ).
cnf(t15514,plain,
add(inverse(add(X1,X2)),add(X2,inverse(X1))) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(step,[status(thm)],[t4311,t1184]) ).
cnf(t15515,plain,
add(add(X2,inverse(X1)),inverse(add(X1,X2))) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(step,[status(thm)],[t15514,t2969]) ).
cnf(t2059,plain,
inverse(inverse(X1)) = add(X1,inverse(add(X2,inverse(X1)))),
inference(cp,[status(thm)],[t2058,t1184]) ).
cnf(t15357,plain,
X1 = add(X1,inverse(add(X2,inverse(X1)))),
inference(step,[status(thm)],[t2059,t1184]) ).
cnf(t2085,plain,
add(X1,inverse(add(X2,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t15357]) ).
cnf(t4308,plain,
add(X1,inverse(inverse(add(X2,inverse(X1))))) = add(X1,inverse(X1)),
inference(cp,[status(thm)],[t4293,t2085]) ).
cnf(t15456,plain,
add(X1,add(X2,inverse(X1))) = add(X1,inverse(X1)),
inference(step,[status(thm)],[t4308,t1184]) ).
cnf(t4350,plain,
add(X1,add(X2,inverse(X1))) = add(X1,inverse(X1)),
inference(orient,[status(thm)],[t15456]) ).
cnf(t2976,plain,
add(inverse(add(X1,X2)),inverse(X2)) = inverse(X2),
inference(rw,[status(thm)],[t1775]) ).
cnf(t15396,plain,
add(inverse(X2),inverse(add(X1,X2))) = inverse(X2),
inference(step,[status(thm)],[t2976,t2969]) ).
cnf(t3005,plain,
add(inverse(X1),inverse(add(X2,X1))) = inverse(X1),
inference(orient,[status(thm)],[t15396]) ).
cnf(t4376,plain,
add(add(X1,X2),inverse(add(X1,X2))) = add(add(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t4350,t3005]) ).
cnf(t4375,plain,
add(add(X1,X2),inverse(add(X1,X2))) = add(add(X1,X2),inverse(X1)),
inference(cp,[status(thm)],[t4350,t2999]) ).
cnf(t15466,plain,
add(add(X1,X2),inverse(add(X1,X2))) = add(inverse(X1),add(X1,X2)),
inference(step,[status(thm)],[t4375,t2969]) ).
cnf(t4318,plain,
add(inverse(X1),inverse(inverse(add(X1,X2)))) = add(inverse(X1),inverse(inverse(X1))),
inference(cp,[status(thm)],[t4293,t2999]) ).
cnf(t15457,plain,
add(inverse(X1),add(X1,X2)) = add(inverse(X1),inverse(inverse(X1))),
inference(step,[status(thm)],[t4318,t1184]) ).
cnf(t15458,plain,
add(inverse(X1),add(X1,X2)) = add(inverse(X1),X1),
inference(step,[status(thm)],[t15457,t1184]) ).
cnf(t15459,plain,
add(inverse(X1),add(X1,X2)) = add(X1,inverse(X1)),
inference(step,[status(thm)],[t15458,t2969]) ).
cnf(t4399,plain,
add(inverse(X1),add(X1,X2)) = add(X1,inverse(X1)),
inference(orient,[status(thm)],[t15459]) ).
cnf(t15467,plain,
add(add(X1,X2),inverse(add(X1,X2))) = add(X1,inverse(X1)),
inference(step,[status(thm)],[t15466,t4399]) ).
cnf(t4601,plain,
add(add(X1,X2),inverse(add(X1,X2))) = add(X1,inverse(X1)),
inference(orient,[status(thm)],[t15467]) ).
cnf(t3112,plain,
inverse(X1) = add(inverse(add(inverse(add(X2,X3)),X1)),inverse(add(X1,inverse(inverse(X3))))),
inference(cp,[status(thm)],[t3092,t3028]) ).
cnf(t15411,plain,
inverse(X1) = add(inverse(add(X1,inverse(inverse(X3)))),inverse(add(inverse(add(X2,X3)),X1))),
inference(step,[status(thm)],[t3112,t2969]) ).
cnf(t15412,plain,
inverse(X1) = add(inverse(add(X1,X3)),inverse(add(inverse(add(X2,X3)),X1))),
inference(step,[status(thm)],[t15411,t1184]) ).
cnf(t15413,plain,
inverse(X1) = add(inverse(add(X1,X3)),inverse(add(X1,inverse(add(X2,X3))))),
inference(step,[status(thm)],[t15412,t2969]) ).
cnf(t3264,plain,
add(inverse(add(X1,X2)),inverse(add(X1,inverse(add(X3,X2))))) = inverse(X1),
inference(orient,[status(thm)],[t15413]) ).
cnf(t3280,plain,
inverse(inverse(add(X1,X2))) = add(inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3)))),inverse(inverse(X2))),
inference(cp,[status(thm)],[t3264,t3092]) ).
cnf(t15426,plain,
add(X1,X2) = add(inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3)))),inverse(inverse(X2))),
inference(step,[status(thm)],[t3280,t1184]) ).
cnf(t15427,plain,
add(X1,X2) = add(inverse(inverse(X2)),inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3))))),
inference(step,[status(thm)],[t15426,t2969]) ).
cnf(t15428,plain,
add(X1,X2) = add(X2,inverse(add(inverse(add(X1,X2)),inverse(add(X1,X3))))),
inference(step,[status(thm)],[t15427,t1184]) ).
cnf(t3610,plain,
add(X1,inverse(add(inverse(add(X2,X1)),inverse(add(X2,X3))))) = add(X2,X1),
inference(orient,[status(thm)],[t15428]) ).
cnf(t4602,plain,
add(X1,inverse(X1)) = add(add(X2,X1),inverse(add(X1,inverse(add(inverse(add(X2,X1)),inverse(add(X2,X3))))))),
inference(cp,[status(thm)],[t4601,t3610]) ).
cnf(t15468,plain,
add(X1,inverse(X1)) = add(add(X2,X1),inverse(add(X2,X1))),
inference(step,[status(thm)],[t4602,t3610]) ).
cnf(t15469,plain,
add(X1,inverse(X1)) = add(X2,inverse(X2)),
inference(step,[status(thm)],[t15468,t4601]) ).
cnf(t4680,plain,
add(X1,inverse(X1)) = add(X2,inverse(X2)),
inference(orient,[status(thm)],[t15469]) ).
cnf(t15475,plain,
add(c,inverse(c)) = add(add(X1,X2),inverse(X2)),
inference(step,[status(thm)],[t4376,t4680]) ).
cnf(t15476,plain,
add(c,inverse(c)) = add(inverse(X2),add(X1,X2)),
inference(step,[status(thm)],[t15475,t2969]) ).
cnf(t4864,plain,
add(inverse(X1),add(X2,X1)) = add(c,inverse(c)),
inference(orient,[status(thm)],[t15476]) ).
cnf(t4914,plain,
add(inverse(X1),add(X2,X1)) = add(add(X2,X1),inverse(add(inverse(add(inverse(X1),X3)),inverse(add(c,inverse(c)))))),
inference(cp,[status(thm)],[t3382,t4864]) ).
cnf(t5015,plain,
add(add(X1,X2),add(X3,inverse(X2))) = add(c,inverse(c)),
inference(orient,[status(thm)],[t4914]) ).
cnf(t5039,plain,
add(c,inverse(c)) = add(X1,add(X2,inverse(inverse(add(X3,inverse(X1)))))),
inference(cp,[status(thm)],[t5015,t2085]) ).
cnf(t15480,plain,
add(c,inverse(c)) = add(X1,add(X2,add(X3,inverse(X1)))),
inference(step,[status(thm)],[t5039,t1184]) ).
cnf(t5109,plain,
add(X1,add(X2,add(X3,inverse(X1)))) = add(c,inverse(c)),
inference(orient,[status(thm)],[t15480]) ).
cnf(t5150,plain,
add(X1,inverse(add(X2,add(X3,inverse(X1))))) = add(X1,inverse(add(c,inverse(c)))),
inference(cp,[status(thm)],[t4293,t5109]) ).
cnf(t4689,plain,
add(X1,inverse(inverse(X1))) = add(X1,inverse(add(X2,inverse(X2)))),
inference(cp,[status(thm)],[t4293,t4680]) ).
cnf(t15470,plain,
add(X1,X1) = add(X1,inverse(add(X2,inverse(X2)))),
inference(step,[status(thm)],[t4689,t1184]) ).
cnf(t15471,plain,
X1 = add(X1,inverse(add(X2,inverse(X2)))),
inference(step,[status(thm)],[t15470,t1164]) ).
cnf(t4734,plain,
add(X1,inverse(add(X2,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t15471]) ).
cnf(t15481,plain,
add(X1,inverse(add(X2,add(X3,inverse(X1))))) = X1,
inference(step,[status(thm)],[t5150,t4734]) ).
cnf(t5174,plain,
add(X1,inverse(add(X2,add(X3,inverse(X1))))) = X1,
inference(orient,[status(thm)],[t15481]) ).
cnf(t5188,plain,
add(X1,inverse(X2)) = add(add(X1,inverse(X2)),inverse(add(X3,X2))),
inference(cp,[status(thm)],[t5174,t2085]) ).
cnf(t15503,plain,
add(X1,inverse(X2)) = add(add(X1,inverse(X2)),inverse(add(X2,X3))),
inference(step,[status(thm)],[t5188,t2969]) ).
cnf(t6071,plain,
add(add(X1,inverse(X2)),inverse(add(X2,X3))) = add(X1,inverse(X2)),
inference(orient,[status(thm)],[t15503]) ).
cnf(t15516,plain,
add(X2,inverse(X1)) = add(inverse(add(X1,X2)),inverse(inverse(X2))),
inference(step,[status(thm)],[t15515,t6071]) ).
cnf(t15517,plain,
add(X2,inverse(X1)) = add(inverse(inverse(X2)),inverse(add(X1,X2))),
inference(step,[status(thm)],[t15516,t2969]) ).
cnf(t15518,plain,
add(X2,inverse(X1)) = add(X2,inverse(add(X1,X2))),
inference(step,[status(thm)],[t15517,t1184]) ).
cnf(t6563,plain,
add(X1,inverse(add(X2,X1))) = add(X1,inverse(X2)),
inference(orient,[status(thm)],[t15518]) ).
cnf(t15595,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(X2,inverse(X1)),
inference(step,[status(thm)],[t15594,t6563]) ).
cnf(t12485,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(X2,inverse(X1)),
inference(orient,[status(thm)],[t15595]) ).
cnf(t12727,plain,
add(inverse(add(X1,X2)),add(X2,inverse(add(X1,X3)))) = add(add(X2,inverse(add(X1,X3))),add(X2,inverse(X1))),
inference(cp,[status(thm)],[t2995,t12485]) ).
cnf(t15596,plain,
add(X2,inverse(X1)) = add(add(X2,inverse(add(X1,X3))),add(X2,inverse(X1))),
inference(step,[status(thm)],[t12727,t12485]) ).
cnf(t15597,plain,
add(X2,inverse(X1)) = add(add(X2,inverse(X1)),add(X2,inverse(add(X1,X3)))),
inference(step,[status(thm)],[t15596,t2969]) ).
cnf(t13142,plain,
add(add(X1,inverse(X2)),add(X1,inverse(add(X2,X3)))) = add(X1,inverse(X2)),
inference(orient,[status(thm)],[t15597]) ).
cnf(t13210,plain,
add(X1,inverse(inverse(add(X2,X3)))) = add(add(X1,inverse(inverse(add(X2,X3)))),add(X3,X1)),
inference(cp,[status(thm)],[t13142,t3322]) ).
cnf(t15598,plain,
add(X1,add(X2,X3)) = add(add(X1,inverse(inverse(add(X2,X3)))),add(X3,X1)),
inference(step,[status(thm)],[t13210,t1184]) ).
cnf(t15599,plain,
add(X1,add(X2,X3)) = add(add(X3,X1),add(X1,inverse(inverse(add(X2,X3))))),
inference(step,[status(thm)],[t15598,t2969]) ).
cnf(t15600,plain,
add(X1,add(X2,X3)) = add(add(X1,X3),add(X1,inverse(inverse(add(X2,X3))))),
inference(step,[status(thm)],[t15599,t2969]) ).
cnf(t15601,plain,
add(X1,add(X2,X3)) = add(add(X1,X3),add(X1,add(X2,X3))),
inference(step,[status(thm)],[t15600,t1184]) ).
cnf(t13361,plain,
add(add(X1,X2),add(X1,add(X3,X2))) = add(X1,add(X3,X2)),
inference(orient,[status(thm)],[t15601]) ).
cnf(t13482,plain,
inverse(add(X1,X2)) = add(inverse(add(X1,X2)),inverse(add(X1,add(X3,X2)))),
inference(cp,[status(thm)],[t2999,t13361]) ).
cnf(t15609,plain,
inverse(add(X1,X2)) = add(inverse(add(X1,X2)),inverse(add(X1,add(X2,X3)))),
inference(step,[status(thm)],[t13482,t2969]) ).
cnf(t14298,plain,
add(inverse(add(X1,X2)),inverse(add(X1,add(X2,X3)))) = inverse(add(X1,X2)),
inference(orient,[status(thm)],[t15609]) ).
cnf(t14485,plain,
add(X1,add(X2,X3)) = add(add(X2,X3),inverse(inverse(add(X1,X2)))),
inference(cp,[status(thm)],[t3382,t14298]) ).
cnf(t15610,plain,
add(X1,add(X2,X3)) = add(add(X2,X3),add(X1,X2)),
inference(step,[status(thm)],[t14485,t1184]) ).
cnf(t15611,plain,
add(X1,add(X2,X3)) = add(add(X1,X2),add(X2,X3)),
inference(step,[status(thm)],[t15610,t2969]) ).
cnf(t14509,plain,
add(add(X1,X2),add(X2,X3)) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t15611]) ).
cnf(t14617,plain,
add(X1,add(X2,inverse(add(inverse(add(X3,X2)),inverse(add(X3,X4)))))) = add(add(X1,X2),add(X3,X2)),
inference(cp,[status(thm)],[t14509,t3610]) ).
cnf(t15612,plain,
add(X1,add(X3,X2)) = add(add(X1,X2),add(X3,X2)),
inference(step,[status(thm)],[t14617,t3610]) ).
cnf(t14736,plain,
add(add(X1,X2),add(X3,X2)) = add(X1,add(X3,X2)),
inference(orient,[status(thm)],[t15612]) ).
cnf(t14798,plain,
add(X1,add(X2,X3)) = add(add(X3,X1),add(X2,X3)),
inference(cp,[status(thm)],[t14736,t2969]) ).
cnf(t15617,plain,
add(X1,add(X2,X3)) = add(add(X2,X3),add(X3,X1)),
inference(step,[status(thm)],[t14798,t2969]) ).
cnf(t15618,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(step,[status(thm)],[t15617,t14509]) ).
cnf(t15619,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t15618,t2969]) ).
cnf(t15128,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t15619]) ).
cnf(goal_0,negated_conjecture,
add(add(a,b),c) != add(a,add(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(rw,[status(thm)],[goal_0,t2969]) ).
cnf(g0_1,plain,
add(c,add(b,a)) != add(a,add(b,c)),
inference(rw,[status(thm)],[g0_0,t2969]) ).
cnf(g0_2,plain,
add(c,add(b,a)) != add(b,add(a,c)),
inference(rw,[status(thm)],[g0_1,t15128]) ).
cnf(g0_3,plain,
add(c,add(b,a)) != add(b,add(c,a)),
inference(rw,[status(thm)],[g0_2,t2969]) ).
cnf(g0_4,plain,
add(c,add(b,a)) != add(c,add(b,a)),
inference(rw,[status(thm)],[g0_3,t15128]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO073-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Fri Sep 25 06:40:22 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.33/2.28 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.33/2.28 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------