%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO038-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:10 AM UTC 2026
% Result : Unsatisfiable 13.18s 12.31s
% Output : CNFRefutation 13.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 2
% Syntax : Number of formulae : 207 ( 199 unt; 0 def)
% Number of atoms : 220 ( 219 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 36 ( 23 ~; 13 |; 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 : 478 ( 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,axiom,
( add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a
| add(add(a,b),c) != add(a,add(b,c))
| add(b,a) != add(a,b) ),
file('theBenchmark.p',huntinton) ).
cnf(c_2,plain,
( add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a
| add(add(a,b),c) != add(a,add(b,c))
| add(b,a) != add(a,b) ),
inference(clausify,[status(thm)],[huntinton]) ).
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_2650,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_2650]) ).
cnf(c_2651,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_2652,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_2651]) ).
cnf(c_2653,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_2652]) ).
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_2653]) ).
cnf(c_2654,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_2655,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_2654]) ).
cnf(c_2656,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_2655]) ).
cnf(c_2657,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_2656]) ).
cnf(c_2658,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_2657]) ).
cnf(c_172,plain,
inverse(add(A,A)) = inverse(A),
inference(paramod,[status(thm)],[c_5,c_2658]) ).
cnf(c_2659,plain,
inverse(add(inverse(A),inverse(add(A,A)))) = A,
inference(paramod,[status(thm)],[c_172,c_85]) ).
cnf(c_2660,plain,
inverse(add(inverse(A),inverse(A))) = A,
inference(paramod,[status(thm)],[c_172,c_2659]) ).
cnf(c_193,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_172,c_2660]) ).
cnf(c_2661,plain,
inverse(add(inverse(A),inverse(add(A,A)))) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_158]) ).
cnf(c_2662,plain,
inverse(add(inverse(A),inverse(A))) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_2661]) ).
cnf(c_2663,plain,
inverse(inverse(A)) = add(A,A),
inference(paramod,[status(thm)],[c_172,c_2662]) ).
cnf(c_2664,plain,
A = add(A,A),
inference(paramod,[status(thm)],[c_193,c_2663]) ).
cnf(c_198,plain,
add(A,A) = A,
inference(copy,[status(thm)],[c_2664]) ).
cnf(c_2665,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_2666,plain,
inverse(add(A,A)) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_56,c_2665]) ).
cnf(c_2667,plain,
inverse(A) = add(inverse(add(B,A)),inverse(add(inverse(add(C,B)),A))),
inference(paramod,[status(thm)],[c_198,c_2666]) ).
cnf(c_205,plain,
add(inverse(add(A,B)),inverse(add(inverse(add(C,A)),B))) = inverse(B),
inference(copy,[status(thm)],[c_2667]) ).
cnf(c_2668,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_2669,plain,
inverse(add(A,A)) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_32,c_2668]) ).
cnf(c_2670,plain,
inverse(A) = add(inverse(add(B,A)),inverse(add(inverse(B),A))),
inference(paramod,[status(thm)],[c_198,c_2669]) ).
cnf(c_213,plain,
add(inverse(add(A,B)),inverse(add(inverse(A),B))) = inverse(B),
inference(copy,[status(thm)],[c_2670]) ).
cnf(c_2671,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_2672,plain,
inverse(add(A,A)) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_15,c_2671]) ).
cnf(c_2673,plain,
inverse(A) = add(inverse(add(inverse(add(B,C)),A)),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_198,c_2672]) ).
cnf(c_215,plain,
add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,C))) = inverse(C),
inference(copy,[status(thm)],[c_2673]) ).
cnf(c_2674,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_2674]) ).
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_2675,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_2676,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_2675]) ).
cnf(c_2677,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_2676]) ).
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_2677]) ).
cnf(c_2678,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_2679,plain,
add(inverse(add(A,inverse(add(B,A)))),A) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_193,c_2678]) ).
cnf(c_292,plain,
add(inverse(add(A,inverse(add(B,A)))),A) = add(B,A),
inference(paramod,[status(thm)],[c_193,c_2679]) ).
cnf(c_2680,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_2681,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_2680]) ).
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_2681]) ).
cnf(c_2682,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_2683,plain,
add(A,inverse(add(inverse(B),inverse(add(B,A))))) = inverse(inverse(add(B,A))),
inference(paramod,[status(thm)],[c_193,c_2682]) ).
cnf(c_344,plain,
add(A,inverse(add(inverse(B),inverse(add(B,A))))) = add(B,A),
inference(paramod,[status(thm)],[c_193,c_2683]) ).
cnf(c_2684,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_2685,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_2684]) ).
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_2685]) ).
cnf(c_2686,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_2686]) ).
cnf(c_2687,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_2687]) ).
cnf(c_2688,plain,
add(inverse(inverse(A)),inverse(add(B,inverse(A)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_355,c_215]) ).
cnf(c_2689,plain,
add(A,inverse(add(B,inverse(A)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_193,c_2688]) ).
cnf(c_367,plain,
add(A,inverse(add(B,inverse(A)))) = A,
inference(paramod,[status(thm)],[c_193,c_2689]) ).
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_2690,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_2690]) ).
cnf(c_2691,plain,
( add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a
| add(add(a,b),c) != add(a,add(b,c))
| add(a,b) != add(a,b) ),
inference(paramod,[status(thm)],[c_397,c_2]) ).
cnf(c_2692,plain,
( add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a
| add(c,add(a,b)) != add(a,add(b,c))
| add(a,b) != add(a,b) ),
inference(paramod,[status(thm)],[c_397,c_2691]) ).
cnf(c_2693,plain,
( add(inverse(add(b,inverse(a))),inverse(add(inverse(a),inverse(b)))) != a
| add(c,add(a,b)) != add(a,add(b,c))
| add(a,b) != add(a,b) ),
inference(paramod,[status(thm)],[c_397,c_2692]) ).
cnf(c_445,plain,
( add(inverse(add(b,inverse(a))),inverse(add(inverse(a),inverse(b)))) != a
| add(c,add(a,b)) != add(a,add(b,c)) ),
inference(copy,[status(thm)],[c_2693]) ).
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_447,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(A)))) = inverse(B),
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_2694,plain,
( inverse(inverse(a)) != a
| add(c,add(a,b)) != add(a,add(b,c)) ),
inference(paramod,[status(thm)],[c_447,c_445]) ).
cnf(c_2695,plain,
( a != a
| add(c,add(a,b)) != add(a,add(b,c)) ),
inference(paramod,[status(thm)],[c_193,c_2694]) ).
cnf(c_450,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(copy,[status(thm)],[c_2695]) ).
cnf(c_453,plain,
add(inverse(A),inverse(add(A,B))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_374]) ).
cnf(c_472,plain,
add(inverse(add(A,B)),inverse(add(A,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_397,c_446]) ).
cnf(c_2696,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_472,c_446]) ).
cnf(c_2697,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_2696]) ).
cnf(c_2698,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_2697]) ).
cnf(c_490,plain,
add(A,inverse(add(add(A,inverse(B)),inverse(add(A,B))))) = add(A,B),
inference(paramod,[status(thm)],[c_193,c_2698]) ).
cnf(c_503,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_504,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_2699,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_2700,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_2699]) ).
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_2700]) ).
cnf(c_2701,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_504,c_249]) ).
cnf(c_2702,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_2701]) ).
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_2702]) ).
cnf(c_2703,plain,
add(A,inverse(inverse(A))) = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_503,c_296]) ).
cnf(c_2704,plain,
add(A,A) = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_193,c_2703]) ).
cnf(c_2705,plain,
A = add(inverse(add(inverse(add(B,A)),B)),A),
inference(paramod,[status(thm)],[c_198,c_2704]) ).
cnf(c_2706,plain,
A = add(inverse(add(B,inverse(add(B,A)))),A),
inference(paramod,[status(thm)],[c_397,c_2705]) ).
cnf(c_2707,plain,
A = add(A,inverse(add(B,inverse(add(B,A))))),
inference(paramod,[status(thm)],[c_397,c_2706]) ).
cnf(c_761,plain,
add(A,inverse(add(B,inverse(add(B,A))))) = A,
inference(copy,[status(thm)],[c_2707]) ).
cnf(c_2708,plain,
add(inverse(add(A,B)),inverse(add(inverse(B),inverse(inverse(B))))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_374,c_761]) ).
cnf(c_2709,plain,
add(inverse(add(A,B)),inverse(add(inverse(B),B))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2708]) ).
cnf(c_780,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(B)))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_397,c_2709]) ).
cnf(c_2710,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_780,c_205]) ).
cnf(c_2711,plain,
add(inverse(A),inverse(inverse(add(B,A)))) = inverse(inverse(add(A,inverse(A)))),
inference(paramod,[status(thm)],[c_367,c_2710]) ).
cnf(c_2712,plain,
add(inverse(A),add(B,A)) = inverse(inverse(add(A,inverse(A)))),
inference(paramod,[status(thm)],[c_193,c_2711]) ).
cnf(c_821,plain,
add(inverse(A),add(B,A)) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_193,c_2712]) ).
cnf(c_2713,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_453,c_780]) ).
cnf(c_2714,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_2713]) ).
cnf(c_2715,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_2714]) ).
cnf(c_2716,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_2715]) ).
cnf(c_2717,plain,
add(A,inverse(add(add(A,B),inverse(add(A,B))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_453,c_2716]) ).
cnf(c_825,plain,
add(A,inverse(add(add(A,B),inverse(add(A,B))))) = A,
inference(paramod,[status(thm)],[c_193,c_2717]) ).
cnf(c_2718,plain,
add(A,add(B,inverse(A))) = add(inverse(A),inverse(inverse(A))),
inference(paramod,[status(thm)],[c_193,c_821]) ).
cnf(c_2719,plain,
add(A,add(B,inverse(A))) = add(inverse(A),A),
inference(paramod,[status(thm)],[c_193,c_2718]) ).
cnf(c_845,plain,
add(A,add(B,inverse(A))) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_397,c_2719]) ).
cnf(c_850,plain,
add(inverse(A),add(A,B)) = add(A,inverse(A)),
inference(paramod,[status(thm)],[c_397,c_821]) ).
cnf(c_2720,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_821]) ).
cnf(c_2721,plain,
add(add(A,B),inverse(B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2720]) ).
cnf(c_2722,plain,
add(inverse(B),add(A,B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_397,c_2721]) ).
cnf(c_2723,plain,
add(B,inverse(B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_821,c_2722]) ).
cnf(c_2724,plain,
add(B,inverse(B)) = add(inverse(add(A,B)),add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2723]) ).
cnf(c_2725,plain,
add(B,inverse(B)) = add(add(A,B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_397,c_2724]) ).
cnf(c_851,plain,
add(add(A,B),inverse(add(A,B))) = add(B,inverse(B)),
inference(copy,[status(thm)],[c_2725]) ).
cnf(c_2726,plain,
add(inverse(inverse(add(A,B))),inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_453,c_821]) ).
cnf(c_2727,plain,
add(add(A,B),inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2726]) ).
cnf(c_2728,plain,
add(inverse(A),add(A,B)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_397,c_2727]) ).
cnf(c_2729,plain,
add(A,inverse(A)) = add(inverse(add(A,B)),inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_850,c_2728]) ).
cnf(c_2730,plain,
add(A,inverse(A)) = add(inverse(add(A,B)),add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2729]) ).
cnf(c_2731,plain,
add(A,inverse(A)) = add(add(A,B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_397,c_2730]) ).
cnf(c_852,plain,
add(A,inverse(A)) = add(B,inverse(B)),
inference(paramod,[status(thm)],[c_851,c_2731]) ).
cnf(c_2732,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_821,c_503]) ).
cnf(c_2733,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_2732]) ).
cnf(c_864,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_2733]) ).
cnf(c_877,plain,
add(A,inverse(add(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_851,c_825]) ).
cnf(c_2734,plain,
add(inverse(add(A,inverse(A))),inverse(add(inverse(B),inverse(B)))) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_852,c_213]) ).
cnf(c_2735,plain,
add(inverse(add(A,inverse(A))),inverse(inverse(B))) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_198,c_2734]) ).
cnf(c_2736,plain,
add(inverse(add(A,inverse(A))),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_193,c_2735]) ).
cnf(c_882,plain,
add(inverse(add(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_193,c_2736]) ).
cnf(c_888,plain,
inverse(add(inverse(A),inverse(add(add(B,A),C)))) = A,
inference(paramod,[status(thm)],[c_882,c_864]) ).
cnf(c_2737,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_888,c_615]) ).
cnf(c_2738,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_2737]) ).
cnf(c_898,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_2738]) ).
cnf(c_2739,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_888,c_552]) ).
cnf(c_2740,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_2739]) ).
cnf(c_899,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_2740]) ).
cnf(c_2741,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_845,c_205]) ).
cnf(c_933,plain,
inverse(add(inverse(add(A,B)),add(C,inverse(B)))) = inverse(add(C,inverse(B))),
inference(paramod,[status(thm)],[c_882,c_2741]) ).
cnf(c_2742,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_845,c_449]) ).
cnf(c_937,plain,
inverse(add(add(A,inverse(B)),inverse(add(C,B)))) = inverse(add(A,inverse(B))),
inference(paramod,[status(thm)],[c_882,c_2742]) ).
cnf(c_2743,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_845,c_296]) ).
cnf(c_2744,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_877,c_2743]) ).
cnf(c_2745,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_933,c_2744]) ).
cnf(c_2746,plain,
add(A,inverse(B)) = add(inverse(add(D,B)),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_367,c_2745]) ).
cnf(c_942,plain,
add(inverse(add(A,B)),add(C,inverse(B))) = add(C,inverse(B)),
inference(copy,[status(thm)],[c_2746]) ).
cnf(c_943,plain,
add(A,inverse(add(A,inverse(B)))) = add(A,B),
inference(paramod,[status(thm)],[c_937,c_490]) ).
cnf(c_948,plain,
add(add(A,B),inverse(add(B,inverse(add(C,A))))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_943,c_899]) ).
cnf(c_949,plain,
add(add(A,B),inverse(add(B,inverse(add(A,C))))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_943,c_898]) ).
cnf(c_2747,plain,
add(inverse(inverse(A)),add(B,inverse(inverse(add(A,C))))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_453,c_942]) ).
cnf(c_2748,plain,
add(A,add(B,inverse(inverse(add(A,C))))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_193,c_2747]) ).
cnf(c_2749,plain,
add(A,add(B,add(A,C))) = add(B,inverse(inverse(add(A,C)))),
inference(paramod,[status(thm)],[c_193,c_2748]) ).
cnf(c_1042,plain,
add(A,add(B,add(A,C))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_193,c_2749]) ).
cnf(c_1060,plain,
add(A,inverse(add(A,B))) = add(A,inverse(B)),
inference(paramod,[status(thm)],[c_193,c_943]) ).
cnf(c_2750,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_943]) ).
cnf(c_2751,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_2750]) ).
cnf(c_2752,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_2751]) ).
cnf(c_2753,plain,
add(A,inverse(B)) = add(inverse(add(A,B)),add(inverse(add(C,B)),A)),
inference(paramod,[status(thm)],[c_1060,c_2752]) ).
cnf(c_1070,plain,
add(inverse(add(A,B)),add(inverse(add(C,B)),A)) = add(A,inverse(B)),
inference(copy,[status(thm)],[c_2753]) ).
cnf(c_1116,plain,
add(A,inverse(add(B,A))) = add(A,inverse(B)),
inference(paramod,[status(thm)],[c_397,c_1060]) ).
cnf(c_2754,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_1070,c_351]) ).
cnf(c_2755,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_2754]) ).
cnf(c_2756,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_2755]) ).
cnf(c_2328,plain,
add(inverse(A),add(inverse(add(B,A)),C)) = add(C,inverse(A)),
inference(paramod,[status(thm)],[c_1070,c_2756]) ).
cnf(c_2757,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_2328]) ).
cnf(c_2758,plain,
add(add(A,B),add(inverse(inverse(B)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2757]) ).
cnf(c_2759,plain,
add(add(A,B),add(B,C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2758]) ).
cnf(c_2418,plain,
add(add(A,B),add(B,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2759]) ).
cnf(c_2760,plain,
add(inverse(inverse(add(A,B))),add(inverse(inverse(A)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_453,c_2328]) ).
cnf(c_2761,plain,
add(add(A,B),add(inverse(inverse(A)),C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2760]) ).
cnf(c_2762,plain,
add(add(A,B),add(A,C)) = add(C,inverse(inverse(add(A,B)))),
inference(paramod,[status(thm)],[c_193,c_2761]) ).
cnf(c_2419,plain,
add(add(A,B),add(A,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_193,c_2762]) ).
cnf(c_2763,plain,
add(add(A,B),inverse(add(C,add(A,B)))) = add(add(A,B),inverse(add(B,C))),
inference(paramod,[status(thm)],[c_2418,c_1060]) ).
cnf(c_2764,plain,
add(add(A,B),inverse(C)) = add(add(A,B),inverse(add(B,C))),
inference(paramod,[status(thm)],[c_1116,c_2763]) ).
cnf(c_2593,plain,
add(add(A,B),inverse(add(B,C))) = add(add(A,B),inverse(C)),
inference(copy,[status(thm)],[c_2764]) ).
cnf(c_2765,plain,
add(add(A,B),inverse(inverse(add(A,C)))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_2593,c_949]) ).
cnf(c_2766,plain,
add(add(A,B),add(A,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_193,c_2765]) ).
cnf(c_2647,plain,
add(A,add(B,C)) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_2419,c_2766]) ).
cnf(c_2767,plain,
add(add(A,B),inverse(inverse(add(C,A)))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_2593,c_948]) ).
cnf(c_2768,plain,
add(add(A,B),add(C,A)) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_193,c_2767]) ).
cnf(c_2769,plain,
add(A,add(C,add(A,B))) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_2647,c_2768]) ).
cnf(c_2648,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_1042,c_2769]) ).
cnf(c_2770,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(copy,[status(thm)],[c_450]) ).
cnf(c_2649,plain,
$false,
inference(resolve,[status(thm)],[c_2648,c_2770]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO038-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n019.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Sat Sep 26 22:39:02 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.38 % Process 2369510 was started by sandbox on n019,
% 0.10/10.38 % Sat Sep 26 22:39:02 2026
% 0.10/10.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/10.38
% 0.10/10.38 % From the command line: assign(max_seconds, 300).
% 13.18/12.31
% 13.18/12.31 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 13.18/12.31
% 13.18/12.31 % SZS status Unsatisfiable for theBenchmark
% 13.18/12.31
% 13.18/12.31 % Proof 1 at 1.48 (+ 0.40) seconds.
% 13.18/12.31 % Length of proof is 84.
% 13.18/12.31 % Level of proof is 37.
% 13.18/12.31 % Maximum clause weight is 96.000.
% 13.18/12.31 % Given clauses 164.
% 13.18/12.31
% 13.18/12.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------