%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KLE028+3 : 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 : n001.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:44:08 AM UTC 2026
% Result : Theorem 67.40s 9.04s
% Output : CNFRefutation 67.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 10
% Syntax : Number of formulae : 143 ( 100 unt; 0 def)
% Number of atoms : 212 ( 156 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 136 ( 67 ~; 53 |; 9 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 133 ( 1 sgn 31 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(additive_commutativity,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('theBenchmark.p',additive_commutativity) ).
fof(additive_associativity,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('theBenchmark.p',additive_associativity) ).
fof(multiplicative_associativity,axiom,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
file('theBenchmark.p',multiplicative_associativity) ).
fof(multiplicative_left_identity,axiom,
! [A] : multiplication(one,A) = A,
file('theBenchmark.p',multiplicative_left_identity) ).
fof(right_distributivity,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('theBenchmark.p',right_distributivity) ).
fof(test_1,axiom,
! [X0] :
( test(X0)
<=> ? [X1] : complement(X1,X0) ),
file('theBenchmark.p',test_1) ).
fof(test_2,axiom,
! [X0,X1] :
( complement(X1,X0)
<=> ( addition(X0,X1) = one
& multiplication(X1,X0) = zero
& multiplication(X0,X1) = zero ) ),
file('theBenchmark.p',test_2) ).
fof(test_3,axiom,
! [X0,X1] :
( test(X0)
=> ( c(X0) = X1
<=> complement(X0,X1) ) ),
file('theBenchmark.p',test_3) ).
fof(test_deMorgan1,axiom,
! [X0,X1] :
( ( test(X1)
& test(X0) )
=> c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ),
file('theBenchmark.p',test_deMorgan1) ).
fof(goals,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( test(X5)
& test(X4) )
=> addition(multiplication(X4,addition(multiplication(X5,X0),multiplication(c(X5),X1))),multiplication(c(X4),addition(multiplication(X5,X2),multiplication(c(X5),X3)))) = addition(multiplication(X5,addition(multiplication(X4,X0),multiplication(c(X4),X2))),multiplication(c(X5),addition(multiplication(X4,X1),multiplication(c(X4),X3)))) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( test(X5)
& test(X4) )
=> addition(multiplication(X4,addition(multiplication(X5,X0),multiplication(c(X5),X1))),multiplication(c(X4),addition(multiplication(X5,X2),multiplication(c(X5),X3)))) = addition(multiplication(X5,addition(multiplication(X4,X0),multiplication(c(X4),X2))),multiplication(c(X5),addition(multiplication(X4,X1),multiplication(c(X4),X3)))) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_22,plain,
( complement(A,B)
| c(A) != B
| ~ test(A) ),
inference(clausify,[status(thm)],[test_3]) ).
cnf(c_23,plain,
( ~ complement(A,B)
| c(A) = B
| ~ test(A) ),
inference(clausify,[status(thm)],[test_3]) ).
cnf(c_24,plain,
( addition(B,A) != one
| multiplication(A,B) != zero
| multiplication(B,A) != zero
| complement(A,B) ),
inference(clausify,[status(thm)],[test_2]) ).
cnf(c_25,plain,
( addition(B,A) = one
| ~ complement(A,B) ),
inference(clausify,[status(thm)],[test_2]) ).
cnf(c_26,plain,
( multiplication(A,B) = zero
| ~ complement(A,B) ),
inference(clausify,[status(thm)],[test_2]) ).
cnf(c_27,plain,
( multiplication(B,A) = zero
| ~ complement(A,B) ),
inference(clausify,[status(thm)],[test_2]) ).
cnf(c_28,plain,
( ~ complement(B,A)
| test(A) ),
inference(clausify,[status(thm)],[test_1]) ).
cnf(c_34,plain,
( c(B) != A
| ~ test(B)
| test(A) ),
inference(resolve,[status(thm)],[c_28,c_22]) ).
cnf(c_36,plain,
( c(B) != A
| ~ test(B)
| multiplication(A,B) = zero ),
inference(resolve,[status(thm)],[c_27,c_22]) ).
cnf(c_37,plain,
( c(A) != B
| ~ test(A)
| multiplication(A,B) = zero ),
inference(resolve,[status(thm)],[c_26,c_22]) ).
cnf(c_38,plain,
( c(B) != A
| ~ test(B)
| addition(A,B) = one ),
inference(resolve,[status(thm)],[c_25,c_22]) ).
cnf(c_39,plain,
( c(B) = A
| ~ test(B)
| addition(A,B) != one
| multiplication(B,A) != zero
| multiplication(A,B) != zero ),
inference(resolve,[status(thm)],[c_24,c_23]) ).
cnf(c_40,plain,
addition(A,B) = addition(B,A),
inference(clausify,[status(thm)],[additive_commutativity]) ).
cnf(c_41,plain,
addition(addition(A,B),C) = addition(A,addition(B,C)),
inference(clausify,[status(thm)],[additive_associativity]) ).
cnf(c_44,plain,
multiplication(multiplication(A,B),C) = multiplication(A,multiplication(B,C)),
inference(clausify,[status(thm)],[multiplicative_associativity]) ).
cnf(c_46,plain,
multiplication(one,A) = A,
inference(clausify,[status(thm)],[multiplicative_left_identity]) ).
cnf(c_47,plain,
multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(clausify,[status(thm)],[right_distributivity]) ).
cnf(c_48,plain,
addition(multiplication(A,B),multiplication(A,C)) = multiplication(A,addition(B,C)),
inference(copy,[status(thm)],[c_47]) ).
cnf(c_54,plain,
( c(addition(A,B)) = multiplication(c(A),c(B))
| ~ test(B)
| ~ test(A) ),
inference(clausify,[status(thm)],[test_deMorgan1]) ).
fof(nnf_19,plain,
? [X0,X1,X2,X3,X4,X5] :
( addition(multiplication(X5,addition(multiplication(X4,X0),multiplication(c(X4),X2))),multiplication(c(X5),addition(multiplication(X4,X1),multiplication(c(X4),X3)))) != addition(multiplication(X4,addition(multiplication(X5,X0),multiplication(c(X5),X1))),multiplication(c(X4),addition(multiplication(X5,X2),multiplication(c(X5),X3))))
& test(X5)
& test(X4) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( addition(multiplication(sK1,addition(multiplication(sK0,sK2),multiplication(c(sK0),sK3))),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5)))) != addition(multiplication(sK0,addition(multiplication(sK1,sK2),multiplication(c(sK1),sK4))),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5))))
& test(sK1)
& test(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK4),skolemize(X2,sK3),skolemize(X3,sK5),skolemize(X4,sK0),skolemize(X5,sK1)],[nnf_19]) ).
cnf(c_56,negated_conjecture,
test(sK0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_57,negated_conjecture,
test(sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_58,negated_conjecture,
addition(multiplication(sK1,addition(multiplication(sK0,sK2),multiplication(c(sK0),sK3))),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5)))) != addition(multiplication(sK0,addition(multiplication(sK1,sK2),multiplication(c(sK1),sK4))),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5)))),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_59,negated_conjecture,
addition(multiplication(sK0,addition(multiplication(sK1,sK2),multiplication(c(sK1),sK4))),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5)))) != addition(multiplication(sK1,addition(multiplication(sK0,sK2),multiplication(c(sK0),sK3))),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5)))),
inference(copy,[status(thm)],[c_58]) ).
cnf(c_1960,plain,
addition(addition(A,B),C) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_40,c_41]) ).
cnf(c_65,plain,
addition(A,addition(B,C)) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_41,c_1960]) ).
cnf(c_71,plain,
addition(multiplication(A,addition(B,C)),D) = addition(multiplication(A,B),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_48,c_41]) ).
cnf(c_1961,negated_conjecture,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5))))) != addition(multiplication(sK1,addition(multiplication(sK0,sK2),multiplication(c(sK0),sK3))),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5)))),
inference(paramod,[status(thm)],[c_71,c_59]) ).
cnf(c_74,negated_conjecture,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5))))) != addition(multiplication(sK1,multiplication(sK0,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_71,c_1961]) ).
cnf(c_1962,negated_conjecture,
( c(sK0) != A
| addition(A,sK0) = one ),
inference(resolve,[status(thm)],[c_38,c_56]) ).
cnf(c_1963,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1964,negated_conjecture,
addition(multiplication(one,c(sK0)),sK0) = one,
inference(resolve,[status(thm)],[c_1962,c_1963]) ).
cnf(c_1965,negated_conjecture,
addition(c(sK0),sK0) = one,
inference(paramod,[status(thm)],[c_46,c_1964]) ).
cnf(c_124,negated_conjecture,
addition(sK0,c(sK0)) = one,
inference(paramod,[status(thm)],[c_40,c_1965]) ).
cnf(c_1966,negated_conjecture,
( c(sK0) != A
| multiplication(sK0,A) = zero ),
inference(resolve,[status(thm)],[c_37,c_56]) ).
cnf(c_1967,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1968,negated_conjecture,
multiplication(sK0,multiplication(one,c(sK0))) = zero,
inference(resolve,[status(thm)],[c_1966,c_1967]) ).
cnf(c_125,negated_conjecture,
multiplication(sK0,c(sK0)) = zero,
inference(paramod,[status(thm)],[c_46,c_1968]) ).
cnf(c_1969,negated_conjecture,
( c(sK0) != A
| multiplication(A,sK0) = zero ),
inference(resolve,[status(thm)],[c_36,c_56]) ).
cnf(c_1970,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1971,negated_conjecture,
multiplication(multiplication(one,c(sK0)),sK0) = zero,
inference(resolve,[status(thm)],[c_1969,c_1970]) ).
cnf(c_126,negated_conjecture,
multiplication(c(sK0),sK0) = zero,
inference(paramod,[status(thm)],[c_46,c_1971]) ).
cnf(c_1972,negated_conjecture,
( c(sK0) != A
| test(A) ),
inference(resolve,[status(thm)],[c_34,c_56]) ).
cnf(c_1973,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1974,negated_conjecture,
test(multiplication(one,c(sK0))),
inference(resolve,[status(thm)],[c_1972,c_1973]) ).
cnf(c_127,negated_conjecture,
test(c(sK0)),
inference(paramod,[status(thm)],[c_46,c_1974]) ).
cnf(c_1975,negated_conjecture,
( c(addition(sK0,A)) = multiplication(c(sK0),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_56]) ).
cnf(c_148,negated_conjecture,
c(addition(sK0,sK1)) = multiplication(c(sK0),c(sK1)),
inference(resolve,[status(thm)],[c_1975,c_57]) ).
cnf(c_1976,negated_conjecture,
( c(addition(sK1,A)) = multiplication(c(sK1),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_57]) ).
cnf(c_1977,negated_conjecture,
c(addition(sK1,sK0)) = multiplication(c(sK1),c(sK0)),
inference(resolve,[status(thm)],[c_1976,c_56]) ).
cnf(c_1978,negated_conjecture,
c(addition(sK0,sK1)) = multiplication(c(sK1),c(sK0)),
inference(paramod,[status(thm)],[c_40,c_1977]) ).
cnf(c_1979,negated_conjecture,
multiplication(c(sK0),c(sK1)) = multiplication(c(sK1),c(sK0)),
inference(paramod,[status(thm)],[c_148,c_1978]) ).
cnf(c_150,negated_conjecture,
multiplication(c(sK1),c(sK0)) = multiplication(c(sK0),c(sK1)),
inference(copy,[status(thm)],[c_1979]) ).
cnf(c_1980,negated_conjecture,
( c(sK1) != A
| addition(A,sK1) = one ),
inference(resolve,[status(thm)],[c_38,c_57]) ).
cnf(c_1981,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1982,negated_conjecture,
addition(multiplication(one,c(sK1)),sK1) = one,
inference(resolve,[status(thm)],[c_1980,c_1981]) ).
cnf(c_1983,negated_conjecture,
addition(c(sK1),sK1) = one,
inference(paramod,[status(thm)],[c_46,c_1982]) ).
cnf(c_152,negated_conjecture,
addition(sK1,c(sK1)) = one,
inference(paramod,[status(thm)],[c_40,c_1983]) ).
cnf(c_1984,negated_conjecture,
( c(sK1) != A
| multiplication(sK1,A) = zero ),
inference(resolve,[status(thm)],[c_37,c_57]) ).
cnf(c_1985,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1986,negated_conjecture,
multiplication(sK1,multiplication(one,c(sK1))) = zero,
inference(resolve,[status(thm)],[c_1984,c_1985]) ).
cnf(c_153,negated_conjecture,
multiplication(sK1,c(sK1)) = zero,
inference(paramod,[status(thm)],[c_46,c_1986]) ).
cnf(c_1987,negated_conjecture,
( c(sK1) != A
| multiplication(A,sK1) = zero ),
inference(resolve,[status(thm)],[c_36,c_57]) ).
cnf(c_1988,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1989,negated_conjecture,
multiplication(multiplication(one,c(sK1)),sK1) = zero,
inference(resolve,[status(thm)],[c_1987,c_1988]) ).
cnf(c_154,negated_conjecture,
multiplication(c(sK1),sK1) = zero,
inference(paramod,[status(thm)],[c_46,c_1989]) ).
cnf(c_1990,negated_conjecture,
( c(sK1) != A
| test(A) ),
inference(resolve,[status(thm)],[c_34,c_57]) ).
cnf(c_1991,plain,
A = multiplication(one,A),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_1992,negated_conjecture,
test(multiplication(one,c(sK1))),
inference(resolve,[status(thm)],[c_1990,c_1991]) ).
cnf(c_155,negated_conjecture,
test(c(sK1)),
inference(paramod,[status(thm)],[c_46,c_1992]) ).
cnf(c_1993,plain,
addition(A,multiplication(B,addition(C,D))) = addition(multiplication(B,C),addition(A,multiplication(B,D))),
inference(paramod,[status(thm)],[c_48,c_65]) ).
cnf(c_159,plain,
addition(multiplication(A,B),addition(C,multiplication(A,D))) = addition(C,multiplication(A,addition(B,D))),
inference(copy,[status(thm)],[c_1993]) ).
cnf(c_1994,negated_conjecture,
( c(addition(sK1,A)) = multiplication(c(sK1),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_57]) ).
cnf(c_239,negated_conjecture,
c(addition(sK1,c(sK0))) = multiplication(c(sK1),c(c(sK0))),
inference(resolve,[status(thm)],[c_1994,c_127]) ).
cnf(c_1995,plain,
( c(addition(c(sK0),A)) = multiplication(c(c(sK0)),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_127]) ).
cnf(c_1996,negated_conjecture,
c(addition(c(sK0),sK1)) = multiplication(c(c(sK0)),c(sK1)),
inference(resolve,[status(thm)],[c_1995,c_57]) ).
cnf(c_1997,negated_conjecture,
c(addition(sK1,c(sK0))) = multiplication(c(c(sK0)),c(sK1)),
inference(paramod,[status(thm)],[c_40,c_1996]) ).
cnf(c_1998,negated_conjecture,
multiplication(c(sK1),c(c(sK0))) = multiplication(c(c(sK0)),c(sK1)),
inference(paramod,[status(thm)],[c_239,c_1997]) ).
cnf(c_242,negated_conjecture,
multiplication(c(c(sK0)),c(sK1)) = multiplication(c(sK1),c(c(sK0))),
inference(copy,[status(thm)],[c_1998]) ).
cnf(c_1999,plain,
( c(addition(c(sK0),A)) = multiplication(c(c(sK0)),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_127]) ).
cnf(c_268,plain,
c(addition(c(sK0),c(sK1))) = multiplication(c(c(sK0)),c(c(sK1))),
inference(resolve,[status(thm)],[c_1999,c_155]) ).
cnf(c_2000,negated_conjecture,
( c(addition(sK0,A)) = multiplication(c(sK0),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_56]) ).
cnf(c_270,negated_conjecture,
c(addition(sK0,c(sK1))) = multiplication(c(sK0),c(c(sK1))),
inference(resolve,[status(thm)],[c_2000,c_155]) ).
cnf(c_2001,plain,
( c(addition(c(sK1),A)) = multiplication(c(c(sK1)),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_155]) ).
cnf(c_2002,plain,
c(addition(c(sK1),c(sK0))) = multiplication(c(c(sK1)),c(c(sK0))),
inference(resolve,[status(thm)],[c_2001,c_127]) ).
cnf(c_2003,plain,
c(addition(c(sK0),c(sK1))) = multiplication(c(c(sK1)),c(c(sK0))),
inference(paramod,[status(thm)],[c_40,c_2002]) ).
cnf(c_2004,plain,
multiplication(c(c(sK0)),c(c(sK1))) = multiplication(c(c(sK1)),c(c(sK0))),
inference(paramod,[status(thm)],[c_268,c_2003]) ).
cnf(c_272,plain,
multiplication(c(c(sK1)),c(c(sK0))) = multiplication(c(c(sK0)),c(c(sK1))),
inference(copy,[status(thm)],[c_2004]) ).
cnf(c_2005,plain,
( c(addition(c(sK1),A)) = multiplication(c(c(sK1)),c(A))
| ~ test(A) ),
inference(resolve,[status(thm)],[c_54,c_155]) ).
cnf(c_2006,negated_conjecture,
c(addition(c(sK1),sK0)) = multiplication(c(c(sK1)),c(sK0)),
inference(resolve,[status(thm)],[c_2005,c_56]) ).
cnf(c_2007,negated_conjecture,
c(addition(sK0,c(sK1))) = multiplication(c(c(sK1)),c(sK0)),
inference(paramod,[status(thm)],[c_40,c_2006]) ).
cnf(c_2008,negated_conjecture,
multiplication(c(sK0),c(c(sK1))) = multiplication(c(c(sK1)),c(sK0)),
inference(paramod,[status(thm)],[c_270,c_2007]) ).
cnf(c_274,negated_conjecture,
multiplication(c(c(sK1)),c(sK0)) = multiplication(c(sK0),c(c(sK1))),
inference(copy,[status(thm)],[c_2008]) ).
cnf(c_2009,plain,
( c(c(sK0)) = sK0
| ~ test(c(sK0))
| addition(sK0,c(sK0)) != one
| multiplication(c(sK0),sK0) != zero ),
inference(resolve,[status(thm)],[c_39,c_125]) ).
cnf(c_2010,plain,
( c(c(sK0)) = sK0
| ~ test(c(sK0))
| addition(sK0,c(sK0)) != one ),
inference(resolve,[status(thm)],[c_2009,c_126]) ).
cnf(c_2011,plain,
( c(c(sK0)) = sK0
| ~ test(c(sK0)) ),
inference(resolve,[status(thm)],[c_2010,c_124]) ).
cnf(c_441,plain,
c(c(sK0)) = sK0,
inference(resolve,[status(thm)],[c_2011,c_127]) ).
cnf(c_2012,plain,
multiplication(c(c(sK1)),sK0) = multiplication(c(c(sK0)),c(c(sK1))),
inference(paramod,[status(thm)],[c_441,c_272]) ).
cnf(c_453,plain,
multiplication(c(c(sK1)),sK0) = multiplication(sK0,c(c(sK1))),
inference(paramod,[status(thm)],[c_441,c_2012]) ).
cnf(c_2013,negated_conjecture,
multiplication(sK0,c(sK1)) = multiplication(c(sK1),c(c(sK0))),
inference(paramod,[status(thm)],[c_441,c_242]) ).
cnf(c_2014,negated_conjecture,
multiplication(sK0,c(sK1)) = multiplication(c(sK1),sK0),
inference(paramod,[status(thm)],[c_441,c_2013]) ).
cnf(c_457,negated_conjecture,
multiplication(c(sK1),sK0) = multiplication(sK0,c(sK1)),
inference(copy,[status(thm)],[c_2014]) ).
cnf(c_2015,plain,
( c(c(sK1)) = sK1
| ~ test(c(sK1))
| addition(sK1,c(sK1)) != one
| multiplication(c(sK1),sK1) != zero ),
inference(resolve,[status(thm)],[c_39,c_153]) ).
cnf(c_2016,plain,
( c(c(sK1)) = sK1
| ~ test(c(sK1))
| addition(sK1,c(sK1)) != one ),
inference(resolve,[status(thm)],[c_2015,c_154]) ).
cnf(c_2017,plain,
( c(c(sK1)) = sK1
| ~ test(c(sK1)) ),
inference(resolve,[status(thm)],[c_2016,c_152]) ).
cnf(c_537,plain,
c(c(sK1)) = sK1,
inference(resolve,[status(thm)],[c_2017,c_155]) ).
cnf(c_2018,plain,
multiplication(sK1,sK0) = multiplication(sK0,c(c(sK1))),
inference(paramod,[status(thm)],[c_537,c_453]) ).
cnf(c_547,plain,
multiplication(sK1,sK0) = multiplication(sK0,sK1),
inference(paramod,[status(thm)],[c_537,c_2018]) ).
cnf(c_2019,negated_conjecture,
multiplication(sK1,c(sK0)) = multiplication(c(sK0),c(c(sK1))),
inference(paramod,[status(thm)],[c_537,c_274]) ).
cnf(c_2020,negated_conjecture,
multiplication(sK1,c(sK0)) = multiplication(c(sK0),sK1),
inference(paramod,[status(thm)],[c_537,c_2019]) ).
cnf(c_553,negated_conjecture,
multiplication(c(sK0),sK1) = multiplication(sK1,c(sK0)),
inference(copy,[status(thm)],[c_2020]) ).
cnf(c_2021,plain,
multiplication(multiplication(sK0,sK1),A) = multiplication(sK1,multiplication(sK0,A)),
inference(paramod,[status(thm)],[c_547,c_44]) ).
cnf(c_2022,plain,
multiplication(sK0,multiplication(sK1,A)) = multiplication(sK1,multiplication(sK0,A)),
inference(paramod,[status(thm)],[c_44,c_2021]) ).
cnf(c_583,plain,
multiplication(sK1,multiplication(sK0,A)) = multiplication(sK0,multiplication(sK1,A)),
inference(copy,[status(thm)],[c_2022]) ).
cnf(c_591,negated_conjecture,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),addition(multiplication(sK1,sK3),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_583,c_74]) ).
cnf(c_2023,plain,
multiplication(multiplication(sK0,c(sK1)),A) = multiplication(c(sK1),multiplication(sK0,A)),
inference(paramod,[status(thm)],[c_457,c_44]) ).
cnf(c_2024,plain,
multiplication(sK0,multiplication(c(sK1),A)) = multiplication(c(sK1),multiplication(sK0,A)),
inference(paramod,[status(thm)],[c_44,c_2023]) ).
cnf(c_710,plain,
multiplication(c(sK1),multiplication(sK0,A)) = multiplication(sK0,multiplication(c(sK1),A)),
inference(copy,[status(thm)],[c_2024]) ).
cnf(c_2025,plain,
multiplication(multiplication(sK1,c(sK0)),A) = multiplication(c(sK0),multiplication(sK1,A)),
inference(paramod,[status(thm)],[c_553,c_44]) ).
cnf(c_2026,plain,
multiplication(sK1,multiplication(c(sK0),A)) = multiplication(c(sK0),multiplication(sK1,A)),
inference(paramod,[status(thm)],[c_44,c_2025]) ).
cnf(c_719,plain,
multiplication(c(sK0),multiplication(sK1,A)) = multiplication(sK1,multiplication(c(sK0),A)),
inference(copy,[status(thm)],[c_2026]) ).
cnf(c_2027,plain,
multiplication(multiplication(c(sK0),c(sK1)),A) = multiplication(c(sK1),multiplication(c(sK0),A)),
inference(paramod,[status(thm)],[c_150,c_44]) ).
cnf(c_2028,plain,
multiplication(c(sK0),multiplication(c(sK1),A)) = multiplication(c(sK1),multiplication(c(sK0),A)),
inference(paramod,[status(thm)],[c_44,c_2027]) ).
cnf(c_1765,plain,
multiplication(c(sK1),multiplication(c(sK0),A)) = multiplication(c(sK0),multiplication(c(sK1),A)),
inference(copy,[status(thm)],[c_2028]) ).
cnf(c_2029,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(c(sK0),multiplication(sK1,sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_159,c_591]) ).
cnf(c_1861,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),addition(multiplication(sK0,sK4),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_719,c_2029]) ).
cnf(c_2030,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(c(sK1),multiplication(sK0,sK4)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_159,c_1861]) ).
cnf(c_2031,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK1),multiplication(c(sK0),sK5))))),
inference(paramod,[status(thm)],[c_710,c_2030]) ).
cnf(c_2032,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),multiplication(c(sK0),multiplication(c(sK1),sK5))))),
inference(paramod,[status(thm)],[c_1765,c_2031]) ).
cnf(c_2033,plain,
addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))) != addition(multiplication(sK0,multiplication(sK1,sK2)),addition(multiplication(sK1,multiplication(c(sK0),sK3)),addition(multiplication(sK0,multiplication(c(sK1),sK4)),multiplication(c(sK0),multiplication(c(sK1),sK5))))),
inference(paramod,[status(thm)],[c_65,c_2032]) ).
cnf(c_1959,plain,
$false,
inference(copy,[status(thm)],[c_2033]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KLE028+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n001.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.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 19:20:56 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 4013557 was started by sandbox2 on n001,
% 0.16/0.44 % Fri Sep 25 19:20:56 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).
% 67.40/9.04
% 67.40/9.04 % SZS status Theorem for theBenchmark
% 67.40/9.04
% 67.40/9.04 % Proof 1 at 0.41 (+ 0.13) seconds.
% 67.40/9.04 % Length of proof is 66.
% 67.40/9.04 % Level of proof is 11.
% 67.40/9.04 % Maximum clause weight is 84.000.
% 67.40/9.04 % Given clauses 180.
% 67.40/9.04
% 67.40/9.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------