%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO073-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 06:55:13 AM UTC 2026
% Result : Unsatisfiable 8.25s 1.44s
% Output : CNFRefutation 8.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 2
% Syntax : Number of formulae : 200 ( 200 unt; 0 def)
% Number of atoms : 200 ( 199 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 17 ( 3 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 : 476 ( 83 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dn1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : inverse(add(inverse(add(inverse(add(VAR_0,VAR_1)),VAR_2)),inverse(add(VAR_0,inverse(add(inverse(VAR_2),inverse(add(VAR_2,VAR_3)))))))) = VAR_2,
file('theBenchmark.p',dn1) ).
cnf(c_1,plain,
inverse(add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,inverse(add(inverse(C),inverse(add(C,D)))))))) = C,
inference(clausify,[status(thm)],[dn1]) ).
fof(huntinton_2,axiom,
add(add(a,b),c) != add(a,add(b,c)),
file('theBenchmark.p',huntinton_2) ).
cnf(c_2,plain,
add(add(a,b),c) != add(a,add(b,c)),
inference(clausify,[status(thm)],[huntinton_2]) ).
cnf(c_3,plain,
inverse(add(inverse(add(A,B)),inverse(add(inverse(add(inverse(add(C,D)),A)),inverse(add(inverse(B),inverse(add(B,E)))))))) = B,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(A)),B)),A)),C)),inverse(A))),A)) = inverse(A),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_9,plain,
inverse(add(inverse(add(A,inverse(A))),A)) = inverse(A),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_11,plain,
inverse(add(inverse(A),inverse(add(A,inverse(add(inverse(A),inverse(add(A,B)))))))) = A,
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_15,plain,
inverse(add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,C)))) = C,
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_19,plain,
inverse(add(inverse(A),inverse(add(A,A)))) = A,
inference(paramod,[status(thm)],[c_11,c_11]) ).
cnf(c_25,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(A),B)),inverse(add(A,C)))),D)),A)),inverse(add(A,C)))) = A,
inference(paramod,[status(thm)],[c_15,c_1]) ).
cnf(c_32,plain,
inverse(add(inverse(add(A,B)),inverse(add(inverse(A),B)))) = B,
inference(paramod,[status(thm)],[c_11,c_15]) ).
cnf(c_34,plain,
inverse(add(A,inverse(add(add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))))))) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_15,c_19]) ).
cnf(c_52,plain,
inverse(add(A,inverse(add(add(inverse(add(B,A)),inverse(add(inverse(B),A))),add(inverse(add(B,A)),inverse(add(inverse(B),A))))))) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_32,c_19]) ).
cnf(c_55,plain,
inverse(add(inverse(add(A,inverse(add(A,A)))),A)) = inverse(add(A,A)),
inference(paramod,[status(thm)],[c_19,c_32]) ).
cnf(c_56,plain,
inverse(add(inverse(add(A,B)),inverse(add(inverse(add(C,A)),B)))) = B,
inference(paramod,[status(thm)],[c_32,c_15]) ).
cnf(c_85,plain,
inverse(add(inverse(add(A,A)),inverse(add(A,A)))) = A,
inference(paramod,[status(thm)],[c_55,c_15]) ).
cnf(c_112,plain,
inverse(add(inverse(add(inverse(A),A)),inverse(A))) = A,
inference(paramod,[status(thm)],[c_9,c_56]) ).
cnf(c_114,plain,
inverse(add(A,inverse(add(add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))))))) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_56,c_19]) ).
cnf(c_138,plain,
inverse(add(A,inverse(add(inverse(A),inverse(A))))) = inverse(A),
inference(paramod,[status(thm)],[c_112,c_15]) ).
cnf(c_2737,plain,
inverse(add(inverse(A),inverse(add(A,inverse(add(inverse(A),inverse(A))))))) = A,
inference(paramod,[status(thm)],[c_138,c_11]) ).
cnf(c_156,plain,
inverse(add(inverse(A),inverse(A))) = A,
inference(paramod,[status(thm)],[c_138,c_2737]) ).
cnf(c_2738,plain,
inverse(add(inverse(A),inverse(add(add(A,inverse(add(inverse(A),inverse(A)))),add(A,inverse(add(inverse(A),inverse(A)))))))) = add(A,inverse(add(inverse(A),inverse(A)))),
inference(paramod,[status(thm)],[c_138,c_19]) ).
cnf(c_2739,plain,
inverse(add(inverse(A),inverse(add(add(A,A),add(A,inverse(add(inverse(A),inverse(A)))))))) = add(A,inverse(add(inverse(A),inverse(A)))),
inference(paramod,[status(thm)],[c_156,c_2738]) ).
cnf(c_2740,plain,
inverse(add(inverse(A),inverse(add(add(A,A),add(A,A))))) = add(A,inverse(add(inverse(A),inverse(A)))),
inference(paramod,[status(thm)],[c_156,c_2739]) ).
cnf(c_158,plain,
inverse(add(inverse(A),inverse(add(add(A,A),add(A,A))))) = add(A,A),
inference(paramod,[status(thm)],[c_156,c_2740]) ).
cnf(c_2741,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(A,inverse(add(inverse(A),inverse(A)))))),B)),add(A,inverse(add(inverse(A),inverse(A)))))),C)),inverse(add(A,inverse(add(inverse(A),inverse(A))))))),add(A,inverse(add(inverse(A),inverse(A)))))) = inverse(A),
inference(paramod,[status(thm)],[c_138,c_5]) ).
cnf(c_2742,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(A,A))),B)),add(A,inverse(add(inverse(A),inverse(A)))))),C)),inverse(add(A,inverse(add(inverse(A),inverse(A))))))),add(A,inverse(add(inverse(A),inverse(A)))))) = inverse(A),
inference(paramod,[status(thm)],[c_156,c_2741]) ).
cnf(c_2743,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(A,A))),B)),add(A,A))),C)),inverse(add(A,inverse(add(inverse(A),inverse(A))))))),add(A,inverse(add(inverse(A),inverse(A)))))) = inverse(A),
inference(paramod,[status(thm)],[c_156,c_2742]) ).
cnf(c_2744,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(A,A))),B)),add(A,A))),C)),inverse(add(A,A)))),add(A,inverse(add(inverse(A),inverse(A)))))) = inverse(A),
inference(paramod,[status(thm)],[c_156,c_2743]) ).
cnf(c_2745,plain,
inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(A,A))),B)),add(A,A))),C)),inverse(add(A,A)))),add(A,A))) = inverse(A),
inference(paramod,[status(thm)],[c_156,c_2744]) ).
cnf(c_172,plain,
inverse(add(A,A)) = inverse(A),
inference(paramod,[status(thm)],[c_5,c_2745]) ).
cnf(c_2746,plain,
inverse(add(inverse(A),inverse(add(A,A)))) = A,
inference(paramod,[status(thm)],[c_172,c_85]) ).
cnf(c_2747,plain,
inverse(add(inverse(A),inverse(A))) = A,
inference(paramod,[status(thm)],[c_172,c_2746]) ).
cnf(c_193,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_172,c_2747]) ).
cnf(c_2748,plain,
inverse(add(inverse(A),inverse(add(A,A)))) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_158]) ).
cnf(c_2749,plain,
inverse(add(inverse(A),inverse(A))) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_2748]) ).
cnf(c_2750,plain,
inverse(inverse(A)) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_2749]) ).
cnf(c_2751,plain,
A = add(A,A),
inference(paramod,[status(thm)],[c_193,c_2750]) ).
cnf(c_198,plain,
add(A,A) = A,
inference(copy,[status(thm)],[c_2751]) ).
cnf(c_2752,plain,
inverse(add(A,inverse(add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A)))))) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_198,c_114]) ).
cnf(c_2753,plain,
inverse(add(A,A)) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_56,c_2752]) ).
cnf(c_2754,plain,
inverse(A) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_198,c_2753]) ).
cnf(c_205,plain,
add(inverse(add(A,B)),inverse(add(inverse(add(C,A)),B))) = inverse(B),
inference(copy,[status(thm)],[c_2754]) ).
cnf(c_2755,plain,
inverse(add(A,inverse(add(inverse(add(B,A)),inverse(add(inverse(B),A)))))) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_198,c_52]) ).
cnf(c_2756,plain,
inverse(add(A,A)) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_32,c_2755]) ).
cnf(c_2757,plain,
inverse(A) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_198,c_2756]) ).
cnf(c_213,plain,
add(inverse(add(A,B)),inverse(add(inverse(A),B))) = inverse(B),
inference(copy,[status(thm)],[c_2757]) ).
cnf(c_2758,plain,
inverse(add(A,inverse(add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A)))))) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_198,c_34]) ).
cnf(c_2759,plain,
inverse(add(A,A)) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_15,c_2758]) ).
cnf(c_2760,plain,
inverse(A) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_198,c_2759]) ).
cnf(c_215,plain,
add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,C))) = inverse(C),
inference(copy,[status(thm)],[c_2760]) ).
cnf(c_2761,plain,
inverse(A) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,inverse(add(inverse(A),inverse(add(A,D))))))),
inference(paramod,[status(thm)],[c_1,c_193]) ).
cnf(c_241,plain,
add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,inverse(add(inverse(C),inverse(add(C,D))))))) = inverse(C),
inference(copy,[status(thm)],[c_2761]) ).
cnf(c_245,plain,
add(inverse(add(inverse(A),B)),inverse(add(A,B))) = inverse(B),
inference(paramod,[status(thm)],[c_193,c_213]) ).
cnf(c_2762,plain,
add(inverse(inverse(A)),inverse(add(inverse(inverse(add(B,A))),inverse(add(inverse(B),A))))) = inverse(inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_213,c_213]) ).
cnf(c_2763,plain,
add(A,inverse(add(inverse(inverse(add(B,A))),inverse(add(inverse(B),A))))) = inverse(inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_193,c_2762]) ).
cnf(c_2764,plain,
add(A,inverse(add(add(B,A),inverse(add(inverse(B),A))))) = inverse(inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_193,c_2763]) ).
cnf(c_249,plain,
add(A,inverse(add(add(B,A),inverse(add(inverse(B),A))))) = add(inverse(B),A),
inference(paramod,[status(thm)],[c_193,c_2764]) ).
cnf(c_2765,plain,
add(inverse(add(A,inverse(add(B,A)))),inverse(inverse(A))) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_245,c_205]) ).
cnf(c_2766,plain,
add(inverse(add(A,inverse(add(B,A)))),A) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_193,c_2765]) ).
cnf(c_292,plain,
add(inverse(add(A,inverse(add(B,A)))),A) = add(B,A),
inference(paramod,[status(thm)],[c_193,c_2766]) ).
cnf(c_2767,plain,
add(inverse(inverse(A)),inverse(add(inverse(add(B,inverse(add(C,A)))),inverse(add(inverse(add(D,C)),A))))) = inverse(inverse(add(inverse(add(D,C)),A))),
inference(paramod,[status(thm)],[c_205,c_205]) ).
cnf(c_2768,plain,
add(A,inverse(add(inverse(add(B,inverse(add(C,A)))),inverse(add(inverse(add(D,C)),A))))) = inverse(inverse(add(inverse(add(D,C)),A))),
inference(paramod,[status(thm)],[c_193,c_2767]) ).
cnf(c_296,plain,
add(A,inverse(add(inverse(add(B,inverse(add(C,A)))),inverse(add(inverse(add(D,C)),A))))) = add(inverse(add(D,C)),A),
inference(paramod,[status(thm)],[c_193,c_2768]) ).
cnf(c_2769,plain,
add(inverse(inverse(A)),inverse(add(inverse(B),inverse(add(B,A))))) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_245,c_215]) ).
cnf(c_2770,plain,
add(A,inverse(add(inverse(B),inverse(add(B,A))))) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_193,c_2769]) ).
cnf(c_344,plain,
add(A,inverse(add(inverse(B),inverse(add(B,A))))) = add(B,A),
inference(paramod,[status(thm)],[c_193,c_2770]) ).
cnf(c_2771,plain,
add(inverse(inverse(A)),inverse(add(B,inverse(add(inverse(add(C,B)),A))))) = inverse(inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_205,c_215]) ).
cnf(c_2772,plain,
add(A,inverse(add(B,inverse(add(inverse(add(C,B)),A))))) = inverse(inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_193,c_2771]) ).
cnf(c_351,plain,
add(A,inverse(add(B,inverse(add(inverse(add(C,B)),A))))) = add(inverse(add(C,B)),A),
inference(paramod,[status(thm)],[c_193,c_2772]) ).
cnf(c_2773,plain,
add(inverse(add(A,B)),inverse(add(B,B))) = inverse(B),
inference(paramod,[status(thm)],[c_292,c_215]) ).
cnf(c_355,plain,
add(inverse(add(A,B)),inverse(B)) = inverse(B),
inference(paramod,[status(thm)],[c_198,c_2773]) ).
cnf(c_2774,plain,
add(inverse(add(A,inverse(B))),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_193,c_355]) ).
cnf(c_361,plain,
add(inverse(add(A,inverse(B))),B) = B,
inference(paramod,[status(thm)],[c_193,c_2774]) ).
cnf(c_2775,plain,
add(inverse(inverse(A)),inverse(add(B,inverse(A)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_355,c_215]) ).
cnf(c_2776,plain,
add(A,inverse(add(B,inverse(A)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_193,c_2775]) ).
cnf(c_367,plain,
add(A,inverse(add(B,inverse(A)))) = A,
inference(paramod,[status(thm)],[c_193,c_2776]) ).
cnf(c_374,plain,
add(inverse(A),inverse(add(B,A))) = inverse(A),
inference(paramod,[status(thm)],[c_361,c_215]) ).
cnf(c_392,plain,
inverse(add(inverse(A),inverse(add(A,B)))) = A,
inference(paramod,[status(thm)],[c_361,c_25]) ).
cnf(c_397,plain,
add(A,B) = add(B,A),
inference(paramod,[status(thm)],[c_392,c_344]) ).
cnf(c_2777,plain,
add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,C))) = inverse(C),
inference(paramod,[status(thm)],[c_392,c_241]) ).
cnf(c_403,plain,
add(inverse(add(A,B)),inverse(add(inverse(add(A,C)),B))) = inverse(B),
inference(paramod,[status(thm)],[c_397,c_2777]) ).
cnf(c_445,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(paramod,[status(thm)],[c_397,c_2]) ).
cnf(c_446,plain,
add(inverse(add(A,B)),inverse(add(inverse(B),A))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_213]) ).
cnf(c_448,plain,
add(inverse(add(A,B)),inverse(add(inverse(add(C,B)),A))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_205]) ).
cnf(c_449,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(add(C,A))))) = inverse(B),
inference(paramod,[status(thm)],[c_397,c_205]) ).
cnf(c_452,plain,
add(inverse(A),inverse(add(A,B))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_374]) ).
cnf(c_471,plain,
add(inverse(add(A,B)),inverse(add(A,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_446]) ).
cnf(c_2778,plain,
add(inverse(inverse(A)),inverse(add(inverse(inverse(add(A,inverse(B)))),inverse(add(A,B))))) = inverse(inverse(add(A,B))),
inference(paramod,[status(thm)],[c_471,c_446]) ).
cnf(c_2779,plain,
add(A,inverse(add(inverse(inverse(add(A,inverse(B)))),inverse(add(A,B))))) = inverse(inverse(add(A,B))),
inference(paramod,[status(thm)],[c_193,c_2778]) ).
cnf(c_2780,plain,
add(A,inverse(add(add(A,inverse(B)),inverse(add(A,B))))) = inverse(inverse(add(A,B))),
inference(paramod,[status(thm)],[c_193,c_2779]) ).
cnf(c_489,plain,
add(A,inverse(add(add(A,inverse(B)),inverse(add(A,B))))) = add(A,B),
inference(paramod,[status(thm)],[c_193,c_2780]) ).
cnf(c_502,plain,
add(inverse(add(A,B)),inverse(add(inverse(add(B,C)),A))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_403]) ).
cnf(c_503,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(add(A,C))))) = inverse(B),
inference(paramod,[status(thm)],[c_397,c_403]) ).
cnf(c_2781,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(inverse(inverse(add(C,A))),inverse(add(A,inverse(add(B,C))))))))) = add(inverse(inverse(add(C,A))),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_449,c_249]) ).
cnf(c_2782,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(add(C,A),inverse(add(A,inverse(add(B,C))))))))) = add(inverse(inverse(add(C,A))),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_193,c_2781]) ).
cnf(c_552,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(add(C,A),inverse(add(A,inverse(add(B,C))))))))) = add(add(C,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_193,c_2782]) ).
cnf(c_2783,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(inverse(inverse(add(B,A))),inverse(add(A,inverse(add(B,C))))))))) = add(inverse(inverse(add(B,A))),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_503,c_249]) ).
cnf(c_2784,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(add(B,A),inverse(add(A,inverse(add(B,C))))))))) = add(inverse(inverse(add(B,A))),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_193,c_2783]) ).
cnf(c_615,plain,
add(inverse(add(A,inverse(add(B,C)))),inverse(add(inverse(A),inverse(add(add(B,A),inverse(add(A,inverse(add(B,C))))))))) = add(add(B,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_193,c_2784]) ).
cnf(c_2785,plain,
add(A,inverse(inverse(A))) = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_502,c_296]) ).
cnf(c_2786,plain,
add(A,A) = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_193,c_2785]) ).
cnf(c_2787,plain,
A = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_198,c_2786]) ).
cnf(c_2788,plain,
A = add(inverse(add(B,inverse(add(B,A)))),A),
inference(paramod,[status(thm)],[c_397,c_2787]) ).
cnf(c_2789,plain,
A = add(A,inverse(add(B,inverse(add(B,A))))),
inference(paramod,[status(thm)],[c_397,c_2788]) ).
cnf(c_793,plain,
add(A,inverse(add(B,inverse(add(B,A))))) = A,
inference(copy,[status(thm)],[c_2789]) ).
cnf(c_2790,plain,
add(inverse(add(A,B)),inverse(add(inverse(B),inverse(inverse(B))))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_374,c_793]) ).
cnf(c_2791,plain,
add(inverse(add(A,B)),inverse(add(inverse(B),B))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2790]) ).
cnf(c_813,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(B)))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_397,c_2791]) ).
cnf(c_2792,plain,
add(inverse(add(A,inverse(add(A,inverse(A))))),inverse(inverse(add(B,A)))) = inverse(inverse(add(A,inverse(A)))),
inference(paramod,[status(thm)],[c_813,c_205]) ).
cnf(c_2793,plain,
add(inverse(A),inverse(inverse(add(B,A)))) = inverse(inverse(add(A,inverse(A)))),
inference(paramod,[status(thm)],[c_367,c_2792]) ).
cnf(c_2794,plain,
add(inverse(A),add(B,A)) = inverse(inverse(add(A,inverse(A)))),
inference(paramod,[status(thm)],[c_193,c_2793]) ).
cnf(c_856,plain,
add(inverse(A),add(B,A)) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_193,c_2794]) ).
cnf(c_2795,plain,
add(inverse(inverse(A)),inverse(add(inverse(add(A,B)),inverse(inverse(add(A,B)))))) = inverse(add(inverse(A),inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_452,c_813]) ).
cnf(c_2796,plain,
add(A,inverse(add(inverse(add(A,B)),inverse(inverse(add(A,B)))))) = inverse(add(inverse(A),inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2795]) ).
cnf(c_2797,plain,
add(A,inverse(add(inverse(add(A,B)),add(A,B)))) = inverse(add(inverse(A),inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2796]) ).
cnf(c_2798,plain,
add(A,inverse(add(add(A,B),inverse(add(A,B))))) = inverse(add(inverse(A),inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_397,c_2797]) ).
cnf(c_2799,plain,
add(A,inverse(add(add(A,B),inverse(add(A,B))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_452,c_2798]) ).
cnf(c_860,plain,
add(A,inverse(add(add(A,B),inverse(add(A,B))))) = A,
inference(paramod,[status(thm)],[c_193,c_2799]) ).
cnf(c_2800,plain,
add(A,add(B,inverse(A))) = add(inverse(A),inverse(inverse(A))),
inference(paramod,[status(thm)],[c_193,c_856]) ).
cnf(c_2801,plain,
add(A,add(B,inverse(A))) = add(inverse(A),A),
inference(paramod,[status(thm)],[c_193,c_2800]) ).
cnf(c_881,plain,
add(A,add(B,inverse(A))) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_397,c_2801]) ).
cnf(c_886,plain,
add(inverse(A),add(A,B)) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_397,c_856]) ).
cnf(c_2802,plain,
add(inverse(inverse(add(A,B))),inverse(B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_374,c_856]) ).
cnf(c_2803,plain,
add(add(A,B),inverse(B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2802]) ).
cnf(c_2804,plain,
add(inverse(B),add(A,B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_397,c_2803]) ).
cnf(c_2805,plain,
add(B,inverse(B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_856,c_2804]) ).
cnf(c_2806,plain,
add(B,inverse(B)) = add(inverse(add(A,B)),add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2805]) ).
cnf(c_2807,plain,
add(B,inverse(B)) = add(add(A,B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_397,c_2806]) ).
cnf(c_887,plain,
add(add(A,B),inverse(add(A,B))) = add(B,inverse(B)),
inference(copy,[status(thm)],[c_2807]) ).
cnf(c_2808,plain,
add(inverse(inverse(add(A,B))),inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_452,c_856]) ).
cnf(c_2809,plain,
add(add(A,B),inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2808]) ).
cnf(c_2810,plain,
add(inverse(A),add(A,B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_397,c_2809]) ).
cnf(c_2811,plain,
add(A,inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_886,c_2810]) ).
cnf(c_2812,plain,
add(A,inverse(A)) = add(inverse(add(A,B)),add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2811]) ).
cnf(c_2813,plain,
add(A,inverse(A)) = add(add(A,B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_397,c_2812]) ).
cnf(c_888,plain,
add(A,inverse(A)) = add(B,inverse(B)),
inference(paramod,[status(thm)],[c_887,c_2813]) ).
cnf(c_2814,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(add(add(B,A),C)),inverse(A)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_856,c_502]) ).
cnf(c_2815,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(A),inverse(add(add(B,A),C))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_397,c_2814]) ).
cnf(c_897,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(A),inverse(add(add(B,A),C))))) = A,
inference(paramod,[status(thm)],[c_193,c_2815]) ).
cnf(c_915,plain,
add(A,inverse(add(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_887,c_860]) ).
cnf(c_2816,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(B),inverse(B)))) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_888,c_213]) ).
cnf(c_2817,plain,
add(inverse(add(A,inverse(A))),inverse(inverse(B))) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_198,c_2816]) ).
cnf(c_2818,plain,
add(inverse(add(A,inverse(A))),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_193,c_2817]) ).
cnf(c_921,plain,
add(inverse(add(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_193,c_2818]) ).
cnf(c_928,plain,
inverse(add(inverse(A),inverse(add(add(B,A),C)))) = A,
inference(paramod,[status(thm)],[c_921,c_897]) ).
cnf(c_2819,plain,
add(inverse(add(A,inverse(add(B,C)))),A) = add(add(B,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_928,c_615]) ).
cnf(c_2820,plain,
add(A,inverse(add(A,inverse(add(B,C))))) = add(add(B,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_397,c_2819]) ).
cnf(c_937,plain,
add(add(A,B),inverse(add(B,inverse(add(A,C))))) = add(B,inverse(add(B,inverse(add(A,C))))),
inference(copy,[status(thm)],[c_2820]) ).
cnf(c_2821,plain,
add(inverse(add(A,inverse(add(B,C)))),A) = add(add(C,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_928,c_552]) ).
cnf(c_2822,plain,
add(A,inverse(add(A,inverse(add(B,C))))) = add(add(C,A),inverse(add(A,inverse(add(B,C))))),
inference(paramod,[status(thm)],[c_397,c_2821]) ).
cnf(c_938,plain,
add(add(A,B),inverse(add(B,inverse(add(C,A))))) = add(B,inverse(add(B,inverse(add(C,A))))),
inference(copy,[status(thm)],[c_2822]) ).
cnf(c_2823,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(add(B,A)),add(C,inverse(A))))) = inverse(add(C,inverse(A))),
inference(paramod,[status(thm)],[c_881,c_205]) ).
cnf(c_975,plain,
inverse(add(inverse(add(A,B)),add(C,inverse(B)))) = inverse(add(C,inverse(B))),
inference(paramod,[status(thm)],[c_921,c_2823]) ).
cnf(c_2824,plain,
add(inverse(add(A,inverse(A))),inverse(add(add(B,inverse(A)),inverse(add(C,A))))) = inverse(add(B,inverse(A))),
inference(paramod,[status(thm)],[c_881,c_449]) ).
cnf(c_979,plain,
inverse(add(add(A,inverse(B)),inverse(add(C,B)))) = inverse(add(A,inverse(B))),
inference(paramod,[status(thm)],[c_921,c_2824]) ).
cnf(c_2825,plain,
add(add(A,inverse(B)),inverse(add(inverse(add(C,inverse(add(B,inverse(B))))),inverse(add(inverse(add(D,B)),add(A,inverse(B))))))) = add(inverse(add(D,B)),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_881,c_296]) ).
cnf(c_2826,plain,
add(add(A,inverse(B)),inverse(add(inverse(C),inverse(add(inverse(add(D,B)),add(A,inverse(B))))))) = add(inverse(add(D,B)),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_915,c_2825]) ).
cnf(c_2827,plain,
add(add(A,inverse(B)),inverse(add(inverse(C),inverse(add(A,inverse(B)))))) = add(inverse(add(D,B)),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_975,c_2826]) ).
cnf(c_2828,plain,
add(A,inverse(B)) = add(inverse(add(D,B)),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_367,c_2827]) ).
cnf(c_985,plain,
add(inverse(add(A,B)),add(C,inverse(B))) = add(C,inverse(B)),
inference(copy,[status(thm)],[c_2828]) ).
cnf(c_986,plain,
add(A,inverse(add(A,inverse(B)))) = add(A,B),
inference(paramod,[status(thm)],[c_979,c_489]) ).
cnf(c_991,plain,
add(add(A,B),inverse(add(B,inverse(add(C,A))))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_986,c_938]) ).
cnf(c_992,plain,
add(add(A,B),inverse(add(B,inverse(add(A,C))))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_986,c_937]) ).
cnf(c_2829,plain,
add(inverse(inverse(A)),add(B,inverse(inverse(add(A,C))))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_452,c_985]) ).
cnf(c_2830,plain,
add(A,add(B,inverse(inverse(add(A,C))))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_193,c_2829]) ).
cnf(c_2831,plain,
add(A,add(B,add(A,C))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_193,c_2830]) ).
cnf(c_1091,plain,
add(A,add(B,add(A,C))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_193,c_2831]) ).
cnf(c_1109,plain,
add(A,inverse(add(A,B))) = add(A,inverse(B)),
inference(paramod,[status(thm)],[c_193,c_986]) ).
cnf(c_2832,plain,
add(inverse(add(A,B)),inverse(inverse(A))) = add(inverse(add(A,B)),add(inverse(add(C,B)),A)),
inference(paramod,[status(thm)],[c_448,c_986]) ).
cnf(c_2833,plain,
add(inverse(add(A,B)),A) = add(inverse(add(A,B)),add(inverse(add(C,B)),A)),
inference(paramod,[status(thm)],[c_193,c_2832]) ).
cnf(c_2834,plain,
add(A,inverse(add(A,B))) = add(inverse(add(A,B)),add(inverse(add(C,B)),A)),
inference(paramod,[status(thm)],[c_397,c_2833]) ).
cnf(c_2835,plain,
add(A,inverse(B)) = add(inverse(add(A,B)),add(inverse(add(C,B)),A)),
inference(paramod,[status(thm)],[c_1109,c_2834]) ).
cnf(c_1118,plain,
add(inverse(add(A,B)),add(inverse(add(C,B)),A)) = add(A,inverse(B)),
inference(copy,[status(thm)],[c_2835]) ).
cnf(c_1169,plain,
add(A,inverse(add(B,A))) = add(A,inverse(B)),
inference(paramod,[status(thm)],[c_397,c_1109]) ).
cnf(c_2836,plain,
add(add(inverse(add(A,B)),C),inverse(add(B,inverse(add(C,inverse(B)))))) = add(inverse(add(C,B)),add(inverse(add(A,B)),C)),
inference(paramod,[status(thm)],[c_1118,c_351]) ).
cnf(c_2837,plain,
add(add(inverse(add(A,B)),C),inverse(B)) = add(inverse(add(C,B)),add(inverse(add(A,B)),C)),
inference(paramod,[status(thm)],[c_367,c_2836]) ).
cnf(c_2838,plain,
add(inverse(B),add(inverse(add(A,B)),C)) = add(inverse(add(C,B)),add(inverse(add(A,B)),C)),
inference(paramod,[status(thm)],[c_397,c_2837]) ).
cnf(c_2415,plain,
add(inverse(A),add(inverse(add(B,A)),C)) = add(C,inverse(A)),
inference(paramod,[status(thm)],[c_1118,c_2838]) ).
cnf(c_2839,plain,
add(inverse(inverse(add(A,B))),add(inverse(inverse(B)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_374,c_2415]) ).
cnf(c_2840,plain,
add(add(A,B),add(inverse(inverse(B)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2839]) ).
cnf(c_2841,plain,
add(add(A,B),add(B,C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2840]) ).
cnf(c_2505,plain,
add(add(A,B),add(B,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2841]) ).
cnf(c_2842,plain,
add(inverse(inverse(add(A,B))),add(inverse(inverse(A)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_452,c_2415]) ).
cnf(c_2843,plain,
add(add(A,B),add(inverse(inverse(A)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2842]) ).
cnf(c_2844,plain,
add(add(A,B),add(A,C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2843]) ).
cnf(c_2506,plain,
add(add(A,B),add(A,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2844]) ).
cnf(c_2845,plain,
add(add(A,B),inverse(add(C,add(A,B)))) = add(add(A,B),inverse(add(B,C))),
inference(paramod,[status(thm)],[c_2505,c_1109]) ).
cnf(c_2846,plain,
add(add(A,B),inverse(C)) = add(add(A,B),inverse(add(B,C))),
inference(paramod,[status(thm)],[c_1169,c_2845]) ).
cnf(c_2681,plain,
add(add(A,B),inverse(add(B,C))) = add(add(A,B),inverse(C)),
inference(copy,[status(thm)],[c_2846]) ).
cnf(c_2847,plain,
add(add(A,B),inverse(inverse(add(A,C)))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_2681,c_992]) ).
cnf(c_2848,plain,
add(add(A,B),add(A,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_193,c_2847]) ).
cnf(c_2734,plain,
add(A,add(B,C)) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_2506,c_2848]) ).
cnf(c_2849,plain,
add(add(A,B),inverse(inverse(add(C,A)))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_2681,c_991]) ).
cnf(c_2850,plain,
add(add(A,B),add(C,A)) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_193,c_2849]) ).
cnf(c_2851,plain,
add(A,add(C,add(A,B))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_2734,c_2850]) ).
cnf(c_2735,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_1091,c_2851]) ).
cnf(c_2852,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(copy,[status(thm)],[c_445]) ).
cnf(c_2736,plain,
$false,
inference(resolve,[status(thm)],[c_2735,c_2852]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : BOO073-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Sat Sep 26 22:42:19 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.30 % Process 1666067 was started by sandbox2 on n012,
% 0.03/0.30 % Sat Sep 26 22:42:19 2026
% 0.03/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.03/0.30
% 0.03/0.30 % From the command line: assign(max_seconds, 300).
% 8.25/1.44
% 8.25/1.44 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 8.25/1.44
% 8.25/1.44 % SZS status Unsatisfiable for theBenchmark
% 8.25/1.44
% 8.25/1.44 % Proof 1 at 0.80 (+ 0.22) seconds.
% 8.25/1.44 % Length of proof is 82.
% 8.25/1.44 % Level of proof is 37.
% 8.25/1.44 % Maximum clause weight is 96.000.
% 8.25/1.44 % Given clauses 164.
% 8.25/1.44
% 8.25/1.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------