%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:07 AM UTC 2026
% Result : Unsatisfiable 3.62s 0.95s
% Output : CNFRefutation 3.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 4
% Syntax : Number of formulae : 104 ( 69 unt; 0 def)
% Number of atoms : 143 ( 142 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 92 ( 53 ~; 39 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 201 ( 16 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(frink1,axiom,
! [VAR_0] : add(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',frink1) ).
cnf(c_1,plain,
add(A,A) = A,
inference(clausify,[status(thm)],[frink1]) ).
fof(frink2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( add(add(add(VAR_0,VAR_1),VAR_2),inverse(VAR_3)) = n0
| add(add(add(VAR_0,VAR_1),VAR_2),VAR_3) != add(add(VAR_1,VAR_2),VAR_0) ),
file('theBenchmark.p',frink2) ).
cnf(c_2,plain,
( add(add(add(A,B),C),inverse(D)) = n0
| add(add(add(A,B),C),D) != add(add(B,C),A) ),
inference(clausify,[status(thm)],[frink2]) ).
fof(frink3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( add(add(add(VAR_0,VAR_1),VAR_2),VAR_3) = add(add(VAR_1,VAR_2),VAR_0)
| add(add(add(VAR_0,VAR_1),VAR_2),inverse(VAR_3)) != n0 ),
file('theBenchmark.p',frink3) ).
cnf(c_3,plain,
( add(add(add(A,B),C),D) = add(add(B,C),A)
| add(add(add(A,B),C),inverse(D)) != n0 ),
inference(clausify,[status(thm)],[frink3]) ).
fof(prove_huntington,axiom,
( add(b,a) != add(a,b)
| add(add(a,b),c) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
file('theBenchmark.p',prove_huntington) ).
cnf(c_4,plain,
( add(b,a) != add(a,b)
| add(add(a,b),c) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(clausify,[status(thm)],[prove_huntington]) ).
cnf(c_714,plain,
add(add(add(A,A),A),inverse(add(add(A,A),A))) = n0,
inference(resolve,[status(thm)],[c_2,c_1]) ).
cnf(c_715,plain,
add(add(A,A),inverse(add(add(A,A),A))) = n0,
inference(paramod,[status(thm)],[c_1,c_714]) ).
cnf(c_716,plain,
add(A,inverse(add(add(A,A),A))) = n0,
inference(paramod,[status(thm)],[c_1,c_715]) ).
cnf(c_717,plain,
add(A,inverse(add(A,A))) = n0,
inference(paramod,[status(thm)],[c_1,c_716]) ).
cnf(c_5,plain,
add(A,inverse(A)) = n0,
inference(paramod,[status(thm)],[c_1,c_717]) ).
cnf(c_718,plain,
add(add(add(A,B),C),add(add(A,B),C)) = add(add(B,C),A),
inference(resolve,[status(thm)],[c_5,c_3]) ).
cnf(c_719,plain,
add(add(A,B),C) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_1,c_718]) ).
cnf(c_12,plain,
add(add(A,B),C) = add(add(C,A),B),
inference(copy,[status(thm)],[c_719]) ).
cnf(c_720,plain,
( add(add(add(B,C),inverse(add(B,C))),A) = add(add(C,inverse(add(B,C))),B)
| add(n0,inverse(A)) != n0 ),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_721,plain,
( add(n0,A) = add(add(C,inverse(add(B,C))),B)
| add(n0,inverse(A)) != n0 ),
inference(paramod,[status(thm)],[c_5,c_720]) ).
cnf(c_722,plain,
( add(n0,A) = add(add(B,C),inverse(add(B,C)))
| add(n0,inverse(A)) != n0 ),
inference(paramod,[status(thm)],[c_12,c_721]) ).
cnf(c_18,plain,
( add(n0,A) = n0
| add(n0,inverse(A)) != n0 ),
inference(paramod,[status(thm)],[c_5,c_722]) ).
cnf(c_723,plain,
add(A,B) = add(add(B,A),A),
inference(paramod,[status(thm)],[c_1,c_12]) ).
cnf(c_26,plain,
add(add(A,B),B) = add(B,A),
inference(copy,[status(thm)],[c_723]) ).
cnf(c_27,plain,
add(add(A,B),A) = add(A,B),
inference(paramod,[status(thm)],[c_1,c_12]) ).
cnf(c_44,plain,
add(add(inverse(A),B),A) = add(n0,B),
inference(paramod,[status(thm)],[c_5,c_12]) ).
cnf(c_724,plain,
add(n0,inverse(A)) = add(inverse(A),A),
inference(paramod,[status(thm)],[c_5,c_26]) ).
cnf(c_56,plain,
add(inverse(A),A) = add(n0,inverse(A)),
inference(copy,[status(thm)],[c_724]) ).
cnf(c_725,plain,
add(add(add(A,B),C),A) = add(A,add(B,C)),
inference(paramod,[status(thm)],[c_12,c_26]) ).
cnf(c_59,plain,
add(add(A,B),add(B,C)) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_12,c_725]) ).
cnf(c_726,plain,
add(add(A,B),A) = add(A,add(B,A)),
inference(paramod,[status(thm)],[c_26,c_26]) ).
cnf(c_727,plain,
add(A,B) = add(A,add(B,A)),
inference(paramod,[status(thm)],[c_27,c_726]) ).
cnf(c_61,plain,
add(A,add(B,A)) = add(A,B),
inference(copy,[status(thm)],[c_727]) ).
cnf(c_728,plain,
add(add(A,add(B,A)),add(B,A)) = add(A,B),
inference(paramod,[status(thm)],[c_26,c_26]) ).
cnf(c_729,plain,
add(add(A,B),add(B,A)) = add(A,B),
inference(paramod,[status(thm)],[c_61,c_728]) ).
cnf(c_730,plain,
add(B,add(A,A)) = add(A,B),
inference(paramod,[status(thm)],[c_59,c_729]) ).
cnf(c_62,plain,
add(A,B) = add(B,A),
inference(paramod,[status(thm)],[c_1,c_730]) ).
cnf(c_731,plain,
add(add(A,B),A) = add(A,add(B,A)),
inference(paramod,[status(thm)],[c_26,c_26]) ).
cnf(c_732,plain,
add(A,add(A,B)) = add(A,add(B,A)),
inference(paramod,[status(thm)],[c_62,c_731]) ).
cnf(c_63,plain,
add(A,add(A,B)) = add(A,B),
inference(paramod,[status(thm)],[c_61,c_732]) ).
cnf(c_733,plain,
add(A,inverse(A)) = add(n0,inverse(A)),
inference(paramod,[status(thm)],[c_62,c_56]) ).
cnf(c_734,plain,
n0 = add(n0,inverse(A)),
inference(paramod,[status(thm)],[c_5,c_733]) ).
cnf(c_64,plain,
add(n0,inverse(A)) = n0,
inference(copy,[status(thm)],[c_734]) ).
cnf(c_68,plain,
add(A,add(inverse(A),B)) = add(n0,B),
inference(paramod,[status(thm)],[c_62,c_44]) ).
cnf(c_735,plain,
( add(b,a) != add(a,b)
| add(c,add(a,b)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_4]) ).
cnf(c_736,plain,
( add(a,b) != add(a,b)
| add(c,add(a,b)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_735]) ).
cnf(c_70,plain,
( add(c,add(a,b)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(copy,[status(thm)],[c_736]) ).
cnf(c_737,plain,
( add(n0,A) = n0
| n0 != n0 ),
inference(paramod,[status(thm)],[c_64,c_18]) ).
cnf(c_71,plain,
add(n0,A) = n0,
inference(copy,[status(thm)],[c_737]) ).
cnf(c_73,plain,
add(A,add(inverse(A),B)) = n0,
inference(paramod,[status(thm)],[c_71,c_68]) ).
cnf(c_88,plain,
( add(add(add(B,C),D),A) = add(add(C,D),B)
| add(inverse(A),add(add(B,C),D)) != n0 ),
inference(paramod,[status(thm)],[c_62,c_3]) ).
cnf(c_738,plain,
add(A,add(B,C)) = add(add(A,B),C),
inference(paramod,[status(thm)],[c_62,c_12]) ).
cnf(c_90,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(copy,[status(thm)],[c_738]) ).
cnf(c_739,plain,
add(add(A,B),C) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_62,c_12]) ).
cnf(c_740,plain,
add(A,add(B,C)) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_90,c_739]) ).
cnf(c_91,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(copy,[status(thm)],[c_740]) ).
cnf(c_92,plain,
add(A,n0) = n0,
inference(paramod,[status(thm)],[c_62,c_71]) ).
cnf(c_741,plain,
( add(c,add(a,b)) != add(a,add(b,c))
| add(inverse(add(inverse(b),a)),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_70]) ).
cnf(c_742,plain,
( add(c,add(a,b)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_741]) ).
cnf(c_743,plain,
( add(b,add(c,a)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_91,c_742]) ).
cnf(c_744,plain,
( add(b,add(a,c)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_743]) ).
cnf(c_745,plain,
( add(a,add(c,b)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_91,c_744]) ).
cnf(c_746,plain,
( add(a,add(b,c)) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
inference(paramod,[status(thm)],[c_62,c_745]) ).
cnf(c_95,plain,
add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b,
inference(copy,[status(thm)],[c_746]) ).
cnf(c_747,plain,
( add(add(add(B,C),D),A) = add(add(C,D),B)
| add(inverse(A),add(B,add(C,D))) != n0 ),
inference(paramod,[status(thm)],[c_90,c_88]) ).
cnf(c_748,plain,
( add(add(B,add(C,D)),A) = add(add(C,D),B)
| add(inverse(A),add(B,add(C,D))) != n0 ),
inference(paramod,[status(thm)],[c_90,c_747]) ).
cnf(c_749,plain,
( add(B,add(add(C,D),A)) = add(add(C,D),B)
| add(inverse(A),add(B,add(C,D))) != n0 ),
inference(paramod,[status(thm)],[c_90,c_748]) ).
cnf(c_750,plain,
( add(B,add(C,add(D,A))) = add(add(C,D),B)
| add(inverse(A),add(B,add(C,D))) != n0 ),
inference(paramod,[status(thm)],[c_90,c_749]) ).
cnf(c_97,plain,
( add(B,add(C,add(D,A))) = add(C,add(D,B))
| add(inverse(A),add(B,add(C,D))) != n0 ),
inference(paramod,[status(thm)],[c_90,c_750]) ).
cnf(c_133,plain,
add(A,add(B,inverse(add(A,B)))) = n0,
inference(paramod,[status(thm)],[c_90,c_5]) ).
cnf(c_751,plain,
add(add(A,B),C) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_62,c_90]) ).
cnf(c_134,plain,
add(A,add(B,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_90,c_751]) ).
cnf(c_752,plain,
add(add(A,B),add(inverse(B),C)) = add(A,n0),
inference(paramod,[status(thm)],[c_73,c_90]) ).
cnf(c_753,plain,
add(inverse(B),add(add(A,B),C)) = add(A,n0),
inference(paramod,[status(thm)],[c_134,c_752]) ).
cnf(c_754,plain,
add(inverse(B),add(A,add(B,C))) = add(A,n0),
inference(paramod,[status(thm)],[c_90,c_753]) ).
cnf(c_136,plain,
add(inverse(A),add(B,add(A,C))) = n0,
inference(paramod,[status(thm)],[c_92,c_754]) ).
cnf(c_146,plain,
add(inverse(A),add(B,A)) = n0,
inference(paramod,[status(thm)],[c_1,c_136]) ).
cnf(c_755,plain,
( add(B,add(C,add(C,A))) = add(C,add(C,B))
| add(inverse(A),add(B,C)) != n0 ),
inference(paramod,[status(thm)],[c_1,c_97]) ).
cnf(c_756,plain,
( add(B,add(C,A)) = add(C,add(C,B))
| add(inverse(A),add(B,C)) != n0 ),
inference(paramod,[status(thm)],[c_63,c_755]) ).
cnf(c_203,plain,
( add(B,add(C,A)) = add(C,B)
| add(inverse(A),add(B,C)) != n0 ),
inference(paramod,[status(thm)],[c_63,c_756]) ).
cnf(c_757,plain,
( add(B,add(B,A)) = add(B,B)
| add(inverse(A),B) != n0 ),
inference(paramod,[status(thm)],[c_1,c_203]) ).
cnf(c_758,plain,
( add(B,A) = add(B,B)
| add(inverse(A),B) != n0 ),
inference(paramod,[status(thm)],[c_63,c_757]) ).
cnf(c_218,plain,
( add(B,A) = B
| add(inverse(A),B) != n0 ),
inference(paramod,[status(thm)],[c_1,c_758]) ).
cnf(c_759,plain,
add(inverse(inverse(A)),A) = inverse(inverse(A)),
inference(resolve,[status(thm)],[c_218,c_5]) ).
cnf(c_229,plain,
add(A,inverse(inverse(A))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_62,c_759]) ).
cnf(c_230,plain,
( add(A,B) = A
| add(A,inverse(B)) != n0 ),
inference(paramod,[status(thm)],[c_62,c_218]) ).
cnf(c_233,plain,
add(A,inverse(inverse(inverse(A)))) = n0,
inference(paramod,[status(thm)],[c_229,c_73]) ).
cnf(c_760,plain,
add(A,inverse(inverse(A))) = A,
inference(resolve,[status(thm)],[c_233,c_230]) ).
cnf(c_328,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_229,c_760]) ).
cnf(c_331,plain,
( add(B,inverse(A)) = B
| add(A,B) != n0 ),
inference(paramod,[status(thm)],[c_328,c_218]) ).
cnf(c_332,plain,
( add(A,inverse(B)) = A
| add(A,B) != n0 ),
inference(paramod,[status(thm)],[c_328,c_230]) ).
cnf(c_761,plain,
add(add(A,inverse(add(B,A))),inverse(B)) = add(A,inverse(add(B,A))),
inference(resolve,[status(thm)],[c_331,c_133]) ).
cnf(c_369,plain,
add(inverse(A),add(B,inverse(add(A,B)))) = add(B,inverse(add(A,B))),
inference(paramod,[status(thm)],[c_62,c_761]) ).
cnf(c_374,plain,
add(inverse(A),inverse(add(B,A))) = inverse(A),
inference(resolve,[status(thm)],[c_332,c_146]) ).
cnf(c_388,plain,
add(inverse(A),inverse(add(A,B))) = inverse(A),
inference(paramod,[status(thm)],[c_62,c_374]) ).
cnf(c_762,plain,
add(A,inverse(B)) = add(inverse(B),add(A,inverse(add(B,C)))),
inference(paramod,[status(thm)],[c_388,c_134]) ).
cnf(c_398,plain,
add(inverse(A),add(B,inverse(add(A,C)))) = add(B,inverse(A)),
inference(copy,[status(thm)],[c_762]) ).
cnf(c_763,plain,
add(B,inverse(A)) = add(B,inverse(add(A,B))),
inference(paramod,[status(thm)],[c_398,c_369]) ).
cnf(c_401,plain,
add(A,inverse(add(B,A))) = add(A,inverse(B)),
inference(copy,[status(thm)],[c_763]) ).
cnf(c_764,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(A)))) = add(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_401,c_401]) ).
cnf(c_765,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(A)))) = add(inverse(B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_62,c_764]) ).
cnf(c_453,plain,
add(inverse(add(A,B)),inverse(add(B,inverse(A)))) = inverse(B),
inference(paramod,[status(thm)],[c_374,c_765]) ).
cnf(c_690,plain,
add(inverse(add(A,B)),inverse(add(inverse(A),B))) = inverse(B),
inference(paramod,[status(thm)],[c_62,c_453]) ).
cnf(c_766,plain,
inverse(inverse(b)) != b,
inference(paramod,[status(thm)],[c_690,c_95]) ).
cnf(c_767,plain,
b != b,
inference(paramod,[status(thm)],[c_328,c_766]) ).
cnf(c_713,plain,
$false,
inference(copy,[status(thm)],[c_767]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n009.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sat Sep 26 22:36:45 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.45 % Process 1302365 was started by sandbox on n009,
% 0.19/0.45 % Sat Sep 26 22:36:45 2026
% 0.19/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.46
% 0.19/0.46 % From the command line: assign(max_seconds, 300).
% 3.62/0.95
% 3.62/0.95 % Assigning unary symbol inverse kb_weight 0 and highest precedence (7).
% 3.62/0.95
% 3.62/0.95 % SZS status Unsatisfiable for theBenchmark
% 3.62/0.95
% 3.62/0.95 % Proof 1 at 0.36 (+ 0.12) seconds.
% 3.62/0.95 % Length of proof is 46.
% 3.62/0.95 % Level of proof is 20.
% 3.62/0.95 % Maximum clause weight is 68.000.
% 3.62/0.95 % Given clauses 127.
% 3.62/0.95
% 3.62/0.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------