%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP748+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 07:31:21 AM UTC 2026
% Result : Theorem 12.32s 2.03s
% Output : CNFRefutation 12.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 9
% Syntax : Number of formulae : 75 ( 51 unt; 0 def)
% Number of atoms : 108 ( 107 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 45 ( 12 ~; 27 |; 6 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-2 aty)
% Number of variables : 167 ( 0 sgn 39 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('theBenchmark.p',f01) ).
fof(f02,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('theBenchmark.p',f02) ).
fof(f03,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('theBenchmark.p',f03) ).
fof(f06,axiom,
! [A] : mult(unit,A) = A,
file('theBenchmark.p',f06) ).
fof(f07,axiom,
! [C,B,A] : mult(mult(mult(A,B),C),B) = mult(A,mult(mult(B,C),B)),
file('theBenchmark.p',f07) ).
fof(f08,axiom,
! [B,A] : mult(mult(A,B),i(B)) = A,
file('theBenchmark.p',f08) ).
fof(f09,axiom,
! [A] : mult(A,i(A)) = unit,
file('theBenchmark.p',f09) ).
fof(f11,axiom,
! [B,A] :
( mult(i(A),mult(A,B)) = B
| mult(A,B) = mult(B,A) ),
file('theBenchmark.p',f11) ).
fof(goals,conjecture,
( ! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11))
| ! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8)
| ! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5)
| ! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ( ! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11))
| ! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8)
| ! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5)
| ! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_13,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
cnf(c_14,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
cnf(c_15,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
cnf(c_18,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[f06]) ).
cnf(c_19,plain,
mult(mult(mult(A,B),C),B) = mult(A,mult(mult(B,C),B)),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_20,plain,
mult(mult(A,B),i(B)) = A,
inference(clausify,[status(thm)],[f08]) ).
cnf(c_21,plain,
mult(A,i(A)) = unit,
inference(clausify,[status(thm)],[f09]) ).
cnf(c_23,plain,
( mult(i(B),mult(B,A)) = A
| mult(A,B) = mult(B,A) ),
inference(clausify,[status(thm)],[f11]) ).
fof(nnf_12,plain,
( ? [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) != mult(X11,mult(mult(X9,X10),X11))
& ? [X6,X7,X8] : mult(mult(X8,mult(X6,X7)),X8) != mult(mult(X8,X6),mult(X7,X8))
& ? [X3,X4,X5] : mult(mult(mult(X3,X5),X4),X5) != mult(X3,mult(X5,mult(X4,X5)))
& ? [X0,X1,X2] : mult(mult(mult(X2,X0),X2),X1) != mult(X2,mult(X0,mult(X2,X1))) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( mult(mult(sK9,sK10),mult(sK11,sK9)) != mult(sK9,mult(mult(sK10,sK11),sK9))
& mult(mult(sK6,mult(sK7,sK8)),sK6) != mult(mult(sK6,sK7),mult(sK8,sK6))
& mult(mult(mult(sK0,sK1),sK2),sK1) != mult(sK0,mult(sK1,mult(sK2,sK1)))
& mult(mult(mult(sK3,sK4),sK3),sK5) != mult(sK3,mult(sK4,mult(sK3,sK5))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK0,sK1,sK2,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK3),skolemize(X3,sK0),skolemize(X4,sK2),skolemize(X5,sK1),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK6),skolemize(X9,sK10),skolemize(X10,sK11),skolemize(X11,sK9)],[nnf_12]) ).
cnf(c_25,negated_conjecture,
mult(mult(mult(sK0,sK1),sK2),sK1) != mult(sK0,mult(sK1,mult(sK2,sK1))),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_26,negated_conjecture,
mult(sK0,mult(mult(sK1,sK2),sK1)) != mult(sK0,mult(sK1,mult(sK2,sK1))),
inference(paramod,[status(thm)],[c_19,c_25]) ).
cnf(c_29,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_15,c_14]) ).
cnf(c_44,plain,
ld(mult(A,B),A) = i(B),
inference(paramod,[status(thm)],[c_20,c_14]) ).
cnf(c_3657,plain,
mult(A,i(B)) = rd(A,B),
inference(paramod,[status(thm)],[c_15,c_20]) ).
cnf(c_45,plain,
rd(A,B) = mult(A,i(B)),
inference(copy,[status(thm)],[c_3657]) ).
cnf(c_3658,plain,
ld(mult(A,i(B)),A) = B,
inference(paramod,[status(thm)],[c_45,c_29]) ).
cnf(c_51,plain,
i(i(A)) = A,
inference(paramod,[status(thm)],[c_44,c_3658]) ).
cnf(c_3659,plain,
mult(mult(unit,A),i(B)) = mult(B,mult(mult(i(B),A),i(B))),
inference(paramod,[status(thm)],[c_21,c_19]) ).
cnf(c_3660,plain,
mult(A,i(B)) = mult(B,mult(mult(i(B),A),i(B))),
inference(paramod,[status(thm)],[c_18,c_3659]) ).
cnf(c_55,plain,
mult(A,mult(mult(i(A),B),i(A))) = mult(B,i(A)),
inference(copy,[status(thm)],[c_3660]) ).
cnf(c_3661,plain,
mult(unit,A) = mult(B,mult(mult(A,i(mult(B,A))),A)),
inference(paramod,[status(thm)],[c_21,c_19]) ).
cnf(c_3662,plain,
A = mult(B,mult(mult(A,i(mult(B,A))),A)),
inference(paramod,[status(thm)],[c_18,c_3661]) ).
cnf(c_56,plain,
mult(A,mult(mult(B,i(mult(A,B))),B)) = B,
inference(copy,[status(thm)],[c_3662]) ).
cnf(c_3663,plain,
( mult(ld(A,B),A) = B
| mult(i(A),mult(A,ld(A,B))) = ld(A,B) ),
inference(paramod,[status(thm)],[c_23,c_13]) ).
cnf(c_3664,plain,
( mult(ld(A,B),A) = B
| mult(i(A),B) = ld(A,B) ),
inference(paramod,[status(thm)],[c_13,c_3663]) ).
cnf(c_59,plain,
( mult(ld(A,B),A) = B
| ld(A,B) = mult(i(A),B) ),
inference(copy,[status(thm)],[c_3664]) ).
cnf(c_62,plain,
( ld(i(B),A) = mult(B,A)
| mult(A,B) = mult(B,A) ),
inference(paramod,[status(thm)],[c_23,c_14]) ).
cnf(c_3665,plain,
( mult(B,i(A)) = ld(A,B)
| ld(A,B) = mult(i(A),B) ),
inference(paramod,[status(thm)],[c_59,c_20]) ).
cnf(c_327,plain,
( ld(A,B) = mult(B,i(A))
| ld(A,B) = mult(i(A),B) ),
inference(copy,[status(thm)],[c_3665]) ).
cnf(c_3666,plain,
( ld(B,A) = mult(i(B),A)
| mult(A,i(B)) = mult(i(B),A) ),
inference(paramod,[status(thm)],[c_51,c_62]) ).
cnf(c_358,plain,
( ld(A,B) = mult(i(A),B)
| mult(i(A),B) = mult(B,i(A)) ),
inference(copy,[status(thm)],[c_3666]) ).
cnf(c_3667,plain,
( mult(i(mult(A,B)),A) = i(B)
| ld(mult(A,B),A) = mult(A,i(mult(A,B))) ),
inference(paramod,[status(thm)],[c_327,c_44]) ).
cnf(c_3668,plain,
( mult(i(mult(A,B)),A) = i(B)
| i(B) = mult(A,i(mult(A,B))) ),
inference(paramod,[status(thm)],[c_44,c_3667]) ).
cnf(c_395,plain,
( mult(i(mult(A,B)),A) = i(B)
| mult(A,i(mult(A,B))) = i(B) ),
inference(copy,[status(thm)],[c_3668]) ).
cnf(c_724,plain,
( mult(i(mult(A,B)),A) = i(B)
| mult(i(mult(A,B)),A) = mult(A,i(mult(A,B))) ),
inference(paramod,[status(thm)],[c_358,c_44]) ).
cnf(c_929,plain,
ld(A,B) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_56,c_14]) ).
cnf(c_3669,plain,
ld(A,B) = i(mult(mult(A,i(mult(B,A))),A)),
inference(paramod,[status(thm)],[c_56,c_44]) ).
cnf(c_3670,plain,
mult(mult(B,i(mult(A,B))),B) = i(mult(mult(A,i(mult(B,A))),A)),
inference(paramod,[status(thm)],[c_929,c_3669]) ).
cnf(c_941,plain,
i(mult(mult(A,i(mult(B,A))),A)) = mult(mult(B,i(mult(A,B))),B),
inference(copy,[status(thm)],[c_3670]) ).
cnf(c_3671,plain,
( mult(i(B),i(A)) = i(mult(A,B))
| mult(A,i(mult(A,B))) = i(B) ),
inference(paramod,[status(thm)],[c_395,c_20]) ).
cnf(c_1187,plain,
( i(mult(A,B)) = mult(i(B),i(A))
| mult(A,i(mult(A,B))) = i(B) ),
inference(copy,[status(thm)],[c_3671]) ).
cnf(c_3672,plain,
( mult(i(mult(A,B)),A) = i(B)
| mult(i(mult(A,B)),A) = i(B)
| i(mult(A,B)) = mult(i(B),i(A)) ),
inference(paramod,[status(thm)],[c_1187,c_724]) ).
cnf(c_2660,plain,
( mult(i(mult(A,B)),A) = i(B)
| i(mult(A,B)) = mult(i(B),i(A)) ),
inference(copy,[status(thm)],[c_3672]) ).
cnf(c_3673,plain,
( mult(i(B),i(A)) = i(mult(A,B))
| i(mult(A,B)) = mult(i(B),i(A)) ),
inference(paramod,[status(thm)],[c_2660,c_20]) ).
cnf(c_3674,plain,
( i(mult(A,B)) = mult(i(B),i(A))
| i(mult(A,B)) = mult(i(B),i(A)) ),
inference(copy,[status(thm)],[c_3673]) ).
cnf(c_2707,plain,
i(mult(A,B)) = mult(i(B),i(A)),
inference(copy,[status(thm)],[c_3674]) ).
cnf(c_3675,plain,
i(mult(mult(A,mult(i(A),i(B))),A)) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_2707,c_941]) ).
cnf(c_3676,plain,
mult(i(A),i(mult(A,mult(i(A),i(B))))) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_2707,c_3675]) ).
cnf(c_3677,plain,
mult(i(A),mult(i(mult(i(A),i(B))),i(A))) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_2707,c_3676]) ).
cnf(c_3678,plain,
mult(i(A),mult(mult(i(i(B)),i(i(A))),i(A))) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_2707,c_3677]) ).
cnf(c_3679,plain,
mult(i(A),mult(mult(B,i(i(A))),i(A))) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_51,c_3678]) ).
cnf(c_3680,plain,
mult(i(A),mult(mult(B,A),i(A))) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_51,c_3679]) ).
cnf(c_3681,plain,
mult(i(A),B) = mult(mult(B,i(mult(A,B))),B),
inference(paramod,[status(thm)],[c_20,c_3680]) ).
cnf(c_3682,plain,
mult(i(A),B) = mult(mult(B,mult(i(B),i(A))),B),
inference(paramod,[status(thm)],[c_2707,c_3681]) ).
cnf(c_3182,plain,
mult(mult(A,mult(i(A),i(B))),A) = mult(i(B),A),
inference(copy,[status(thm)],[c_3682]) ).
cnf(c_3683,plain,
mult(A,mult(mult(B,mult(i(B),i(A))),B)) = B,
inference(paramod,[status(thm)],[c_2707,c_56]) ).
cnf(c_3224,plain,
mult(A,mult(i(A),B)) = B,
inference(paramod,[status(thm)],[c_3182,c_3683]) ).
cnf(c_3684,plain,
mult(A,mult(B,i(i(A)))) = mult(mult(i(i(A)),B),i(i(A))),
inference(paramod,[status(thm)],[c_55,c_3224]) ).
cnf(c_3685,plain,
mult(A,mult(B,A)) = mult(mult(i(i(A)),B),i(i(A))),
inference(paramod,[status(thm)],[c_51,c_3684]) ).
cnf(c_3686,plain,
mult(A,mult(B,A)) = mult(mult(A,B),i(i(A))),
inference(paramod,[status(thm)],[c_51,c_3685]) ).
cnf(c_3687,plain,
mult(A,mult(B,A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_51,c_3686]) ).
cnf(c_3470,plain,
mult(mult(A,B),A) = mult(A,mult(B,A)),
inference(copy,[status(thm)],[c_3687]) ).
cnf(c_3688,negated_conjecture,
mult(sK0,mult(sK1,mult(sK2,sK1))) != mult(sK0,mult(sK1,mult(sK2,sK1))),
inference(paramod,[status(thm)],[c_3470,c_26]) ).
cnf(c_3656,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_3688]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP748+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n018.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Fri Sep 25 15:45:35 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 2339497 was started by sandbox2 on n018,
% 0.16/0.44 % Fri Sep 25 15:45:35 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.45
% 0.16/0.45 % From the command line: assign(max_seconds, 300).
% 12.32/2.03
% 12.32/2.03 % SZS status Theorem for theBenchmark
% 12.32/2.03
% 12.32/2.03 % Proof 1 at 1.37 (+ 0.19) seconds.
% 12.32/2.03 % Length of proof is 40.
% 12.32/2.03 % Level of proof is 11.
% 12.32/2.03 % Maximum clause weight is 58.000.
% 12.32/2.03 % Given clauses 101.
% 12.32/2.03
% 12.32/2.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------