%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT392-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.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 : Fri Sep 25 01:59:47 PM UTC 2026
% Result : Unsatisfiable 179.42s 33.41s
% Output : CNFRefutation 179.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 6
% Syntax : Number of formulae : 148 ( 148 unt; 4 def)
% Number of atoms : 466 ( 147 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 19 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 235 ( 0 sgn 235 !; 0 ?; 227 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(mult(plus(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)),plus(mult(plus(X1,plus(plus(mult(X3,mult(X1,X4)),mult(X5,X1)),X1)),plus(X6,mult(X1,plus(plus(mult(X1,X7),mult(X5,X1)),X1)))),mult(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos) ).
fof(f2,negated_conjecture,
plus(plus(mult(a,b),mult(b,c)),b) != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f3,plain,
b != plus(plus(mult(a,b),mult(b,c)),b),
inference(reorient_equations,[],[f2]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(mult(plus(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)),plus(mult(plus(X1,plus(plus(mult(X3,mult(X1,X4)),mult(X5,X1)),X1)),plus(X6,mult(X1,plus(plus(mult(X1,X7),mult(X5,X1)),X1)))),mult(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
plus(plus(mult(a,b),mult(b,c)),b) != b,
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,definition,
iPr_def_10 = mult(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_63,definition,
iPr_def_11 = mult(b,c),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_64,definition,
iPr_def_12 = plus(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_65,definition,
iPr_def_13 = plus(iPr_def_12,b),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_66,negated_conjecture,
iPr_def_13 != b,
inference(demodulation,[status(thm)],[c_52,c_63,c_62,c_64,c_65]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(mult(plus(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)),plus(mult(plus(X1,plus(plus(mult(X3,mult(X1,X4)),mult(X5,X1)),X1)),plus(X6,mult(X1,plus(plus(mult(X1,X7),mult(X5,X1)),X1)))),mult(X0,mult(mult(plus(X3,X1),plus(X1,X4)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(plus(mult(plus(X0,mult(plus(X1,X2),plus(X2,mult(X1,X2)))),plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),mult(X0,mult(plus(X1,X2),plus(X2,mult(X1,X2)))))),X3),plus(mult(plus(X0,mult(mult(plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),mult(plus(X1,X2),plus(X2,mult(X1,X2)))),plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),X4)),mult(plus(X1,X2),plus(X2,mult(X1,X2))))),plus(X2,mult(X0,mult(mult(plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),mult(plus(X1,X2),plus(X2,mult(X1,X2)))),plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),X4)),mult(plus(X1,X2),plus(X2,mult(X1,X2))))))),mult(mult(plus(X0,mult(plus(X1,X2),plus(X2,mult(X1,X2)))),plus(mult(plus(X1,X2),plus(X2,mult(X1,X2))),mult(X0,mult(plus(X1,X2),plus(X2,mult(X1,X2)))))),X3))) = mult(plus(X1,X2),plus(X2,mult(X1,X2))),
inference(superposition,[status(thm)],[c_67,c_67]) ).
tcf(c_1004,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X3)),X1)),plus(mult(plus(X4,mult(mult(plus(X5,X1),plus(X1,X6)),X1)),plus(mult(plus(X1,plus(plus(mult(X5,mult(X1,X6)),mult(X7,X1)),X1)),plus(X8,mult(X1,plus(plus(mult(X1,X9),mult(X7,X1)),X1)))),mult(X4,mult(mult(plus(X5,X1),plus(X1,X6)),X1)))),mult(X0,mult(mult(plus(X1,X1),plus(X1,X3)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
inference(superposition,[status(thm)],[c_67,c_190]) ).
tcf(c_3214,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1),plus(X1,mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1))),X2),plus(X1,mult(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1),plus(X1,mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1))),X2))) = X1,
inference(superposition,[status(thm)],[c_67,c_1004]) ).
tcf(c_3332,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X1),plus(X0,mult(X0,X1))) = X0,
inference(superposition,[status(thm)],[c_3214,c_3214]) ).
tcf(c_3963,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X3)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X3)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
inference(superposition,[status(thm)],[c_3332,c_67]) ).
tcf(c_5257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1))))),plus(mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1))))))),X3),plus(X1,mult(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1))))),plus(mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)))),mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1))))))),X3))) = mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)))),
inference(superposition,[status(thm)],[c_3963,c_3963]) ).
tcf(c_5300,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)),plus(X1,mult(X0,mult(mult(plus(X1,X1),plus(X1,X2)),X1)))) = X1,
inference(demodulation,[status(thm)],[c_5257,c_3332,c_3963]) ).
tcf(c_5713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(plus(mult(plus(X0,iPr_def_11),plus(iPr_def_11,mult(X0,iPr_def_11))),X1),plus(mult(plus(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X2)),iPr_def_11)),plus(mult(plus(iPr_def_11,plus(plus(mult(iPr_def_10,mult(iPr_def_11,X2)),mult(X3,iPr_def_11)),iPr_def_11)),plus(X4,mult(iPr_def_11,plus(plus(mult(iPr_def_11,X5),mult(X3,iPr_def_11)),iPr_def_11)))),mult(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X2)),iPr_def_11)))),mult(mult(plus(X0,iPr_def_11),plus(iPr_def_11,mult(X0,iPr_def_11))),X1))) = iPr_def_11,
inference(superposition,[status(thm)],[c_64,c_67]) ).
tcf(c_5714,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(plus(mult(plus(X0,b),plus(b,mult(X0,b))),X1),plus(mult(plus(X0,mult(mult(iPr_def_13,plus(b,X2)),b)),plus(mult(plus(b,plus(plus(mult(iPr_def_12,mult(b,X2)),mult(X3,b)),b)),plus(X4,mult(b,plus(plus(mult(b,X5),mult(X3,b)),b)))),mult(X0,mult(mult(iPr_def_13,plus(b,X2)),b)))),mult(mult(plus(X0,b),plus(b,mult(X0,b))),X1))) = b,
inference(superposition,[status(thm)],[c_65,c_67]) ).
tcf(c_5721,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(plus(mult(plus(a,b),plus(b,iPr_def_10)),X0),plus(mult(plus(a,mult(mult(plus(X1,b),plus(b,X2)),b)),plus(mult(plus(b,plus(plus(mult(X1,mult(b,X2)),mult(X3,b)),b)),plus(X4,mult(b,plus(plus(mult(b,X5),mult(X3,b)),b)))),mult(a,mult(mult(plus(X1,b),plus(b,X2)),b)))),mult(mult(plus(a,b),plus(b,iPr_def_10)),X0))) = b,
inference(superposition,[status(thm)],[c_62,c_67]) ).
tcf(c_5725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] : mult(plus(X0,X1),plus(mult(plus(mult(plus(X2,X0),plus(X0,mult(X2,X0))),mult(mult(plus(X3,mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0))))),plus(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),X9)),mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))),plus(mult(plus(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),plus(plus(mult(X3,mult(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),X9)),mult(X10,mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))),mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))),plus(X11,mult(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),plus(plus(mult(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),X12),mult(X10,mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))),mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))))),mult(mult(plus(X2,X0),plus(X0,mult(X2,X0))),mult(mult(plus(X3,mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0))))),plus(mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),X9)),mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))))))),mult(X0,X1))) = mult(plus(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)),plus(mult(plus(X0,plus(plus(mult(X4,mult(X0,X5)),mult(X6,X0)),X0)),plus(X7,mult(X0,plus(plus(mult(X0,X8),mult(X6,X0)),X0)))),mult(X2,mult(mult(plus(X4,X0),plus(X0,X5)),X0)))),
inference(superposition,[status(thm)],[c_67,c_67]) ).
tcf(c_5731,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : mult(plus(X0,mult(mult(plus(X1,X2),plus(X2,X3)),X2)),plus(mult(plus(X2,plus(plus(mult(X1,mult(X2,X3)),mult(X4,X2)),X2)),plus(X5,mult(X2,plus(plus(mult(X2,X6),mult(X4,X2)),X2)))),mult(X0,mult(mult(plus(X1,X2),plus(X2,X3)),X2)))) = X2,
inference(superposition,[status(thm)],[c_67,c_5300]) ).
tcf(c_5742,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1),plus(X1,mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1))),X2),plus(X1,mult(mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1),plus(X1,mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X1))),X2))) = X1,
inference(superposition,[status(thm)],[c_67,c_1004]) ).
tcf(c_5806,plain,
! [X0: $i] : mult(plus(mult(plus(a,b),plus(b,iPr_def_10)),X0),plus(b,mult(mult(plus(a,b),plus(b,iPr_def_10)),X0))) = b,
inference(demodulation,[status(thm)],[c_5721,c_5731]) ).
tcf(c_5842,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X1),plus(X0,mult(X0,X1))) = X0,
inference(demodulation,[status(thm)],[c_5725,c_5731]) ).
tcf(c_5902,plain,
mult(iPr_def_13,plus(iPr_def_12,mult(iPr_def_12,b))) = iPr_def_12,
inference(superposition,[status(thm)],[c_65,c_5842]) ).
tcf(c_5909,plain,
! [X0: $i,X1: $i] : mult(plus(plus(X0,X1),plus(X0,mult(X0,X1))),plus(plus(X0,X1),X0)) = plus(X0,X1),
inference(superposition,[status(thm)],[c_5842,c_5842]) ).
tcf(c_5928,plain,
! [X0: $i,X1: $i] : mult(plus(X0,mult(X1,X1)),plus(X1,mult(X0,mult(X1,X1)))) = X1,
inference(superposition,[status(thm)],[c_5842,c_5300]) ).
tcf(c_6149,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2),plus(X1,mult(mult(plus(X0,X1),plus(X1,mult(X0,X1))),X2))) = X1,
inference(superposition,[status(thm)],[c_5731,c_67]) ).
tcf(c_6305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(plus(X0,plus(plus(mult(X1,mult(X0,X2)),mult(X3,X0)),X0)),plus(X4,mult(X0,plus(plus(mult(X0,X5),mult(X3,X0)),X0)))) = X0,
inference(superposition,[status(thm)],[c_5742,c_5731]) ).
tcf(c_6431,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(plus(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X1)),iPr_def_11)),plus(mult(plus(iPr_def_11,plus(plus(mult(iPr_def_10,mult(iPr_def_11,X1)),mult(X2,iPr_def_11)),iPr_def_11)),plus(X3,mult(iPr_def_11,plus(plus(mult(iPr_def_11,X4),mult(X2,iPr_def_11)),iPr_def_11)))),mult(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X1)),iPr_def_11)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_5713,c_5300]) ).
tcf(c_6473,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(plus(X0,mult(mult(iPr_def_13,plus(b,X1)),b)),plus(mult(plus(b,plus(plus(mult(iPr_def_12,mult(b,X1)),mult(X2,b)),b)),plus(X3,mult(b,plus(plus(mult(b,X4),mult(X2,b)),b)))),mult(X0,mult(mult(iPr_def_13,plus(b,X1)),b)))) = b,
inference(superposition,[status(thm)],[c_5714,c_5300]) ).
tcf(c_6474,plain,
! [X0: $i,X1: $i] : mult(plus(X0,mult(mult(iPr_def_13,plus(b,X1)),b)),plus(b,mult(X0,mult(mult(iPr_def_13,plus(b,X1)),b)))) = b,
inference(demodulation,[status(thm)],[c_6473,c_6305]) ).
tcf(c_6475,plain,
! [X0: $i,X1: $i] : mult(plus(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X1)),iPr_def_11)),plus(iPr_def_11,mult(X0,mult(mult(iPr_def_12,plus(iPr_def_11,X1)),iPr_def_11)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6431,c_6305]) ).
tcf(c_7206,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(b,plus(plus(mult(X0,iPr_def_11),mult(X1,b)),b)),plus(X2,mult(b,plus(plus(mult(b,X3),mult(X1,b)),b)))) = b,
inference(superposition,[status(thm)],[c_63,c_6305]) ).
tcf(c_7215,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(iPr_def_13,plus(plus(mult(X0,iPr_def_12),mult(X1,iPr_def_13)),iPr_def_13)),plus(X2,mult(iPr_def_13,plus(plus(mult(iPr_def_13,X3),mult(X1,iPr_def_13)),iPr_def_13)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_5902,c_6305]) ).
tcf(c_7301,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(b,plus(plus(mult(X0,mult(b,X1)),iPr_def_10),b)),plus(X2,mult(b,plus(plus(mult(b,X3),iPr_def_10),b)))) = b,
inference(superposition,[status(thm)],[c_62,c_6305]) ).
tcf(c_7370,plain,
mult(plus(a,b),plus(b,iPr_def_10)) = b,
inference(superposition,[status(thm)],[c_6305,c_5806]) ).
tcf(c_7375,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X1),plus(X1,mult(X0,X1))) = X1,
inference(superposition,[status(thm)],[c_6305,c_6149]) ).
tcf(c_7815,plain,
mult(plus(plus(a,b),plus(b,iPr_def_10)),plus(plus(b,iPr_def_10),b)) = plus(b,iPr_def_10),
inference(superposition,[status(thm)],[c_7370,c_7375]) ).
tcf(c_7894,plain,
! [X0: $i,X1: $i,X2: $i] : plus(plus(mult(X0,mult(X0,X1)),mult(X2,X0)),X0) = X0,
inference(superposition,[status(thm)],[c_7375,c_6305]) ).
tcf(c_7984,plain,
! [X0: $i] : plus(plus(mult(b,mult(b,X0)),iPr_def_10),b) = b,
inference(superposition,[status(thm)],[c_7301,c_7375]) ).
tcf(c_8699,plain,
! [X0: $i] : mult(b,plus(b,mult(plus(mult(b,mult(b,X0)),iPr_def_10),b))) = b,
inference(superposition,[status(thm)],[c_7984,c_7375]) ).
tcf(c_8719,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(b,plus(plus(mult(X0,mult(b,X1)),iPr_def_10),b)),plus(X2,mult(b,b))) = b,
inference(superposition,[status(thm)],[c_7984,c_7301]) ).
tcf(c_8894,plain,
! [X0: $i,X1: $i,X2: $i] : plus(plus(mult(plus(X0,X1),X0),mult(X2,plus(X0,X1))),plus(X0,X1)) = plus(X0,X1),
inference(superposition,[status(thm)],[c_5842,c_7894]) ).
tcf(c_8990,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,plus(X0,mult(plus(mult(X0,mult(X0,X1)),mult(X2,X0)),X0))) = X0,
inference(superposition,[status(thm)],[c_7894,c_7375]) ).
tcf(c_9040,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(b,plus(plus(mult(X0,iPr_def_11),mult(X1,b)),b)),plus(X2,mult(b,b))) = b,
inference(superposition,[status(thm)],[c_7894,c_7206]) ).
tcf(c_9054,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(plus(X0,X0),plus(X1,mult(X0,plus(plus(mult(X0,X2),mult(X3,X0)),X0)))) = X0,
inference(superposition,[status(thm)],[c_7894,c_6305]) ).
tcf(c_9067,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(iPr_def_13,plus(plus(mult(X0,iPr_def_12),mult(X1,iPr_def_13)),iPr_def_13)),plus(X2,mult(iPr_def_13,iPr_def_13))) = iPr_def_13,
inference(superposition,[status(thm)],[c_7894,c_7215]) ).
tcf(c_10285,plain,
! [X0: $i,X1: $i] : plus(plus(mult(X0,X0),mult(X1,X0)),X0) = X0,
inference(superposition,[status(thm)],[c_8990,c_7894]) ).
tcf(c_10328,plain,
plus(plus(mult(b,b),iPr_def_10),b) = b,
inference(superposition,[status(thm)],[c_8990,c_7984]) ).
tcf(c_10922,plain,
plus(plus(mult(plus(b,iPr_def_10),plus(b,iPr_def_10)),b),plus(b,iPr_def_10)) = plus(b,iPr_def_10),
inference(superposition,[status(thm)],[c_7370,c_10285]) ).
tcf(c_13220,plain,
! [X0: $i,X1: $i] : mult(plus(b,plus(plus(mult(X0,b),iPr_def_10),b)),plus(X1,mult(b,b))) = b,
inference(superposition,[status(thm)],[c_8699,c_8719]) ).
tcf(c_14210,plain,
! [X0: $i] : mult(plus(b,plus(plus(iPr_def_10,iPr_def_10),b)),plus(X0,mult(b,b))) = b,
inference(superposition,[status(thm)],[c_62,c_13220]) ).
tcf(c_14559,plain,
! [X0: $i] : plus(plus(mult(b,plus(mult(b,b),iPr_def_10)),mult(X0,b)),b) = b,
inference(superposition,[status(thm)],[c_10328,c_8894]) ).
tcf(c_14574,plain,
! [X0: $i,X1: $i,X2: $i] : plus(plus(mult(X0,plus(mult(X0,X0),mult(X1,X0))),mult(X2,X0)),X0) = X0,
inference(superposition,[status(thm)],[c_10285,c_8894]) ).
tcf(c_18956,plain,
! [X0: $i,X1: $i,X2: $i] : mult(plus(X0,X0),mult(X0,plus(plus(mult(X0,X1),mult(X2,X0)),X0))) = X0,
inference(superposition,[status(thm)],[c_7894,c_9054]) ).
tcf(c_18980,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X0),plus(X1,mult(X0,X0))) = X0,
inference(superposition,[status(thm)],[c_14574,c_9054]) ).
tcf(c_19829,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(plus(X0,X1),plus(X1,X2)),X1) = X1,
inference(superposition,[status(thm)],[c_18980,c_5731]) ).
tcf(c_19831,plain,
! [X0: $i] : mult(X0,X0) = X0,
inference(superposition,[status(thm)],[c_18980,c_5928]) ).
tcf(c_19839,plain,
! [X0: $i] : mult(mult(iPr_def_13,plus(b,X0)),b) = b,
inference(superposition,[status(thm)],[c_18980,c_6474]) ).
tcf(c_19840,plain,
! [X0: $i] : mult(mult(iPr_def_12,plus(iPr_def_11,X0)),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_18980,c_6475]) ).
tcf(c_19927,plain,
! [X0: $i] : mult(plus(X0,X0),mult(X0,X0)) = X0,
inference(superposition,[status(thm)],[c_14574,c_18956]) ).
tcf(c_20306,plain,
! [X0: $i] : mult(plus(X0,X0),X0) = X0,
inference(demodulation,[status(thm)],[c_19927,c_19831]) ).
tcf(c_20667,plain,
plus(plus(mult(b,plus(b,iPr_def_10)),b),b) = b,
inference(superposition,[status(thm)],[c_19831,c_14559]) ).
tcf(c_20728,plain,
plus(plus(b,iPr_def_10),b) = b,
inference(superposition,[status(thm)],[c_19831,c_7984]) ).
tcf(c_20781,plain,
! [X0: $i,X1: $i] : mult(plus(mult(mult(plus(X0,X0),plus(X0,X1)),X0),mult(mult(plus(X0,X0),plus(X0,X1)),X0)),plus(X0,mult(mult(plus(X0,X0),plus(X0,X1)),X0))) = X0,
inference(superposition,[status(thm)],[c_19831,c_5300]) ).
tcf(c_20786,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X0),plus(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_19831,c_18980]) ).
tcf(c_20789,plain,
! [X0: $i,X1: $i] : plus(plus(X0,mult(X1,X0)),X0) = X0,
inference(superposition,[status(thm)],[c_19831,c_10285]) ).
tcf(c_20820,plain,
! [X0: $i] : plus(plus(X0,X0),X0) = X0,
inference(superposition,[status(thm)],[c_19831,c_10285]) ).
tcf(c_20856,plain,
plus(plus(plus(b,iPr_def_10),b),plus(b,iPr_def_10)) = plus(b,iPr_def_10),
inference(superposition,[status(thm)],[c_19831,c_10922]) ).
tcf(c_20968,plain,
! [X0: $i] : mult(plus(plus(X0,X0),X0),plus(plus(X0,X0),X0)) = plus(X0,X0),
inference(superposition,[status(thm)],[c_20306,c_5842]) ).
tcf(c_20982,plain,
! [X0: $i,X1: $i] : plus(plus(mult(X0,mult(X0,X1)),X0),X0) = X0,
inference(superposition,[status(thm)],[c_20306,c_7894]) ).
tcf(c_21193,plain,
plus(b,plus(b,iPr_def_10)) = plus(b,iPr_def_10),
inference(demodulation,[status(thm)],[c_20856,c_20728]) ).
tcf(c_21204,plain,
! [X0: $i] : plus(X0,X0) = mult(X0,X0),
inference(demodulation,[status(thm)],[c_20968,c_20820]) ).
tcf(c_21205,plain,
! [X0: $i] : plus(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_21204,c_19831]) ).
tcf(c_21283,plain,
! [X0: $i,X1: $i] : mult(mult(X0,plus(X0,X1)),X0) = X0,
inference(demodulation,[status(thm)],[c_20781,c_20786,c_21205]) ).
tcf(c_21756,plain,
! [X0: $i,X1: $i] : mult(X0,plus(X1,mult(X0,X0))) = X0,
inference(superposition,[status(thm)],[c_21205,c_18980]) ).
tcf(c_22186,plain,
! [X0: $i,X1: $i] : mult(X0,plus(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_21756,c_19831]) ).
tcf(c_22800,plain,
mult(iPr_def_11,iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_64,c_22186]) ).
tcf(c_22971,plain,
mult(iPr_def_12,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_22186,c_19840]) ).
tcf(c_22974,plain,
mult(iPr_def_13,b) = b,
inference(superposition,[status(thm)],[c_22186,c_19839]) ).
tcf(c_23138,plain,
plus(plus(plus(plus(b,iPr_def_10),b),plus(b,iPr_def_10)),plus(plus(b,iPr_def_10),b)) = plus(plus(b,iPr_def_10),b),
inference(superposition,[status(thm)],[c_7815,c_20789]) ).
tcf(c_23359,plain,
plus(plus(b,plus(b,iPr_def_10)),b) = b,
inference(demodulation,[status(thm)],[c_23138,c_20728]) ).
tcf(c_28411,plain,
! [X0: $i,X1: $i] : mult(b,plus(plus(mult(X0,iPr_def_11),mult(X1,b)),b)) = plus(plus(mult(X0,iPr_def_11),mult(X1,b)),b),
inference(superposition,[status(thm)],[c_9040,c_19829]) ).
tcf(c_28413,plain,
! [X0: $i,X1: $i] : mult(iPr_def_13,plus(plus(mult(X0,iPr_def_12),mult(X1,iPr_def_13)),iPr_def_13)) = plus(plus(mult(X0,iPr_def_12),mult(X1,iPr_def_13)),iPr_def_13),
inference(superposition,[status(thm)],[c_9067,c_19829]) ).
tcf(c_28428,plain,
! [X0: $i] : mult(b,plus(plus(mult(X0,b),iPr_def_10),b)) = plus(plus(mult(X0,b),iPr_def_10),b),
inference(superposition,[status(thm)],[c_13220,c_19829]) ).
tcf(c_28431,plain,
mult(b,plus(plus(iPr_def_10,iPr_def_10),b)) = plus(plus(iPr_def_10,iPr_def_10),b),
inference(superposition,[status(thm)],[c_14210,c_19829]) ).
tcf(c_28435,plain,
! [X0: $i,X1: $i] : mult(plus(X0,X1),X1) = X1,
inference(superposition,[status(thm)],[c_22186,c_19829]) ).
tcf(c_28830,plain,
mult(mult(plus(mult(b,plus(b,iPr_def_10)),b),b),plus(mult(b,plus(b,iPr_def_10)),b)) = plus(mult(b,plus(b,iPr_def_10)),b),
inference(superposition,[status(thm)],[c_20667,c_21283]) ).
tcf(c_28886,plain,
plus(iPr_def_10,b) = b,
inference(demodulation,[status(thm)],[c_28431,c_21205,c_22186]) ).
tcf(c_28902,plain,
! [X0: $i] : plus(plus(mult(X0,b),iPr_def_10),b) = b,
inference(demodulation,[status(thm)],[c_28428,c_22186]) ).
tcf(c_28912,plain,
! [X0: $i,X1: $i] : plus(plus(mult(X0,iPr_def_12),mult(X1,iPr_def_13)),iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_28413,c_22186]) ).
tcf(c_28914,plain,
! [X0: $i,X1: $i] : plus(plus(mult(X0,iPr_def_11),mult(X1,b)),b) = b,
inference(demodulation,[status(thm)],[c_28411,c_22186]) ).
tcf(c_28922,plain,
mult(b,plus(mult(b,plus(b,iPr_def_10)),b)) = plus(mult(b,plus(b,iPr_def_10)),b),
inference(demodulation,[status(thm)],[c_28830,c_28435]) ).
tcf(c_28923,plain,
plus(mult(b,plus(b,iPr_def_10)),b) = b,
inference(demodulation,[status(thm)],[c_28922,c_22186]) ).
tcf(c_29241,plain,
mult(mult(iPr_def_10,b),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_28886,c_21283]) ).
tcf(c_29258,plain,
! [X0: $i] : mult(mult(plus(X0,iPr_def_10),b),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_28886,c_19829]) ).
tcf(c_29389,plain,
! [X0: $i,X1: $i] : mult(plus(plus(X0,X1),X1),plus(plus(X0,X1),X1)) = plus(X0,X1),
inference(superposition,[status(thm)],[c_28435,c_5842]) ).
tcf(c_29814,plain,
! [X0: $i,X1: $i] : plus(plus(X0,X1),X1) = plus(X0,X1),
inference(demodulation,[status(thm)],[c_29389,c_19831]) ).
tcf(c_30137,plain,
mult(plus(mult(iPr_def_10,b),iPr_def_10),plus(mult(iPr_def_10,b),iPr_def_10)) = mult(iPr_def_10,b),
inference(superposition,[status(thm)],[c_29241,c_5842]) ).
tcf(c_30373,plain,
mult(b,plus(mult(b,plus(b,iPr_def_10)),mult(mult(b,plus(b,iPr_def_10)),b))) = mult(b,plus(b,iPr_def_10)),
inference(superposition,[status(thm)],[c_28923,c_5842]) ).
tcf(c_30968,plain,
plus(mult(iPr_def_10,b),iPr_def_10) = mult(iPr_def_10,b),
inference(demodulation,[status(thm)],[c_30137,c_19831]) ).
tcf(c_30983,plain,
mult(b,plus(b,iPr_def_10)) = b,
inference(demodulation,[status(thm)],[c_30373,c_19831,c_21283,c_28923]) ).
tcf(c_32404,plain,
mult(plus(plus(b,plus(b,iPr_def_10)),plus(b,b)),plus(plus(b,plus(b,iPr_def_10)),b)) = plus(b,plus(b,iPr_def_10)),
inference(superposition,[status(thm)],[c_30983,c_5909]) ).
tcf(c_32406,plain,
mult(plus(b,plus(b,iPr_def_10)),plus(b,b)) = b,
inference(superposition,[status(thm)],[c_30983,c_5842]) ).
tcf(c_32704,plain,
plus(mult(iPr_def_10,b),b) = b,
inference(superposition,[status(thm)],[c_30968,c_28902]) ).
tcf(c_32856,plain,
mult(plus(b,iPr_def_10),b) = b,
inference(demodulation,[status(thm)],[c_32406,c_21193,c_21205]) ).
tcf(c_32888,plain,
plus(b,iPr_def_10) = b,
inference(demodulation,[status(thm)],[c_32404,c_19831,c_20728,c_21193,c_21205,c_23359]) ).
tcf(c_33269,plain,
mult(iPr_def_10,b) = iPr_def_10,
inference(superposition,[status(thm)],[c_32888,c_22186]) ).
tcf(c_33313,plain,
! [X0: $i] : plus(plus(mult(b,mult(iPr_def_10,b)),mult(X0,b)),b) = b,
inference(superposition,[status(thm)],[c_32704,c_8894]) ).
tcf(c_33577,plain,
mult(b,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_32856,c_29258]) ).
tcf(c_33770,plain,
! [X0: $i] : plus(plus(iPr_def_10,mult(X0,b)),b) = b,
inference(demodulation,[status(thm)],[c_33313,c_33577,c_33269]) ).
tcf(c_36198,plain,
! [X0: $i,X1: $i] : plus(plus(X0,plus(X1,X0)),plus(X1,X0)) = plus(X1,X0),
inference(superposition,[status(thm)],[c_28435,c_20982]) ).
tcf(c_36416,plain,
! [X0: $i,X1: $i] : plus(mult(X0,mult(X0,X1)),X0) = X0,
inference(superposition,[status(thm)],[c_20982,c_29814]) ).
tcf(c_36441,plain,
! [X0: $i,X1: $i] : plus(X0,plus(X1,X0)) = plus(X1,X0),
inference(demodulation,[status(thm)],[c_36198,c_29814]) ).
tcf(c_39124,plain,
! [X0: $i] : mult(mult(iPr_def_13,plus(X0,b)),b) = b,
inference(superposition,[status(thm)],[c_36441,c_19839]) ).
tcf(c_40933,plain,
! [X0: $i] : plus(plus(mult(X0,iPr_def_12),iPr_def_13),iPr_def_13) = iPr_def_13,
inference(superposition,[status(thm)],[c_28435,c_28912]) ).
tcf(c_41103,plain,
! [X0: $i] : plus(plus(mult(X0,iPr_def_11),b),b) = b,
inference(superposition,[status(thm)],[c_39124,c_28914]) ).
tcf(c_41147,plain,
! [X0: $i] : plus(mult(X0,iPr_def_11),b) = b,
inference(demodulation,[status(thm)],[c_41103,c_29814]) ).
tcf(c_41149,plain,
! [X0: $i] : plus(mult(X0,iPr_def_12),iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_40933,c_29814]) ).
tcf(c_41444,plain,
plus(iPr_def_11,b) = b,
inference(superposition,[status(thm)],[c_22971,c_41147]) ).
tcf(c_41574,plain,
plus(iPr_def_11,iPr_def_13) = iPr_def_13,
inference(superposition,[status(thm)],[c_22800,c_41149]) ).
tcf(c_42561,plain,
! [X0: $i] : mult(mult(plus(X0,iPr_def_11),b),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_41444,c_19829]) ).
tcf(c_42610,plain,
mult(mult(iPr_def_11,iPr_def_13),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_41574,c_21283]) ).
tcf(c_42614,plain,
mult(iPr_def_13,plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))) = iPr_def_13,
inference(superposition,[status(thm)],[c_41574,c_7375]) ).
tcf(c_42618,plain,
mult(iPr_def_13,plus(iPr_def_11,mult(iPr_def_11,iPr_def_13))) = iPr_def_11,
inference(superposition,[status(thm)],[c_41574,c_5842]) ).
tcf(c_44129,plain,
plus(iPr_def_11,mult(iPr_def_11,iPr_def_13)) = mult(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_42610,c_36416]) ).
tcf(c_45730,plain,
mult(plus(plus(iPr_def_13,plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))),plus(iPr_def_13,iPr_def_13)),plus(plus(iPr_def_13,plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))),iPr_def_13)) = plus(iPr_def_13,plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))),
inference(superposition,[status(thm)],[c_42614,c_5909]) ).
tcf(c_45750,plain,
plus(plus(plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),iPr_def_13),plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))) = plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),
inference(superposition,[status(thm)],[c_42614,c_20789]) ).
tcf(c_46086,plain,
plus(iPr_def_13,plus(iPr_def_13,mult(iPr_def_11,iPr_def_13))) = plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),
inference(demodulation,[status(thm)],[c_45750,c_20789]) ).
tcf(c_46146,plain,
mult(plus(plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),plus(iPr_def_13,iPr_def_13)),plus(plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),iPr_def_13)) = plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)),
inference(demodulation,[status(thm)],[c_45730,c_46086]) ).
tcf(c_46147,plain,
plus(iPr_def_13,mult(iPr_def_11,iPr_def_13)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_46146,c_19831,c_20789,c_21205]) ).
tcf(c_46668,plain,
mult(iPr_def_13,mult(iPr_def_11,iPr_def_13)) = mult(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_46147,c_28435]) ).
tcf(c_46914,plain,
mult(plus(plus(iPr_def_11,iPr_def_13),mult(iPr_def_11,iPr_def_13)),plus(plus(iPr_def_11,iPr_def_13),iPr_def_11)) = plus(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_44129,c_5909]) ).
tcf(c_46920,plain,
mult(iPr_def_13,mult(iPr_def_11,iPr_def_13)) = iPr_def_11,
inference(superposition,[status(thm)],[c_44129,c_42618]) ).
tcf(c_47090,plain,
mult(iPr_def_11,iPr_def_13) = iPr_def_11,
inference(demodulation,[status(thm)],[c_46668,c_46920]) ).
tcf(c_47166,plain,
mult(plus(plus(iPr_def_11,iPr_def_13),iPr_def_11),plus(plus(iPr_def_11,iPr_def_13),iPr_def_11)) = plus(iPr_def_11,iPr_def_13),
inference(demodulation,[status(thm)],[c_46914,c_47090]) ).
tcf(c_47167,plain,
plus(iPr_def_13,iPr_def_11) = iPr_def_13,
inference(demodulation,[status(thm)],[c_47166,c_19831,c_41574]) ).
tcf(c_47867,plain,
mult(mult(iPr_def_13,b),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_47167,c_42561]) ).
tcf(c_48027,plain,
mult(b,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_47867,c_22974]) ).
tcf(c_48354,plain,
mult(plus(b,iPr_def_11),plus(b,iPr_def_11)) = b,
inference(superposition,[status(thm)],[c_48027,c_5842]) ).
tcf(c_48790,plain,
plus(b,iPr_def_11) = b,
inference(demodulation,[status(thm)],[c_48354,c_19831]) ).
tcf(c_48969,plain,
mult(iPr_def_11,b) = iPr_def_11,
inference(superposition,[status(thm)],[c_48790,c_22186]) ).
tcf(c_50095,plain,
plus(plus(iPr_def_10,iPr_def_11),b) = b,
inference(superposition,[status(thm)],[c_48969,c_33770]) ).
tcf(c_50713,plain,
b = iPr_def_13,
inference(demodulation,[status(thm)],[c_50095,c_64,c_65]) ).
tcf(c_51947,plain,
$false,
inference(superposition,[status(thm)],[c_50713,c_66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT392-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 21:34:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running UEQ theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 179.42/33.41 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 179.42/33.41 % SZS status Started for theBenchmark.p
% 179.42/33.41 % SZS status Unsatisfiable for theBenchmark.p
% 179.42/33.41
% 179.42/33.41 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 179.42/33.41
% 179.42/33.41 % ------ iProver source info
% 179.42/33.41
% 179.42/33.41 % git: date: 2026-07-19 20:42:38 +0200
% 179.42/33.41 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 179.42/33.41 % git: non_committed_changes: false
% 179.42/33.41
% 179.42/33.41 % ------ Parsing...% successful
% 179.42/33.41
% 179.42/33.41
% 179.42/33.41 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 179.42/33.41
% 179.42/33.41 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 179.42/33.41
% 179.42/33.41 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 179.42/33.41
% 179.42/33.41 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 179.42/33.41 % ------ Proving...
% 179.42/33.41 % ------ Problem Properties
% 179.42/33.41
% 179.42/33.41 %
% 179.42/33.41 % clauses 6
% 179.42/33.41 % conjectures 1
% 179.42/33.41 % EPR 1
% 179.42/33.41 % Horn 6
% 179.42/33.41 % unary 6
% 179.42/33.41 % binary 0
% 179.42/33.41 % lits 6
% 179.42/33.41 % lits eq 6
% 179.42/33.41 % fd_pure 0
% 179.42/33.41 % fd_pseudo 0
% 179.42/33.41 % fd_cond 0
% 179.42/33.41 % fd_pseudo_cond 0
% 179.42/33.41 % AC symbols 0
% 179.42/33.41
% 179.42/33.41 % ------ Input Options Time Limit: Unbounded
% 179.42/33.41
% 179.42/33.41
% 179.42/33.41 % ------
% 179.42/33.41 % Current options:
% 179.42/33.41 % ------
% 179.42/33.41
% 179.42/33.41
% 179.42/33.41 %
% 179.42/33.41
% 179.42/33.41 % ------ Proving...
% 179.42/33.41 %
% 179.42/33.41
% 179.42/33.41 % SZS status Unsatisfiable for theBenchmark.p
% 179.42/33.41
% 179.42/33.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 179.42/33.41
% 179.42/33.41
%------------------------------------------------------------------------------