%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO002-2 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:00 AM UTC 2026
% Result : Unsatisfiable 9.64s 8.07s
% Output : CNFRefutation 9.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 6
% Syntax : Number of formulae : 61 ( 61 unt; 0 def)
% Number of atoms : 61 ( 60 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-3 aty)
% Number of variables : 195 ( 7 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : multiply(multiply(VAR_0,VAR_1,VAR_2),VAR_3,multiply(VAR_0,VAR_1,VAR_4)) = multiply(VAR_0,VAR_1,multiply(VAR_2,VAR_3,VAR_4)),
file('theBenchmark.p',associativity) ).
cnf(c_1,plain,
multiply(multiply(A,B,C),D,multiply(A,B,E)) = multiply(A,B,multiply(C,D,E)),
inference(clausify,[status(thm)],[associativity]) ).
fof(ternary_multiply_1,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_1,VAR_1) = VAR_1,
file('theBenchmark.p',ternary_multiply_1) ).
cnf(c_2,plain,
multiply(A,B,B) = B,
inference(clausify,[status(thm)],[ternary_multiply_1]) ).
fof(ternary_multiply_2,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_0,VAR_1) = VAR_0,
file('theBenchmark.p',ternary_multiply_2) ).
cnf(c_3,plain,
multiply(A,A,B) = A,
inference(clausify,[status(thm)],[ternary_multiply_2]) ).
fof(left_inverse,axiom,
! [VAR_0,VAR_1] : multiply(inverse(VAR_0),VAR_0,VAR_1) = VAR_1,
file('theBenchmark.p',left_inverse) ).
cnf(c_4,plain,
multiply(inverse(A),A,B) = B,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(extra_lemma,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_1,VAR_0) = VAR_0,
file('theBenchmark.p',extra_lemma) ).
cnf(c_5,plain,
multiply(A,B,A) = A,
inference(clausify,[status(thm)],[extra_lemma]) ).
fof(prove_equation,axiom,
multiply(a,inverse(a),b) != b,
file('theBenchmark.p',prove_equation) ).
cnf(c_6,plain,
multiply(a,inverse(a),b) != b,
inference(clausify,[status(thm)],[prove_equation]) ).
cnf(c_7,plain,
multiply(A,B,multiply(C,A,D)) = multiply(C,A,multiply(A,B,D)),
inference(paramod,[status(thm)],[c_2,c_1]) ).
cnf(c_8,plain,
multiply(multiply(A,B,C),D,B) = multiply(A,B,multiply(C,D,B)),
inference(paramod,[status(thm)],[c_2,c_1]) ).
cnf(c_812,plain,
multiply(A,B,C) = multiply(A,B,multiply(D,multiply(A,B,C),C)),
inference(paramod,[status(thm)],[c_2,c_1]) ).
cnf(c_9,plain,
multiply(A,B,multiply(C,multiply(A,B,D),D)) = multiply(A,B,D),
inference(copy,[status(thm)],[c_812]) ).
cnf(c_813,plain,
multiply(A,B,C) = multiply(A,B,multiply(C,multiply(A,B,C),D)),
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_10,plain,
multiply(A,B,multiply(C,multiply(A,B,C),D)) = multiply(A,B,C),
inference(copy,[status(thm)],[c_813]) ).
cnf(c_11,plain,
multiply(A,B,multiply(A,C,D)) = multiply(A,C,multiply(A,B,D)),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_12,plain,
multiply(multiply(A,B,C),D,A) = multiply(A,B,multiply(C,D,A)),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_18,plain,
multiply(A,B,multiply(C,D,multiply(D,A,E))) = multiply(D,A,multiply(A,B,multiply(C,D,E))),
inference(paramod,[status(thm)],[c_7,c_7]) ).
cnf(c_814,plain,
multiply(A,B,C) = multiply(A,C,multiply(A,B,C)),
inference(paramod,[status(thm)],[c_5,c_8]) ).
cnf(c_23,plain,
multiply(A,B,multiply(A,C,B)) = multiply(A,C,B),
inference(copy,[status(thm)],[c_814]) ).
cnf(c_815,plain,
multiply(multiply(multiply(A,B,C),C,A),B,C) = multiply(A,B,C),
inference(paramod,[status(thm)],[c_5,c_8]) ).
cnf(c_816,plain,
multiply(multiply(A,B,multiply(C,C,A)),B,C) = multiply(A,B,C),
inference(paramod,[status(thm)],[c_12,c_815]) ).
cnf(c_24,plain,
multiply(multiply(A,B,C),B,C) = multiply(A,B,C),
inference(paramod,[status(thm)],[c_3,c_816]) ).
cnf(c_817,plain,
multiply(multiply(A,B,C),D,B) = multiply(multiply(A,B,C),B,multiply(C,D,B)),
inference(paramod,[status(thm)],[c_24,c_8]) ).
cnf(c_818,plain,
multiply(A,B,multiply(C,D,B)) = multiply(multiply(A,B,C),B,multiply(C,D,B)),
inference(paramod,[status(thm)],[c_8,c_817]) ).
cnf(c_51,plain,
multiply(multiply(A,B,C),B,multiply(C,D,B)) = multiply(A,B,multiply(C,D,B)),
inference(copy,[status(thm)],[c_818]) ).
cnf(c_64,plain,
multiply(A,B,multiply(A,B,C)) = multiply(A,B,C),
inference(paramod,[status(thm)],[c_3,c_9]) ).
cnf(c_819,plain,
multiply(A,B,multiply(C,multiply(A,B,C),B)) = multiply(C,multiply(A,B,C),multiply(multiply(A,B,C),B,B)),
inference(paramod,[status(thm)],[c_51,c_7]) ).
cnf(c_820,plain,
multiply(A,B,C) = multiply(C,multiply(A,B,C),multiply(multiply(A,B,C),B,B)),
inference(paramod,[status(thm)],[c_10,c_819]) ).
cnf(c_821,plain,
multiply(A,B,C) = multiply(C,multiply(A,B,C),B),
inference(paramod,[status(thm)],[c_2,c_820]) ).
cnf(c_88,plain,
multiply(A,multiply(B,C,A),C) = multiply(B,C,A),
inference(copy,[status(thm)],[c_821]) ).
cnf(c_822,plain,
multiply(A,B,multiply(C,D,A)) = multiply(A,multiply(C,D,A),multiply(A,B,D)),
inference(paramod,[status(thm)],[c_88,c_11]) ).
cnf(c_95,plain,
multiply(A,multiply(B,C,A),multiply(A,D,C)) = multiply(A,D,multiply(B,C,A)),
inference(copy,[status(thm)],[c_822]) ).
cnf(c_100,plain,
multiply(multiply(A,B,C),D,C) = multiply(C,multiply(A,B,C),multiply(B,D,C)),
inference(paramod,[status(thm)],[c_88,c_12]) ).
cnf(c_823,plain,
multiply(A,multiply(B,multiply(A,C,B),A),multiply(A,C,multiply(A,C,B))) = multiply(A,C,B),
inference(paramod,[status(thm)],[c_95,c_10]) ).
cnf(c_824,plain,
multiply(A,multiply(B,multiply(A,C,B),A),multiply(A,C,B)) = multiply(A,C,B),
inference(paramod,[status(thm)],[c_64,c_823]) ).
cnf(c_134,plain,
multiply(A,multiply(B,C,A),B) = multiply(B,C,A),
inference(paramod,[status(thm)],[c_88,c_824]) ).
cnf(c_825,plain,
multiply(A,multiply(A,B,C),C) = multiply(C,multiply(A,B,C),A),
inference(paramod,[status(thm)],[c_134,c_134]) ).
cnf(c_163,plain,
multiply(A,multiply(A,B,C),C) = multiply(A,B,C),
inference(paramod,[status(thm)],[c_134,c_825]) ).
cnf(c_826,plain,
multiply(A,B,multiply(A,C,D)) = multiply(A,multiply(A,C,D),multiply(A,B,D)),
inference(paramod,[status(thm)],[c_163,c_11]) ).
cnf(c_182,plain,
multiply(A,multiply(A,B,C),multiply(A,D,C)) = multiply(A,D,multiply(A,B,C)),
inference(copy,[status(thm)],[c_826]) ).
cnf(c_827,plain,
multiply(A,multiply(A,B,C),multiply(A,multiply(D,C,A),C)) = multiply(A,B,multiply(D,C,A)),
inference(paramod,[status(thm)],[c_182,c_95]) ).
cnf(c_334,plain,
multiply(A,multiply(A,B,C),multiply(D,C,A)) = multiply(A,B,multiply(D,C,A)),
inference(paramod,[status(thm)],[c_88,c_827]) ).
cnf(c_828,plain,
multiply(A,B,multiply(C,D,multiply(multiply(C,D,A),A,C))) = multiply(multiply(C,D,A),A,multiply(A,B,multiply(C,multiply(C,D,A),C))),
inference(paramod,[status(thm)],[c_334,c_18]) ).
cnf(c_829,plain,
multiply(A,B,multiply(C,D,multiply(C,D,multiply(A,A,C)))) = multiply(multiply(C,D,A),A,multiply(A,B,multiply(C,multiply(C,D,A),C))),
inference(paramod,[status(thm)],[c_12,c_828]) ).
cnf(c_830,plain,
multiply(A,B,multiply(C,D,multiply(C,D,A))) = multiply(multiply(C,D,A),A,multiply(A,B,multiply(C,multiply(C,D,A),C))),
inference(paramod,[status(thm)],[c_3,c_829]) ).
cnf(c_831,plain,
multiply(A,B,multiply(C,D,A)) = multiply(multiply(C,D,A),A,multiply(A,B,multiply(C,multiply(C,D,A),C))),
inference(paramod,[status(thm)],[c_64,c_830]) ).
cnf(c_832,plain,
multiply(A,B,multiply(C,D,A)) = multiply(multiply(C,D,A),A,multiply(A,B,C)),
inference(paramod,[status(thm)],[c_5,c_831]) ).
cnf(c_461,plain,
multiply(multiply(A,B,C),C,multiply(C,D,A)) = multiply(C,D,multiply(A,B,C)),
inference(copy,[status(thm)],[c_832]) ).
cnf(c_833,plain,
multiply(multiply(A,B,C),A,multiply(A,D,C)) = multiply(A,D,multiply(C,multiply(A,B,C),A)),
inference(paramod,[status(thm)],[c_134,c_461]) ).
cnf(c_489,plain,
multiply(multiply(A,B,C),A,multiply(A,D,C)) = multiply(A,D,multiply(A,B,C)),
inference(paramod,[status(thm)],[c_134,c_833]) ).
cnf(c_834,plain,
multiply(multiply(A,B,C),A,C) = multiply(A,C,multiply(A,B,C)),
inference(paramod,[status(thm)],[c_2,c_489]) ).
cnf(c_835,plain,
multiply(C,multiply(A,B,C),multiply(B,A,C)) = multiply(A,C,multiply(A,B,C)),
inference(paramod,[status(thm)],[c_100,c_834]) ).
cnf(c_804,plain,
multiply(A,multiply(B,C,A),multiply(C,B,A)) = multiply(B,C,A),
inference(paramod,[status(thm)],[c_23,c_835]) ).
cnf(c_836,plain,
multiply(A,multiply(B,inverse(B),A),A) = multiply(B,inverse(B),A),
inference(paramod,[status(thm)],[c_4,c_804]) ).
cnf(c_837,plain,
A = multiply(B,inverse(B),A),
inference(paramod,[status(thm)],[c_5,c_836]) ).
cnf(c_810,plain,
multiply(A,inverse(A),B) = B,
inference(copy,[status(thm)],[c_837]) ).
cnf(c_811,plain,
$false,
inference(resolve,[status(thm)],[c_810,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO002-2 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/5.33 % Computer : n017.cluster.edu
% 0.04/5.33 % Model : x86_64 x86_64
% 0.04/5.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.33 % Memory : 8046.5625MB
% 0.04/5.33 % OS : Linux 6.8.0-71-generic
% 0.04/5.33 % CPULimit : 300
% 0.04/5.33 % WCLimit : 300
% 0.04/5.33 % DateTime : Sat Sep 26 22:28:24 UTC 2026
% 0.04/5.33 % CPUTime :
% 0.04/5.33 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/5.33 % Process 1812814 was started by sandbox on n017,
% 0.04/5.33 % Sat Sep 26 22:28:24 2026
% 0.04/5.33 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.04/5.34
% 0.04/5.34 % From the command line: assign(max_seconds, 300).
% 9.64/8.07
% 9.64/8.07 % SZS status Unsatisfiable for theBenchmark
% 9.64/8.07
% 9.64/8.07 % Proof 1 at 0.92 (+ 0.34) seconds.
% 9.64/8.07 % Length of proof is 29.
% 9.64/8.07 % Level of proof is 14.
% 9.64/8.07 % Maximum clause weight is 29.000.
% 9.64/8.07 % Given clauses 108.
% 9.64/8.07
% 9.64/8.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------