%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP699-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 : n020.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:14 AM UTC 2026
% Result : Unsatisfiable 2.66s 0.81s
% Output : CNFRefutation 2.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 9
% Syntax : Number of formulae : 76 ( 76 unt; 0 def)
% Number of atoms : 76 ( 75 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 149 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[c01]) ).
fof(c02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[c02]) ).
fof(c03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[c03]) ).
fof(c04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[c04]) ).
fof(c05,axiom,
! [VAR_0] : mult(VAR_0,unit) = VAR_0,
file('theBenchmark.p',c05) ).
cnf(c_5,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[c05]) ).
fof(c06,axiom,
! [VAR_0] : mult(unit,VAR_0) = VAR_0,
file('theBenchmark.p',c06) ).
cnf(c_6,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[c06]) ).
fof(c07,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(mult(VAR_0,VAR_1),VAR_0),mult(VAR_0,VAR_2)) = mult(VAR_0,mult(mult(mult(VAR_1,VAR_0),VAR_0),VAR_2)),
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
mult(mult(mult(A,B),A),mult(A,C)) = mult(A,mult(mult(mult(B,A),A),C)),
inference(clausify,[status(thm)],[c07]) ).
fof(c08,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),mult(VAR_1,mult(VAR_2,VAR_1))) = mult(mult(VAR_0,mult(VAR_1,mult(VAR_1,VAR_2))),VAR_1),
file('theBenchmark.p',c08) ).
cnf(c_8,plain,
mult(mult(A,B),mult(B,mult(C,B))) = mult(mult(A,mult(B,mult(B,C))),B),
inference(clausify,[status(thm)],[c08]) ).
cnf(c_9,plain,
mult(mult(A,mult(B,mult(B,C))),B) = mult(mult(A,B),mult(B,mult(C,B))),
inference(copy,[status(thm)],[c_8]) ).
fof(goals,axiom,
mult(mult(a,b),c) != mult(mult(a,c),ld(c,mult(b,c))),
file('theBenchmark.p',goals) ).
cnf(c_10,plain,
mult(mult(a,b),c) != mult(mult(a,c),ld(c,mult(b,c))),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_11,plain,
mult(mult(a,c),ld(c,mult(b,c))) != mult(mult(a,b),c),
inference(copy,[status(thm)],[c_10]) ).
cnf(c_890,plain,
mult(mult(A,A),mult(A,B)) = mult(A,mult(mult(mult(unit,A),A),B)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_29,plain,
mult(mult(A,A),mult(A,B)) = mult(A,mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_6,c_890]) ).
cnf(c_891,plain,
mult(mult(mult(A,B),A),A) = mult(A,mult(mult(mult(B,A),A),unit)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_30,plain,
mult(mult(mult(A,B),A),A) = mult(A,mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_5,c_891]) ).
cnf(c_32,plain,
mult(mult(A,mult(B,C)),B) = mult(mult(A,B),mult(B,mult(ld(B,C),B))),
inference(paramod,[status(thm)],[c_1,c_9]) ).
cnf(c_892,plain,
mult(mult(A,mult(A,B)),A) = mult(mult(unit,A),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_38,plain,
mult(mult(A,mult(A,B)),A) = mult(A,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_6,c_892]) ).
cnf(c_893,plain,
mult(mult(A,A),B) = mult(A,mult(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_29]) ).
cnf(c_39,plain,
mult(A,mult(mult(A,A),ld(A,B))) = mult(mult(A,A),B),
inference(copy,[status(thm)],[c_893]) ).
cnf(c_40,plain,
ld(mult(A,A),mult(A,mult(mult(A,A),B))) = mult(A,B),
inference(paramod,[status(thm)],[c_29,c_2]) ).
cnf(c_73,plain,
ld(A,mult(mult(A,A),B)) = mult(mult(A,A),ld(A,B)),
inference(paramod,[status(thm)],[c_39,c_2]) ).
cnf(c_157,plain,
ld(mult(A,A),mult(A,B)) = mult(A,ld(mult(A,A),B)),
inference(paramod,[status(thm)],[c_1,c_40]) ).
cnf(c_894,plain,
ld(mult(A,A),B) = mult(A,ld(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_157]) ).
cnf(c_161,plain,
mult(A,ld(mult(A,A),ld(A,B))) = ld(mult(A,A),B),
inference(copy,[status(thm)],[c_894]) ).
cnf(c_895,plain,
ld(A,ld(mult(A,A),B)) = ld(mult(A,A),ld(A,B)),
inference(paramod,[status(thm)],[c_161,c_2]) ).
cnf(c_174,plain,
ld(mult(A,A),ld(A,B)) = ld(A,ld(mult(A,A),B)),
inference(copy,[status(thm)],[c_895]) ).
cnf(c_896,plain,
mult(mult(A,B),C) = mult(mult(A,C),mult(C,mult(ld(C,ld(C,B)),C))),
inference(paramod,[status(thm)],[c_1,c_32]) ).
cnf(c_188,plain,
mult(mult(A,B),mult(B,mult(ld(B,ld(B,C)),B))) = mult(mult(A,C),B),
inference(copy,[status(thm)],[c_896]) ).
cnf(c_897,plain,
ld(A,mult(mult(A,mult(A,B)),A)) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_32,c_73]) ).
cnf(c_898,plain,
ld(A,mult(A,mult(A,mult(B,A)))) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_38,c_897]) ).
cnf(c_899,plain,
mult(A,mult(B,A)) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_2,c_898]) ).
cnf(c_900,plain,
mult(A,mult(B,A)) = mult(mult(A,A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_2,c_899]) ).
cnf(c_207,plain,
mult(mult(A,A),mult(ld(A,B),A)) = mult(A,mult(B,A)),
inference(copy,[status(thm)],[c_900]) ).
cnf(c_901,plain,
ld(mult(A,A),mult(A,mult(B,A))) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_207,c_2]) ).
cnf(c_333,plain,
mult(A,ld(mult(A,A),mult(B,A))) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_157,c_901]) ).
cnf(c_902,plain,
ld(A,mult(ld(A,B),A)) = ld(mult(A,A),mult(B,A)),
inference(paramod,[status(thm)],[c_333,c_2]) ).
cnf(c_348,plain,
ld(mult(A,A),mult(B,A)) = ld(A,mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_903,plain,
mult(A,ld(mult(A,A),B)) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_3,c_333]) ).
cnf(c_349,plain,
mult(ld(A,rd(B,A)),A) = mult(A,ld(mult(A,A),B)),
inference(copy,[status(thm)],[c_903]) ).
cnf(c_904,plain,
mult(A,ld(mult(A,A),mult(A,mult(mult(B,A),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_30,c_333]) ).
cnf(c_905,plain,
mult(A,mult(A,ld(mult(A,A),mult(mult(B,A),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_157,c_904]) ).
cnf(c_906,plain,
mult(A,mult(A,ld(A,mult(ld(A,mult(B,A)),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_348,c_905]) ).
cnf(c_907,plain,
mult(A,mult(ld(A,mult(B,A)),A)) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_1,c_906]) ).
cnf(c_364,plain,
mult(ld(A,mult(mult(A,B),A)),A) = mult(A,mult(ld(A,mult(B,A)),A)),
inference(copy,[status(thm)],[c_907]) ).
cnf(c_908,plain,
ld(mult(A,A),mult(A,mult(A,mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_38,c_348]) ).
cnf(c_909,plain,
mult(A,ld(mult(A,A),mult(A,mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_157,c_908]) ).
cnf(c_910,plain,
mult(A,mult(A,ld(mult(A,A),mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_157,c_909]) ).
cnf(c_911,plain,
mult(A,mult(A,ld(A,mult(ld(A,B),A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_348,c_910]) ).
cnf(c_912,plain,
mult(A,mult(ld(A,B),A)) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_1,c_911]) ).
cnf(c_913,plain,
mult(A,mult(ld(A,B),A)) = ld(A,mult(mult(A,B),A)),
inference(paramod,[status(thm)],[c_2,c_912]) ).
cnf(c_449,plain,
ld(A,mult(mult(A,B),A)) = mult(A,mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_913]) ).
cnf(c_914,plain,
mult(mult(A,mult(ld(A,B),A)),A) = mult(A,mult(ld(A,mult(B,A)),A)),
inference(paramod,[status(thm)],[c_449,c_364]) ).
cnf(c_453,plain,
mult(A,mult(ld(A,mult(B,A)),A)) = mult(mult(A,mult(ld(A,B),A)),A),
inference(copy,[status(thm)],[c_914]) ).
cnf(c_456,plain,
rd(mult(A,ld(mult(A,A),B)),A) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_349,c_4]) ).
cnf(c_915,plain,
rd(mult(A,ld(A,ld(mult(A,A),B))),A) = ld(A,rd(ld(A,B),A)),
inference(paramod,[status(thm)],[c_174,c_456]) ).
cnf(c_660,plain,
rd(ld(mult(A,A),B),A) = ld(A,rd(ld(A,B),A)),
inference(paramod,[status(thm)],[c_1,c_915]) ).
cnf(c_672,plain,
rd(ld(A,mult(ld(A,B),A)),A) = ld(A,rd(ld(A,mult(B,A)),A)),
inference(paramod,[status(thm)],[c_348,c_660]) ).
cnf(c_916,plain,
rd(ld(A,mult(ld(A,mult(mult(A,B),A)),A)),A) = ld(A,rd(ld(A,mult(A,mult(mult(B,A),A))),A)),
inference(paramod,[status(thm)],[c_30,c_672]) ).
cnf(c_917,plain,
rd(ld(A,mult(mult(A,mult(ld(A,B),A)),A)),A) = ld(A,rd(ld(A,mult(A,mult(mult(B,A),A))),A)),
inference(paramod,[status(thm)],[c_449,c_916]) ).
cnf(c_918,plain,
rd(mult(A,mult(ld(A,mult(ld(A,B),A)),A)),A) = ld(A,rd(ld(A,mult(A,mult(mult(B,A),A))),A)),
inference(paramod,[status(thm)],[c_449,c_917]) ).
cnf(c_919,plain,
rd(mult(mult(A,mult(ld(A,ld(A,B)),A)),A),A) = ld(A,rd(ld(A,mult(A,mult(mult(B,A),A))),A)),
inference(paramod,[status(thm)],[c_453,c_918]) ).
cnf(c_920,plain,
mult(A,mult(ld(A,ld(A,B)),A)) = ld(A,rd(ld(A,mult(A,mult(mult(B,A),A))),A)),
inference(paramod,[status(thm)],[c_4,c_919]) ).
cnf(c_921,plain,
mult(A,mult(ld(A,ld(A,B)),A)) = ld(A,rd(mult(mult(B,A),A),A)),
inference(paramod,[status(thm)],[c_2,c_920]) ).
cnf(c_880,plain,
mult(A,mult(ld(A,ld(A,B)),A)) = ld(A,mult(B,A)),
inference(paramod,[status(thm)],[c_4,c_921]) ).
cnf(c_888,plain,
mult(mult(A,B),ld(B,mult(C,B))) = mult(mult(A,C),B),
inference(paramod,[status(thm)],[c_880,c_188]) ).
cnf(c_889,plain,
$false,
inference(resolve,[status(thm)],[c_888,c_11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP699-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 15:39:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3277580 was started by sandbox2 on n020,
% 0.09/0.37 % Fri Sep 25 15:39:19 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 2.66/0.81
% 2.66/0.81 % SZS status Unsatisfiable for theBenchmark
% 2.66/0.81
% 2.66/0.81 % Proof 1 at 0.34 (+ 0.08) seconds.
% 2.66/0.81 % Length of proof is 35.
% 2.66/0.81 % Level of proof is 12.
% 2.66/0.81 % Maximum clause weight is 74.000.
% 2.66/0.81 % Given clauses 106.
% 2.66/0.81
% 2.66/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------