%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP683-11 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:35:11 PM UTC 2026
% Result : Unsatisfiable 9.19s 2.27s
% Output : CNFRefutation 9.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 8
% Syntax : Number of formulae : 248 ( 248 unt; 0 def)
% Number of atoms : 565 ( 247 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 692 ( 0 sgn 692 !; 0 ?; 676 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : ld(X0,mult(X0,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0] : rd(mult(X0,X0),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = ld(X0,mult(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = rd(mult(X0,X1),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : ld(ld(X0,X1),mult(ld(X0,X1),mult(X2,X3))) = mult(ld(X0,mult(X0,X2)),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f6,axiom,
! [X2,X3,X0,X1] : rd(mult(mult(X0,X1),rd(X2,X3)),rd(X2,X3)) = mult(X0,rd(mult(X1,X3),X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
fof(f7,axiom,
! [X0,X1] : ld(X0,mult(X0,ld(X1,X1))) = rd(mult(rd(X0,X0),X1),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
fof(f8,negated_conjecture,
mult(rd(mult(x3,x4),x4),x5) != mult(x3,x5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tcf(c_57,plain,
! [X0: $i] : ld(X0,mult(X0,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_58,plain,
! [X0: $i] : rd(mult(X0,X0),X0) = X0,
inference(cnf_transformation,[],[f2]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = ld(X0,mult(X0,X1)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = rd(mult(X0,X1),X1),
inference(cnf_transformation,[],[f4]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ld(ld(X0,X1),mult(ld(X0,X1),mult(X2,X3))) = mult(ld(X0,mult(X0,X2)),X3),
inference(cnf_transformation,[],[f5]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : rd(mult(mult(X0,X1),rd(X2,X3)),rd(X2,X3)) = mult(X0,rd(mult(X1,X3),X3)),
inference(cnf_transformation,[],[f6]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,ld(X1,X1))) = rd(mult(rd(X0,X0),X1),X1),
inference(cnf_transformation,[],[f7]) ).
tcf(c_64,negated_conjecture,
mult(rd(mult(x3,x4),x4),x5) != mult(x3,x5),
inference(cnf_transformation,[],[f8]) ).
tcf(c_77,plain,
! [X0: $i] : mult(X0,ld(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_57,c_59]) ).
tcf(c_80,plain,
! [X0: $i] : mult(rd(X0,X0),X0) = X0,
inference(demodulation,[status(thm)],[c_58,c_60]) ).
tcf(c_81,plain,
mult(mult(rd(x3,x4),x4),x5) != mult(x3,x5),
inference(demodulation,[status(thm)],[c_64,c_60]) ).
tcf(c_84,plain,
! [X0: $i] : mult(rd(X0,ld(X0,X0)),ld(X0,X0)) = rd(X0,ld(X0,X0)),
inference(superposition,[status(thm)],[c_77,c_60]) ).
tcf(c_85,plain,
! [X0: $i] : mult(rd(rd(X0,X0),X0),X0) = rd(X0,X0),
inference(superposition,[status(thm)],[c_80,c_60]) ).
tcf(c_86,plain,
! [X0: $i] : mult(rd(X0,X0),ld(rd(X0,X0),X0)) = ld(rd(X0,X0),X0),
inference(superposition,[status(thm)],[c_80,c_59]) ).
tcf(c_90,plain,
! [X0: $i] : rd(mult(rd(X0,X0),X0),X0) = ld(X0,X0),
inference(superposition,[status(thm)],[c_77,c_63]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,ld(X1,X1))) = rd(mult(rd(X0,X0),X1),X1),
inference(superposition,[status(thm)],[c_63,c_59]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(X0,mult(X0,rd(X1,X1))),X1) = ld(ld(X0,X2),mult(ld(X0,X2),X1)),
inference(superposition,[status(thm)],[c_80,c_61]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : ld(mult(ld(X0,mult(X0,X1)),X2),mult(mult(ld(X0,mult(X0,X1)),X2),mult(X3,X4))) = mult(ld(ld(X0,X5),mult(ld(X0,X5),X3)),X4),
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3))) = mult(ld(X0,mult(X0,X2)),X3),
inference(superposition,[status(thm)],[c_61,c_59]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(mult(ld(X0,X0),X1),X1)) = rd(mult(X0,rd(X2,X1)),rd(X2,X1)),
inference(superposition,[status(thm)],[c_77,c_62]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X0),rd(mult(X0,X1),X1)) = rd(mult(X0,rd(X2,X1)),rd(X2,X1)),
inference(superposition,[status(thm)],[c_80,c_62]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(mult(X0,X1),rd(X2,X3)),rd(X2,X3)) = mult(X0,rd(mult(X1,X3),X3)),
inference(superposition,[status(thm)],[c_62,c_60]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : rd(mult(mult(X0,X1),mult(X2,rd(mult(X3,X4),X4))),mult(X2,rd(mult(X3,X4),X4))) = mult(X0,rd(mult(X1,rd(X5,X4)),rd(X5,X4))),
inference(superposition,[status(thm)],[c_62,c_62]) ).
tcf(c_115,plain,
! [X0: $i] : mult(rd(rd(X0,X0),X0),X0) = ld(X0,X0),
inference(demodulation,[status(thm)],[c_90,c_60]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i] : mult(rd(rd(X0,X0),X1),X1) = mult(X0,ld(X0,ld(X1,X1))),
inference(demodulation,[status(thm)],[c_92,c_60]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(mult(X0,X1),rd(X2,X3)),rd(X2,X3)) = mult(X0,mult(rd(X1,X3),X3)),
inference(demodulation,[status(thm)],[c_113,c_60]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = mult(rd(X0,X0),mult(rd(X0,X2),X2)),
inference(demodulation,[status(thm)],[c_107,c_60]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = mult(X0,mult(rd(ld(X0,X0),X2),X2)),
inference(demodulation,[status(thm)],[c_106,c_60]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3))) = mult(mult(X0,ld(X0,X2)),X3),
inference(demodulation,[status(thm)],[c_104,c_59]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,ld(X0,rd(X1,X1))),X1) = mult(ld(X0,X2),ld(ld(X0,X2),X1)),
inference(demodulation,[status(thm)],[c_101,c_59]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(rd(mult(X0,X1),mult(X2,mult(rd(X3,X4),X4))),mult(X2,mult(rd(X3,X4),X4))) = mult(X0,mult(rd(X1,rd(X5,X4)),rd(X5,X4))),
inference(demodulation,[status(thm)],[c_114,c_60]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(X0,mult(rd(X1,rd(X2,X3)),rd(X2,X3))) = iPr_def_10(X0,X1,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_128]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(mult(mult(X0,ld(X0,X1)),X2),ld(mult(mult(X0,ld(X0,X1)),X2),mult(X3,X4))) = mult(mult(ld(X0,X5),ld(ld(X0,X5),X3)),X4),
inference(demodulation,[status(thm)],[c_103,c_59]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(mult(ld(X0,X1),ld(ld(X0,X1),X2)),X3) = iPr_def_11(X0,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_131]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(mult(mult(X0,ld(X0,X1)),X2),ld(mult(mult(X0,ld(X0,X1)),X2),mult(X3,X4))) = iPr_def_11(X0,X3,X4),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_131]) ).
tcf(c_227,plain,
! [X0: $i] : ld(X0,X0) = rd(X0,X0),
inference(superposition,[status(thm)],[c_115,c_85]) ).
tcf(c_242,plain,
! [X0: $i] : mult(X0,ld(X0,ld(X0,X0))) = rd(X0,X0),
inference(demodulation,[status(thm)],[c_85,c_116]) ).
tcf(c_243,plain,
! [X0: $i] : mult(X0,ld(X0,rd(X0,X0))) = rd(X0,X0),
inference(demodulation,[status(thm)],[c_242,c_227]) ).
tcf(c_272,plain,
! [X0: $i] : mult(rd(X0,rd(X0,X0)),rd(X0,X0)) = rd(X0,rd(X0,X0)),
inference(demodulation,[status(thm)],[c_84,c_227]) ).
tcf(c_274,plain,
! [X0: $i] : mult(X0,rd(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_77,c_227]) ).
tcf(c_278,plain,
! [X0: $i] : rd(X0,rd(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_272,c_80,c_118]) ).
tcf(c_379,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(mult(X1,rd(X2,X2)),rd(X2,X2))) = rd(mult(mult(X0,X1),X2),X2),
inference(superposition,[status(thm)],[c_278,c_62]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] : mult(X0,mult(X1,rd(X1,X1))) = iPr_def_10(X0,X1,X1),
inference(superposition,[status(thm)],[c_278,c_129]) ).
tcf(c_418,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(rd(X1,X2),X2)) = iPr_def_10(X0,X1,rd(X2,X2)),
inference(superposition,[status(thm)],[c_278,c_129]) ).
tcf(c_419,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(X0,rd(mult(mult(rd(X1,rd(X2,X3)),rd(X2,X3)),X4),X4)) = rd(mult(iPr_def_10(X0,X1,X3),rd(X5,X4)),rd(X5,X4)),
inference(superposition,[status(thm)],[c_129,c_62]) ).
tcf(c_439,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(ld(X0,X1),rd(ld(X0,X1),ld(X0,X1))),X2) = iPr_def_11(X0,ld(X0,X1),X2),
inference(superposition,[status(thm)],[c_227,c_132]) ).
tcf(c_442,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(rd(X0,X0),ld(rd(X0,X0),X1)),X2) = iPr_def_11(X0,X1,X2),
inference(superposition,[status(thm)],[c_227,c_132]) ).
tcf(c_447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(ld(X0,X1),rd(mult(ld(ld(X0,X1),X2),X3),X3)) = rd(iPr_def_11(X0,X2,rd(X4,X3)),rd(X4,X3)),
inference(superposition,[status(thm)],[c_132,c_62]) ).
tcf(c_460,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(X0,mult(rd(mult(rd(X1,rd(X2,X3)),rd(X2,X3)),X4),X4)) = mult(rd(iPr_def_10(X0,X1,X3),rd(X5,X4)),rd(X5,X4)),
inference(superposition,[status(thm)],[c_129,c_117]) ).
tcf(c_490,plain,
! [X0: $i,X1: $i] : mult(rd(X0,rd(X1,X0)),rd(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_80,c_118]) ).
tcf(c_516,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(X0,rd(X1,rd(X2,X3))),rd(X1,rd(X2,X3))) = iPr_def_10(rd(X0,X0),X0,X3),
inference(superposition,[status(thm)],[c_118,c_129]) ).
tcf(c_536,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = mult(X0,mult(rd(rd(X0,X0),X2),X2)),
inference(superposition,[status(thm)],[c_227,c_119]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : rd(mult(mult(X0,mult(rd(ld(X0,X0),X1),X1)),rd(X2,X3)),rd(X2,X3)) = mult(rd(X0,rd(X4,X1)),rd(mult(rd(X4,X1),X3),X3)),
inference(superposition,[status(thm)],[c_119,c_62]) ).
tcf(c_555,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = mult(rd(X0,rd(X3,X2)),rd(X3,X2)),
inference(superposition,[status(thm)],[c_119,c_119]) ).
tcf(c_556,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(X0,rd(X1,rd(X2,X3))),rd(X1,rd(X2,X3))) = iPr_def_10(X0,ld(X0,X0),X3),
inference(superposition,[status(thm)],[c_119,c_129]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(mult(ld(X0,mult(X0,X1)),X2),ld(mult(ld(X0,mult(X0,X1)),X2),mult(X3,X4))) = mult(mult(ld(X0,X5),ld(ld(X0,X5),X3)),X4),
inference(superposition,[status(thm)],[c_61,c_120]) ).
tcf(c_575,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(ld(X0,X1),ld(ld(X0,X1),mult(rd(X2,rd(X3,X4)),rd(X3,X4)))) = mult(mult(X0,ld(X0,X2)),mult(rd(ld(X2,X2),X4),X4)),
inference(superposition,[status(thm)],[c_119,c_120]) ).
tcf(c_582,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(rd(mult(mult(X0,ld(X0,X1)),X2),rd(X3,X4)),rd(X3,X4)) = mult(ld(X0,X5),mult(rd(ld(ld(X0,X5),mult(X1,X2)),X4),X4)),
inference(superposition,[status(thm)],[c_120,c_117]) ).
tcf(c_583,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : mult(ld(X0,X1),rd(mult(ld(ld(X0,X1),mult(X2,X3)),X4),X4)) = rd(mult(mult(mult(X0,ld(X0,X2)),X3),rd(X5,X4)),rd(X5,X4)),
inference(superposition,[status(thm)],[c_120,c_62]) ).
tcf(c_588,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(mult(mult(X0,ld(X0,X1)),X2),X3) = iPr_def_11(X0,mult(X1,X2),X3),
inference(superposition,[status(thm)],[c_120,c_132]) ).
tcf(c_595,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X1),ld(ld(X0,X1),X0)) = mult(rd(X0,X0),X0),
inference(superposition,[status(thm)],[c_243,c_121]) ).
tcf(c_596,plain,
! [X0: $i,X1: $i] : mult(mult(rd(X0,X0),rd(rd(X0,X0),rd(X0,X0))),X0) = mult(ld(rd(X0,X0),X1),ld(ld(rd(X0,X0),X1),X0)),
inference(superposition,[status(thm)],[c_227,c_121]) ).
tcf(c_611,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = mult(ld(X0,X3),ld(ld(X0,X3),X2)),
inference(superposition,[status(thm)],[c_121,c_121]) ).
tcf(c_613,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(ld(X0,X1),X2),ld(ld(ld(X0,X1),X2),X3)) = iPr_def_11(X0,rd(X3,X3),X3),
inference(superposition,[status(thm)],[c_121,c_132]) ).
tcf(c_615,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : rd(mult(mult(mult(X0,ld(X0,rd(X1,X1))),X1),rd(X2,X3)),rd(X2,X3)) = mult(ld(X0,X4),rd(mult(ld(ld(X0,X4),X1),X3),X3)),
inference(superposition,[status(thm)],[c_121,c_62]) ).
tcf(c_622,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(mult(X0,ld(X0,rd(X1,X1))),X1),X2) = iPr_def_11(X0,X1,X2),
inference(superposition,[status(thm)],[c_121,c_132]) ).
tcf(c_623,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1,X1) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_412,c_274]) ).
tcf(c_624,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X1),ld(ld(X0,X1),X0)) = X0,
inference(demodulation,[status(thm)],[c_595,c_80]) ).
tcf(c_634,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = iPr_def_12(X0,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_611]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = iPr_def_13(X0,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_555]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,rd(X0,X0),rd(X1,X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_536,c_418,c_637]) ).
tcf(c_651,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(mult(X0,X1),X2),X2) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_379,c_60,c_129]) ).
tcf(c_656,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,rd(X1,X1),X1) = iPr_def_12(ld(X0,X2),X1),
inference(demodulation,[status(thm)],[c_613,c_634]) ).
tcf(c_658,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,ld(X0,X0),X1) = iPr_def_13(X0,rd(X2,X1)),
inference(demodulation,[status(thm)],[c_556,c_637]) ).
tcf(c_659,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,rd(X0,X0),X1) = iPr_def_13(X0,rd(X2,X1)),
inference(demodulation,[status(thm)],[c_658,c_227]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(X0,X0),X0,X1) = iPr_def_13(X0,rd(X2,X1)),
inference(demodulation,[status(thm)],[c_516,c_637]) ).
tcf(c_666,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,ld(X0,X1),X2) = mult(ld(X0,X1),X2),
inference(demodulation,[status(thm)],[c_439,c_274]) ).
tcf(c_695,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(ld(X0,X1),mult(rd(ld(ld(X0,X1),X2),X3),X3)) = rd(iPr_def_11(X0,X2,rd(X4,X3)),rd(X4,X3)),
inference(demodulation,[status(thm)],[c_447,c_60]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : rd(iPr_def_11(X0,X1,rd(X2,X3)),rd(X2,X3)) = iPr_def_14(X0,X1,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_695]) ).
tcf(c_713,plain,
! [X0: $i] : mult(mult(rd(X0,X0),rd(rd(X0,X0),rd(X0,X0))),X0) = iPr_def_12(rd(X0,X0),X0),
inference(demodulation,[status(thm)],[c_596,c_634]) ).
tcf(c_714,plain,
! [X0: $i] : iPr_def_12(rd(X0,X0),X0) = X0,
inference(demodulation,[status(thm)],[c_713,c_80,c_274]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,iPr_def_13(X1,X2),rd(X3,X3)) = iPr_def_13(iPr_def_10(X0,X1,X2),X3),
inference(demodulation,[status(thm)],[c_460,c_418,c_637]) ).
tcf(c_764,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : rd(mult(iPr_def_10(X0,X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X0,rd(mult(iPr_def_13(X1,X2),X4),X4)),
inference(demodulation,[status(thm)],[c_419,c_637]) ).
tcf(c_765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(rd(iPr_def_10(X0,X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X0,mult(rd(iPr_def_13(X1,X2),X4),X4)),
inference(demodulation,[status(thm)],[c_764,c_60]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),rd(mult(ld(ld(X0,X1),X2),X3),X3)) = iPr_def_14(X0,X2,X3),
inference(demodulation,[status(thm)],[c_615,c_622,c_696]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),mult(rd(ld(ld(X0,X1),X2),X3),X3)) = iPr_def_14(X0,X2,X3),
inference(demodulation,[status(thm)],[c_769,c_60]) ).
tcf(c_787,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(ld(X0,X1),rd(mult(ld(ld(X0,X1),mult(X2,X3)),X4),X4)) = iPr_def_14(X0,mult(X2,X3),X4),
inference(demodulation,[status(thm)],[c_583,c_588,c_696]) ).
tcf(c_788,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(ld(X0,X1),mult(rd(ld(ld(X0,X1),mult(X2,X3)),X4),X4)) = iPr_def_14(X0,mult(X2,X3),X4),
inference(demodulation,[status(thm)],[c_787,c_60]) ).
tcf(c_789,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(mult(X0,ld(X0,X1)),X2,rd(X3,X4)) = iPr_def_14(X0,mult(X1,X2),X4),
inference(demodulation,[status(thm)],[c_582,c_651,c_788]) ).
tcf(c_790,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,mult(X1,ld(X1,X1)),X2) = iPr_def_12(X0,iPr_def_13(X1,X2)),
inference(demodulation,[status(thm)],[c_575,c_418,c_634,c_637,c_789]) ).
tcf(c_791,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_13(X1,X2)) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_790,c_227,c_274]) ).
tcf(c_796,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(mult(ld(X0,mult(X0,X1)),X2),ld(mult(ld(X0,mult(X0,X1)),X2),mult(X3,X4))) = mult(iPr_def_12(X0,X3),X4),
inference(demodulation,[status(thm)],[c_564,c_634]) ).
tcf(c_797,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_12(X0,X1),X2) = iPr_def_11(X0,X1,X2),
inference(demodulation,[status(thm)],[c_796,c_59,c_133]) ).
tcf(c_813,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : rd(mult(iPr_def_10(X0,ld(X0,X0),rd(X1,X1)),rd(X2,X3)),rd(X2,X3)) = mult(rd(X0,rd(X4,X1)),rd(mult(rd(X4,X1),X3),X3)),
inference(demodulation,[status(thm)],[c_538,c_418]) ).
tcf(c_814,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : mult(rd(iPr_def_10(X0,rd(X0,X0),rd(X1,X1)),rd(X2,X3)),rd(X2,X3)) = mult(rd(X0,rd(X4,X1)),mult(rd(rd(X4,X1),X3),X3)),
inference(demodulation,[status(thm)],[c_813,c_60,c_227]) ).
tcf(c_815,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(X0,rd(X1,X2)),mult(rd(rd(X1,X2),X3),X3)) = iPr_def_16(X0,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_814]) ).
tcf(c_816,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(iPr_def_10(X0,rd(X0,X0),rd(X1,X1)),rd(X2,X3)),rd(X2,X3)) = iPr_def_16(X0,X1,X3),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_814]) ).
tcf(c_817,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(rd(X0,rd(X1,X2)),rd(X1,X2),rd(X3,X3)) = iPr_def_16(X0,X2,X3),
inference(demodulation,[status(thm)],[c_815,c_418]) ).
tcf(c_818,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(iPr_def_13(X0,X1),X2) = iPr_def_16(X0,X1,X2),
inference(demodulation,[status(thm)],[c_816,c_418,c_641,c_757,c_765]) ).
tcf(c_900,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(X1,X2)) = iPr_def_10(rd(X0,X0),X0,rd(X2,X2)),
inference(demodulation,[status(thm)],[c_118,c_418]) ).
tcf(c_901,plain,
! [X0: $i,X1: $i] : iPr_def_10(rd(X0,X0),X0,rd(X1,X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_900,c_637]) ).
tcf(c_1615,plain,
! [X0: $i,X1: $i] : iPr_def_11(rd(X0,X0),X0,X1) = mult(X0,X1),
inference(superposition,[status(thm)],[c_714,c_797]) ).
tcf(c_1650,plain,
! [X0: $i] : mult(rd(X0,X0),ld(rd(X0,X0),X0)) = X0,
inference(superposition,[status(thm)],[c_227,c_624]) ).
tcf(c_1651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(ld(X0,X1),rd(mult(ld(ld(X0,X1),X0),X2),X2)) = rd(mult(X0,rd(X3,X2)),rd(X3,X2)),
inference(superposition,[status(thm)],[c_624,c_62]) ).
tcf(c_1667,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,X0,X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_1651,c_60,c_637,c_770]) ).
tcf(c_1673,plain,
! [X0: $i] : ld(rd(X0,X0),X0) = X0,
inference(demodulation,[status(thm)],[c_86,c_1650]) ).
tcf(c_1710,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(rd(X0,X0),mult(rd(X0,X0),X1)),X2) = ld(X0,mult(X0,mult(X1,X2))),
inference(superposition,[status(thm)],[c_1673,c_61]) ).
tcf(c_1719,plain,
! [X0: $i,X1: $i] : mult(mult(rd(X0,X1),X1),X1) = iPr_def_10(X0,X1,X1),
inference(superposition,[status(thm)],[c_60,c_651]) ).
tcf(c_1728,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,rd(X0,X0),X1) = mult(rd(X0,X1),X1),
inference(superposition,[status(thm)],[c_274,c_651]) ).
tcf(c_1745,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,rd(X1,X1),X1) = iPr_def_12(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_227,c_656]) ).
tcf(c_1746,plain,
! [X0: $i,X1: $i] : iPr_def_11(rd(X0,X0),rd(X1,X1),X1) = iPr_def_12(X0,X1),
inference(superposition,[status(thm)],[c_1673,c_656]) ).
tcf(c_1747,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(ld(X0,X1),X2) = iPr_def_12(ld(X0,X3),X2),
inference(superposition,[status(thm)],[c_656,c_656]) ).
tcf(c_1778,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X0),X0) = iPr_def_13(X0,rd(X1,X0)),
inference(superposition,[status(thm)],[c_662,c_623]) ).
tcf(c_1787,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,rd(X0,X0),X1) = mult(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_227,c_666]) ).
tcf(c_1810,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,rd(X1,rd(X2,X2))) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_901,c_662]) ).
tcf(c_1812,plain,
! [X0: $i] : iPr_def_12(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_624,c_634]) ).
tcf(c_1815,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,rd(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_1778,c_80]) ).
tcf(c_1819,plain,
! [X0: $i,X1: $i] : mult(mult(rd(X0,X1),X1),X1) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_1719,c_623]) ).
tcf(c_1840,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,ld(X0,mult(X1,X2))) = iPr_def_11(X0,X1,X2),
inference(demodulation,[status(thm)],[c_1710,c_59,c_442]) ).
tcf(c_1913,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X1),rd(ld(X0,X1),ld(X0,X1))) = iPr_def_12(X0,ld(X0,X1)),
inference(superposition,[status(thm)],[c_227,c_634]) ).
tcf(c_1917,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = iPr_def_12(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_1673,c_634]) ).
tcf(c_3101,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,X0,X1) = mult(X0,X1),
inference(superposition,[status(thm)],[c_1812,c_797]) ).
tcf(c_3106,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,mult(rd(X1,X0),X0)) = X0,
inference(superposition,[status(thm)],[c_60,c_1815]) ).
tcf(c_3170,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(ld(X0,X1),ld(X0,X2)) = ld(X0,X2),
inference(superposition,[status(thm)],[c_1747,c_1812]) ).
tcf(c_3225,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,mult(rd(X1,rd(X2,X2)),rd(X2,X2))) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_60,c_1810]) ).
tcf(c_3239,plain,
! [X0: $i,X1: $i] : mult(mult(X0,ld(X0,ld(X1,X1))),X1) = mult(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_116,c_1819]) ).
tcf(c_3240,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_10(X0,X1,X2),X2) = mult(mult(X0,X1),X2),
inference(superposition,[status(thm)],[c_651,c_1819]) ).
tcf(c_3251,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,rd(X1,X2)),rd(mult(rd(X1,X2),X2),X2)) = rd(mult(X0,rd(X1,X2)),rd(X1,X2)),
inference(superposition,[status(thm)],[c_1819,c_62]) ).
tcf(c_3284,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X1),X1) = iPr_def_13(X0,rd(X2,X1)),
inference(superposition,[status(thm)],[c_1728,c_659]) ).
tcf(c_3321,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(ld(X0,X1),X2) = iPr_def_12(rd(X0,X0),X2),
inference(superposition,[status(thm)],[c_1745,c_656]) ).
tcf(c_3327,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(rd(X0,X0),rd(X0,X0)),X1) = iPr_def_12(X0,X1),
inference(superposition,[status(thm)],[c_1746,c_1745]) ).
tcf(c_3328,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(ld(rd(X0,X0),X1),X2) = iPr_def_12(X0,X2),
inference(superposition,[status(thm)],[c_1746,c_656]) ).
tcf(c_3335,plain,
! [X0: $i] : mult(rd(rd(X0,X0),rd(X0,X0)),rd(X0,X0)) = iPr_def_12(X0,rd(X0,X0)),
inference(superposition,[status(thm)],[c_1787,c_1746]) ).
tcf(c_3338,plain,
! [X0: $i,X1: $i] : mult(X0,mult(X0,ld(X0,X1))) = iPr_def_11(X0,X0,X1),
inference(superposition,[status(thm)],[c_59,c_1840]) ).
tcf(c_3365,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(ld(X0,X1),X2,X3) = iPr_def_12(X0,mult(X2,X3)),
inference(superposition,[status(thm)],[c_1840,c_634]) ).
tcf(c_3370,plain,
! [X0: $i,X1: $i] : mult(X0,iPr_def_12(rd(X0,X0),X1)) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_3338,c_1917,c_3101]) ).
tcf(c_3389,plain,
! [X0: $i,X1: $i] : mult(iPr_def_12(rd(X0,X0),ld(X1,X1)),X1) = mult(rd(X0,X0),X1),
inference(demodulation,[status(thm)],[c_3239,c_1917]) ).
tcf(c_3390,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X0),X1) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_3389,c_227,c_797,c_1746]) ).
tcf(c_3392,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,iPr_def_13(X1,X2)) = iPr_def_13(X0,X2),
inference(demodulation,[status(thm)],[c_3225,c_637]) ).
tcf(c_3408,plain,
! [X0: $i] : iPr_def_12(rd(X0,X0),rd(X0,X0)) = iPr_def_12(X0,rd(X0,X0)),
inference(demodulation,[status(thm)],[c_3335,c_3390]) ).
tcf(c_3409,plain,
! [X0: $i] : iPr_def_12(X0,rd(X0,X0)) = rd(X0,X0),
inference(demodulation,[status(thm)],[c_3408,c_1812]) ).
tcf(c_3422,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,ld(X0,X1)) = ld(X0,X1),
inference(demodulation,[status(thm)],[c_1913,c_274]) ).
tcf(c_3466,plain,
! [X0: $i,X1: $i] : iPr_def_16(X0,X1,X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_3251,c_60,c_418,c_637,c_817]) ).
tcf(c_3483,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = iPr_def_12(rd(X0,X0),X1),
inference(demodulation,[status(thm)],[c_59,c_1917]) ).
tcf(c_3488,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(rd(ld(X0,X1),ld(X0,X1)),X2) = iPr_def_12(X0,X2),
inference(demodulation,[status(thm)],[c_634,c_1917]) ).
tcf(c_3489,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ld(ld(X0,X1),mult(ld(X0,X1),mult(X2,X3))) = mult(iPr_def_12(rd(X0,X0),X2),X3),
inference(demodulation,[status(thm)],[c_61,c_3483]) ).
tcf(c_3490,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_12(rd(X0,X0),X1),X2) = iPr_def_12(X0,mult(X1,X2)),
inference(demodulation,[status(thm)],[c_3489,c_3483,c_3488]) ).
tcf(c_3491,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(rd(X0,X0),X1,X2) = iPr_def_12(X0,mult(X1,X2)),
inference(demodulation,[status(thm)],[c_3490,c_797]) ).
tcf(c_3492,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,mult(X0,X1)) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_1615,c_3491]) ).
tcf(c_3777,plain,
! [X0: $i,X1: $i] : iPr_def_13(rd(X0,X1),X1) = rd(X0,X1),
inference(superposition,[status(thm)],[c_490,c_3106]) ).
tcf(c_3778,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,mult(mult(rd(X1,X0),X0),X0)) = X0,
inference(superposition,[status(thm)],[c_60,c_3106]) ).
tcf(c_3793,plain,
! [X0: $i,X1: $i] : mult(rd(rd(X0,X0),X1),X1) = rd(iPr_def_12(X0,X1),X1),
inference(superposition,[status(thm)],[c_3390,c_60]) ).
tcf(c_3808,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,rd(X1,X2)) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_1815,c_3392]) ).
tcf(c_3811,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,mult(rd(X1,X2),X2)) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_3106,c_3392]) ).
tcf(c_3946,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(rd(X0,X0),rd(X0,X0)),X1) = iPr_def_12(X0,ld(rd(X0,X0),X1)),
inference(superposition,[status(thm)],[c_1917,c_3390]) ).
tcf(c_3952,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,ld(rd(X0,X0),X1)) = ld(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_1673,c_3170]) ).
tcf(c_3986,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_13(mult(X0,X1),rd(X2,X3)) = iPr_def_10(X0,X1,X3),
inference(superposition,[status(thm)],[c_651,c_3284]) ).
tcf(c_4002,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,mult(rd(X1,X2),X2)) = mult(rd(X0,X2),X2),
inference(superposition,[status(thm)],[c_60,c_3284]) ).
tcf(c_4005,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(rd(X0,X1),iPr_def_13(X0,rd(X2,X1))) = iPr_def_13(X0,rd(X2,X1)),
inference(superposition,[status(thm)],[c_3284,c_3492]) ).
tcf(c_4009,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(rd(iPr_def_13(X0,rd(X1,X2)),X3),X3) = iPr_def_10(rd(X0,X2),X2,X3),
inference(superposition,[status(thm)],[c_3284,c_651]) ).
tcf(c_4011,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(rd(X0,X1),X1),X1) = rd(iPr_def_13(X0,rd(X2,X1)),X1),
inference(superposition,[status(thm)],[c_3284,c_60]) ).
tcf(c_4015,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_13(X0,rd(X1,X2)),X2) = mult(X0,X2),
inference(superposition,[status(thm)],[c_3284,c_1819]) ).
tcf(c_4017,plain,
! [X0: $i] : mult(iPr_def_13(x3,rd(X0,x4)),x5) != mult(x3,x5),
inference(superposition,[status(thm)],[c_3284,c_81]) ).
tcf(c_4019,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_13(mult(X0,X1),rd(X2,X3)) = iPr_def_10(X0,X1,X3),
inference(superposition,[status(thm)],[c_3284,c_651]) ).
tcf(c_4038,plain,
! [X0: $i,X1: $i] : mult(iPr_def_13(X0,X1),X1) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_4015,c_3808]) ).
tcf(c_4040,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,mult(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_3778,c_1819]) ).
tcf(c_4042,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(mult(X0,X1),X2) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_4019,c_3808]) ).
tcf(c_4043,plain,
mult(iPr_def_13(x3,x4),x5) != mult(x3,x5),
inference(demodulation,[status(thm)],[c_4017,c_3808]) ).
tcf(c_4044,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,X1,rd(X2,X3)) = iPr_def_10(X0,X1,X3),
inference(demodulation,[status(thm)],[c_3986,c_4042]) ).
tcf(c_4049,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_4002,c_3811]) ).
tcf(c_4060,plain,
! [X0: $i,X1: $i] : rd(iPr_def_12(X0,X1),X1) = iPr_def_13(rd(X0,X0),X1),
inference(demodulation,[status(thm)],[c_3793,c_4049]) ).
tcf(c_4082,plain,
! [X0: $i,X1: $i] : rd(iPr_def_13(X0,X1),X1) = rd(X0,X1),
inference(demodulation,[status(thm)],[c_4011,c_3777,c_3808,c_4049]) ).
tcf(c_4083,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(X0,X1),iPr_def_13(X0,X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_4005,c_3808]) ).
tcf(c_4084,plain,
! [X0: $i,X1: $i] : iPr_def_14(rd(X0,X1),X0,X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_4083,c_791]) ).
tcf(c_4096,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(X0,X1),X1,X2) = iPr_def_13(iPr_def_13(X0,X1),X2),
inference(demodulation,[status(thm)],[c_4009,c_3808,c_4049]) ).
tcf(c_4097,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(X0,X1),X1,X2) = iPr_def_16(X0,X1,X2),
inference(demodulation,[status(thm)],[c_4096,c_818]) ).
tcf(c_4111,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(rd(X0,X0),rd(X0,X0)),X1) = ld(rd(X0,X0),X1),
inference(demodulation,[status(thm)],[c_3946,c_3952]) ).
tcf(c_4112,plain,
! [X0: $i,X1: $i] : ld(rd(X0,X0),X1) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_4111,c_3327]) ).
tcf(c_4145,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,rd(X0,X0),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_641,c_4044]) ).
tcf(c_4161,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_60,c_4049]) ).
tcf(c_4165,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : rd(mult(mult(X0,X1),rd(X2,X3)),rd(X2,X3)) = mult(X0,iPr_def_13(X1,X3)),
inference(demodulation,[status(thm)],[c_62,c_4161]) ).
tcf(c_4166,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,iPr_def_13(X1,X2)) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_4165,c_4044,c_4042,c_4161]) ).
tcf(c_4772,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,iPr_def_12(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_3390,c_4040]) ).
tcf(c_4777,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_16(X0,mult(X1,X0),X2) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_4040,c_818]) ).
tcf(c_4778,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,mult(X1,X2)) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_4040,c_3392]) ).
tcf(c_4815,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_13(X0,X1),iPr_def_13(X2,X1)) = mult(X0,iPr_def_13(X2,X1)),
inference(superposition,[status(thm)],[c_3392,c_4038]) ).
tcf(c_4850,plain,
! [X0: $i] : rd(rd(X0,X0),rd(X0,X0)) = iPr_def_12(X0,rd(X0,X0)),
inference(superposition,[status(thm)],[c_4112,c_227]) ).
tcf(c_4857,plain,
! [X0: $i,X1: $i,X2: $i] : rd(iPr_def_11(X0,X1,X2),X2) = iPr_def_13(iPr_def_12(X0,X1),X2),
inference(superposition,[status(thm)],[c_797,c_4161]) ).
tcf(c_4893,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_13(X0,X1),X1,X2) = iPr_def_13(mult(X0,X1),X2),
inference(superposition,[status(thm)],[c_4038,c_4042]) ).
tcf(c_4945,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(X0,X0),X1,X2) = iPr_def_12(X0,iPr_def_13(X1,X2)),
inference(superposition,[status(thm)],[c_4166,c_3390]) ).
tcf(c_4960,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(rd(rd(X0,X0),rd(X0,X0)),X1) = iPr_def_12(iPr_def_12(X0,X2),X1),
inference(superposition,[status(thm)],[c_4112,c_3321]) ).
tcf(c_5003,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_12(X0,X1),X2) = iPr_def_12(X0,X2),
inference(superposition,[status(thm)],[c_4112,c_3328]) ).
tcf(c_5034,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(X0,X0),X1,X2) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_4945,c_791]) ).
tcf(c_5037,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_13(X0,X1),X1,X2) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_4893,c_4042]) ).
tcf(c_5054,plain,
! [X0: $i] : rd(rd(X0,X0),rd(X0,X0)) = rd(X0,X0),
inference(demodulation,[status(thm)],[c_4850,c_3409]) ).
tcf(c_5057,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_13(X0,X1),X2,X1) = iPr_def_10(X0,X2,X1),
inference(demodulation,[status(thm)],[c_4815,c_4166]) ).
tcf(c_5079,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(X0,X0),X1) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_4960,c_5003,c_5054]) ).
tcf(c_5105,plain,
! [X0: $i,X1: $i] : mult(X0,iPr_def_12(X0,X1)) = mult(X0,X1),
inference(demodulation,[status(thm)],[c_3370,c_5079]) ).
tcf(c_5106,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_1917,c_5079]) ).
tcf(c_5108,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(ld(X0,X1),X2) = iPr_def_12(X0,X2),
inference(demodulation,[status(thm)],[c_3321,c_5079]) ).
tcf(c_5194,plain,
! [X0: $i,X1: $i] : iPr_def_13(ld(X0,X1),ld(X0,X1)) = ld(X0,X1),
inference(superposition,[status(thm)],[c_3422,c_4772]) ).
tcf(c_5223,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,iPr_def_12(X1,X2)) = iPr_def_13(X0,X2),
inference(superposition,[status(thm)],[c_3390,c_4778]) ).
tcf(c_5232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_16(X0,mult(X1,X2),X3) = iPr_def_13(iPr_def_13(X0,X2),X3),
inference(superposition,[status(thm)],[c_4778,c_818]) ).
tcf(c_5260,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_14(X0,X1,X2),X3) = iPr_def_12(X0,X3),
inference(superposition,[status(thm)],[c_791,c_5003]) ).
tcf(c_5319,plain,
! [X0: $i,X1: $i] : rd(iPr_def_12(X0,X1),ld(X0,X1)) = iPr_def_13(X0,ld(X0,X1)),
inference(superposition,[status(thm)],[c_5106,c_4161]) ).
tcf(c_5324,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,ld(X1,X2)) = iPr_def_13(X0,iPr_def_12(X1,X2)),
inference(superposition,[status(thm)],[c_5106,c_4778]) ).
tcf(c_5338,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(ld(X0,X1),X2,X3) = mult(iPr_def_12(X0,X2),X3),
inference(superposition,[status(thm)],[c_5108,c_797]) ).
tcf(c_5355,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_16(iPr_def_12(X0,X1),mult(X0,X1),X2) = iPr_def_13(iPr_def_12(X0,X1),X2),
inference(superposition,[status(thm)],[c_5105,c_4777]) ).
tcf(c_5455,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(X0,ld(X1,X2)) = iPr_def_13(X0,X2),
inference(demodulation,[status(thm)],[c_5324,c_5223]) ).
tcf(c_5457,plain,
! [X0: $i,X1: $i] : iPr_def_13(ld(X0,X1),X1) = ld(X0,X1),
inference(demodulation,[status(thm)],[c_5194,c_5455]) ).
tcf(c_5459,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,mult(X1,X2)) = iPr_def_11(X0,X1,X2),
inference(demodulation,[status(thm)],[c_5338,c_797,c_3365]) ).
tcf(c_5470,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_16(X0,mult(X1,X2),X3) = iPr_def_16(X0,X2,X3),
inference(demodulation,[status(thm)],[c_5232,c_818]) ).
tcf(c_5488,plain,
! [X0: $i,X1: $i] : rd(iPr_def_12(X0,X1),ld(X0,X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_5319,c_5455]) ).
tcf(c_5505,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_16(iPr_def_12(X0,X1),X1,X2) = iPr_def_13(iPr_def_12(X0,X1),X2),
inference(demodulation,[status(thm)],[c_5355,c_5470]) ).
tcf(c_6129,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_12(X0,X1),X1) = iPr_def_12(X0,X1),
inference(superposition,[status(thm)],[c_4112,c_5457]) ).
tcf(c_6213,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_13(X0,X1),X2) = iPr_def_12(X0,X2),
inference(superposition,[status(thm)],[c_1667,c_5260]) ).
tcf(c_6215,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(rd(X0,X1),X2) = iPr_def_12(iPr_def_13(X0,X1),X2),
inference(superposition,[status(thm)],[c_4084,c_5260]) ).
tcf(c_6293,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,rd(X1,X2),X2) = iPr_def_12(X0,iPr_def_13(X1,X2)),
inference(superposition,[status(thm)],[c_4049,c_5459]) ).
tcf(c_6340,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(rd(X0,X1),X2) = iPr_def_12(X0,X2),
inference(demodulation,[status(thm)],[c_6215,c_6213]) ).
tcf(c_6347,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,rd(X1,X2),X2) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_6293,c_791]) ).
tcf(c_6508,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(iPr_def_12(X0,rd(X1,X2)),X2) = iPr_def_12(X0,rd(X1,X2)),
inference(superposition,[status(thm)],[c_6129,c_3808]) ).
tcf(c_6737,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(iPr_def_12(X1,X2),X2)) = iPr_def_10(X0,rd(X1,X1),X2),
inference(superposition,[status(thm)],[c_4060,c_4166]) ).
tcf(c_7463,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(rd(iPr_def_12(X0,X1),X1),X1,X2) = iPr_def_10(rd(X0,X0),X1,X2),
inference(superposition,[status(thm)],[c_4060,c_5037]) ).
tcf(c_7520,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,rd(iPr_def_13(X0,X1),iPr_def_13(X0,X1)),X1) = iPr_def_13(iPr_def_13(X0,X1),X1),
inference(superposition,[status(thm)],[c_5057,c_4145]) ).
tcf(c_7581,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(iPr_def_12(X0,X1),X2) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_7463,c_4097,c_5034,c_5505]) ).
tcf(c_7587,plain,
! [X0: $i,X1: $i] : mult(X0,rd(iPr_def_12(X0,X1),X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7520,c_818,c_3466,c_6213,c_6737]) ).
tcf(c_7666,plain,
! [X0: $i,X1: $i,X2: $i] : rd(iPr_def_14(X0,X1,X2),X2) = rd(iPr_def_12(X0,X1),X2),
inference(superposition,[status(thm)],[c_7581,c_4082]) ).
tcf(c_9802,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(iPr_def_12(X0,rd(X1,X2)),X2) = rd(iPr_def_14(X0,X1,X2),X2),
inference(superposition,[status(thm)],[c_6347,c_4857]) ).
tcf(c_10060,plain,
! [X0: $i,X1: $i,X2: $i] : rd(iPr_def_12(X0,X1),X2) = iPr_def_12(X0,rd(X1,X2)),
inference(demodulation,[status(thm)],[c_9802,c_6508,c_7666]) ).
tcf(c_10080,plain,
! [X0: $i,X1: $i] : mult(X0,iPr_def_12(X0,rd(X1,X1))) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7587,c_10060]) ).
tcf(c_10082,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,rd(X1,ld(X0,X1))) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_5488,c_10060]) ).
tcf(c_10083,plain,
! [X0: $i,X1: $i] : mult(X0,rd(X1,X1)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_10080,c_5105]) ).
tcf(c_10555,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,iPr_def_12(X1,rd(X2,iPr_def_12(X1,X2)))) = iPr_def_13(X0,iPr_def_12(X1,X2)),
inference(superposition,[status(thm)],[c_10060,c_10083]) ).
tcf(c_10692,plain,
! [X0: $i,X1: $i] : iPr_def_12(rd(X0,X0),rd(X1,iPr_def_12(X0,X1))) = iPr_def_13(rd(X0,X0),X1),
inference(superposition,[status(thm)],[c_4112,c_10082]) ).
tcf(c_10800,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,rd(X1,iPr_def_12(X0,X1))) = iPr_def_13(rd(X0,X0),X1),
inference(demodulation,[status(thm)],[c_10692,c_6340]) ).
tcf(c_10826,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,iPr_def_13(rd(X1,X1),X2)) = iPr_def_13(X0,iPr_def_12(X1,X2)),
inference(demodulation,[status(thm)],[c_10555,c_10800]) ).
tcf(c_10827,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,rd(X1,X1),X2) = iPr_def_13(X0,X2),
inference(demodulation,[status(thm)],[c_10826,c_4166,c_5223]) ).
tcf(c_11411,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,rd(X1,X1)),X2) = mult(iPr_def_13(X0,X2),X2),
inference(superposition,[status(thm)],[c_10827,c_3240]) ).
tcf(c_11582,plain,
! [X0: $i,X1: $i,X2: $i] : mult(iPr_def_13(X0,X1),X2) = mult(X0,X2),
inference(demodulation,[status(thm)],[c_11411,c_4038,c_10083]) ).
tcf(c_11714,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_4043,c_11582]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP683-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Wed Sep 23 15:47:20 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.41 Running UEQ theorem proving
% 0.12/0.41 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.12/0.42
% 0.12/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.42
% 0.12/0.42 % Detected problem language: tptp
% 0.12/0.44 % Proving...
% 9.19/2.27 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 9.19/2.27 % SZS status Started for theBenchmark.p
% 9.19/2.27 % SZS status Unsatisfiable for theBenchmark.p
% 9.19/2.27
% 9.19/2.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.19/2.27
% 9.19/2.27 % ------ iProver source info
% 9.19/2.27
% 9.19/2.27 % git: date: 2026-07-19 20:42:38 +0200
% 9.19/2.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.19/2.27 % git: non_committed_changes: false
% 9.19/2.27
% 9.19/2.27 % ------ Parsing...% successful
% 9.19/2.27
% 9.19/2.27
% 9.19/2.27 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 9.19/2.27 % ------ Proving...
% 9.19/2.27 % ------ Problem Properties
% 9.19/2.27
% 9.19/2.27 %
% 9.19/2.27 % clauses 8
% 9.19/2.27 % conjectures 1
% 9.19/2.27 % EPR 0
% 9.19/2.27 % Horn 8
% 9.19/2.27 % unary 8
% 9.19/2.27 % binary 0
% 9.19/2.27 % lits 8
% 9.19/2.27 % lits eq 8
% 9.19/2.27 % fd_pure 0
% 9.19/2.27 % fd_pseudo 0
% 9.19/2.27 % fd_cond 0
% 9.19/2.27 % fd_pseudo_cond 0
% 9.19/2.27 % AC symbols 0
% 9.19/2.27
% 9.19/2.27 % ------ Input Options Time Limit: Unbounded
% 9.19/2.27
% 9.19/2.27
% 9.19/2.27 % ------
% 9.19/2.27 % Current options:
% 9.19/2.27 % ------
% 9.19/2.27
% 9.19/2.27
% 9.19/2.27 %
% 9.19/2.27
% 9.19/2.27 % ------ Proving...
% 9.19/2.27 %
% 9.19/2.27
% 9.19/2.27 % SZS status Unsatisfiable for theBenchmark.p
% 9.19/2.27
% 9.19/2.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.19/2.27
% 9.19/2.27
%------------------------------------------------------------------------------