%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP688-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 : n014.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:13 PM UTC 2026
% Result : Unsatisfiable 45.18s 7.26s
% Output : CNFRefutation 45.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 19
% Syntax : Number of formulae : 292 ( 292 unt; 7 def)
% Number of atoms : 868 ( 291 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 8 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 209 ( 0 sgn 209 !; 0 ?; 192 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X0,X2))) = mult(mult(X0,mult(X1,X0)),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,axiom,
! [X0,X1] : i(mult(X0,X1)) = mult(i(X0),i(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
fof(f10,axiom,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f11,plain,
unit = mult(op_c,mult(op_c,mult(op_c,op_c))),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
mult(op_d,mult(op_d,op_d)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
fof(f13,plain,
unit = mult(op_d,mult(op_d,op_d)),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
mult(op_c,op_d) != mult(op_d,op_c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = X1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_65,plain,
! [X0: $i] : mult(X0,unit) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_66,plain,
! [X0: $i] : mult(unit,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,mult(X1,X0)),X2) = mult(X0,mult(X1,mult(X0,X2))),
inference(cnf_transformation,[],[f7]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] : mult(i(X0),mult(X0,X1)) = X1,
inference(cnf_transformation,[],[f8]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] : mult(i(X0),i(X1)) = i(mult(X0,X1)),
inference(cnf_transformation,[],[f9]) ).
tcf(c_70,plain,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
inference(cnf_transformation,[],[f11]) ).
tcf(c_71,plain,
mult(op_d,mult(op_d,op_d)) = unit,
inference(cnf_transformation,[],[f13]) ).
tcf(c_72,negated_conjecture,
mult(op_c,op_d) != mult(op_d,op_c),
inference(cnf_transformation,[],[f14]) ).
tcf(c_112,definition,
iPr_def_10 = mult(op_c,op_d),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_113,definition,
iPr_def_11 = mult(op_d,op_c),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_114,definition,
iPr_def_12 = mult(op_d,op_d),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_115,definition,
iPr_def_13 = mult(op_d,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_116,definition,
iPr_def_14 = mult(op_c,op_c),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_117,definition,
iPr_def_15 = mult(op_c,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_118,definition,
iPr_def_16 = mult(op_c,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_119,negated_conjecture,
iPr_def_10 != iPr_def_11,
inference(demodulation,[status(thm)],[c_72,c_113,c_112]) ).
tcf(c_120,plain,
iPr_def_13 = unit,
inference(demodulation,[status(thm)],[c_71,c_114,c_115]) ).
tcf(c_121,plain,
iPr_def_16 = unit,
inference(demodulation,[status(thm)],[c_70,c_116,c_117,c_118]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : mult(i(X0),i(X1)) = i(mult(X0,X1)),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] : mult(i(X0),mult(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,mult(X1,X0)),X2) = mult(X0,mult(X1,mult(X0,X2))),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_125,plain,
! [X0: $i] : mult(unit,X0) = X0,
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_126,plain,
! [X0: $i] : mult(X0,unit) = X0,
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_207,plain,
iPr_def_13 = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_121,c_120]) ).
tcf(c_209,plain,
mult(op_c,iPr_def_15) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_118,c_207]) ).
tcf(c_211,plain,
! [X0: $i] : mult(iPr_def_13,X0) = X0,
inference(light_normalisation,[status(thm)],[c_125,c_120]) ).
tcf(c_213,plain,
! [X0: $i] : mult(X0,iPr_def_13) = X0,
inference(light_normalisation,[status(thm)],[c_126,c_120]) ).
tcf(c_223,plain,
rd(iPr_def_14,op_c) = op_c,
inference(superposition,[status(thm)],[c_116,c_127]) ).
tcf(c_224,plain,
rd(iPr_def_12,op_d) = op_d,
inference(superposition,[status(thm)],[c_114,c_127]) ).
tcf(c_225,plain,
rd(iPr_def_10,op_d) = op_c,
inference(superposition,[status(thm)],[c_112,c_127]) ).
tcf(c_226,plain,
rd(iPr_def_11,op_c) = op_d,
inference(superposition,[status(thm)],[c_113,c_127]) ).
tcf(c_227,plain,
rd(iPr_def_13,iPr_def_12) = op_d,
inference(superposition,[status(thm)],[c_115,c_127]) ).
tcf(c_228,plain,
rd(iPr_def_15,iPr_def_14) = op_c,
inference(superposition,[status(thm)],[c_117,c_127]) ).
tcf(c_229,plain,
rd(iPr_def_13,iPr_def_15) = op_c,
inference(superposition,[status(thm)],[c_209,c_127]) ).
tcf(c_250,plain,
mult(op_c,op_c) = iPr_def_14,
inference(superposition,[status(thm)],[c_223,c_128]) ).
tcf(c_251,plain,
mult(op_d,op_d) = iPr_def_12,
inference(superposition,[status(thm)],[c_224,c_128]) ).
tcf(c_252,plain,
mult(op_c,op_d) = iPr_def_10,
inference(superposition,[status(thm)],[c_225,c_128]) ).
tcf(c_253,plain,
mult(op_d,op_c) = iPr_def_11,
inference(superposition,[status(thm)],[c_226,c_128]) ).
tcf(c_254,plain,
mult(op_d,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_227,c_128]) ).
tcf(c_255,plain,
mult(op_c,iPr_def_14) = iPr_def_15,
inference(superposition,[status(thm)],[c_228,c_128]) ).
tcf(c_332,plain,
! [X0: $i,X1: $i] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_130,c_127]) ).
tcf(c_409,plain,
! [X0: $i,X1: $i] : mult(i(X0),X1) = ld(X0,X1),
inference(superposition,[status(thm)],[c_130,c_123]) ).
tcf(c_410,plain,
! [X0: $i,X1: $i] : mult(i(rd(X0,X1)),X0) = X1,
inference(superposition,[status(thm)],[c_128,c_123]) ).
tcf(c_412,plain,
mult(i(op_c),iPr_def_14) = op_c,
inference(superposition,[status(thm)],[c_250,c_123]) ).
tcf(c_414,plain,
mult(i(op_d),iPr_def_12) = op_d,
inference(superposition,[status(thm)],[c_251,c_123]) ).
tcf(c_416,plain,
mult(i(op_c),iPr_def_10) = op_d,
inference(superposition,[status(thm)],[c_252,c_123]) ).
tcf(c_418,plain,
mult(i(op_d),iPr_def_11) = op_c,
inference(superposition,[status(thm)],[c_253,c_123]) ).
tcf(c_420,plain,
mult(i(op_d),iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_254,c_123]) ).
tcf(c_422,plain,
mult(i(op_c),iPr_def_15) = iPr_def_14,
inference(superposition,[status(thm)],[c_255,c_123]) ).
tcf(c_424,plain,
mult(i(op_c),iPr_def_13) = iPr_def_15,
inference(superposition,[status(thm)],[c_209,c_123]) ).
tcf(c_426,plain,
! [X0: $i] : mult(i(X0),X0) = iPr_def_13,
inference(superposition,[status(thm)],[c_213,c_123]) ).
tcf(c_428,plain,
! [X0: $i,X1: $i] : ld(i(X0),X1) = mult(X0,X1),
inference(superposition,[status(thm)],[c_123,c_129]) ).
tcf(c_429,plain,
! [X0: $i,X1: $i] : rd(X0,mult(X1,X0)) = i(X1),
inference(superposition,[status(thm)],[c_123,c_127]) ).
tcf(c_430,plain,
i(op_c) = iPr_def_15,
inference(demodulation,[status(thm)],[c_424,c_213]) ).
tcf(c_431,plain,
mult(iPr_def_15,iPr_def_15) = iPr_def_14,
inference(demodulation,[status(thm)],[c_422,c_430]) ).
tcf(c_432,plain,
i(op_d) = iPr_def_12,
inference(demodulation,[status(thm)],[c_420,c_213]) ).
tcf(c_433,plain,
mult(iPr_def_12,iPr_def_11) = op_c,
inference(demodulation,[status(thm)],[c_418,c_432]) ).
tcf(c_434,plain,
mult(iPr_def_15,iPr_def_10) = op_d,
inference(demodulation,[status(thm)],[c_416,c_430]) ).
tcf(c_435,plain,
mult(iPr_def_12,iPr_def_12) = op_d,
inference(demodulation,[status(thm)],[c_414,c_432]) ).
tcf(c_436,plain,
mult(iPr_def_15,iPr_def_14) = op_c,
inference(demodulation,[status(thm)],[c_412,c_430]) ).
tcf(c_530,plain,
mult(iPr_def_15,op_c) = iPr_def_13,
inference(superposition,[status(thm)],[c_430,c_426]) ).
tcf(c_531,plain,
mult(iPr_def_12,op_d) = iPr_def_13,
inference(superposition,[status(thm)],[c_432,c_426]) ).
tcf(c_534,plain,
! [X0: $i] : rd(iPr_def_13,X0) = i(X0),
inference(superposition,[status(thm)],[c_426,c_127]) ).
tcf(c_536,plain,
i(iPr_def_12) = op_d,
inference(demodulation,[status(thm)],[c_227,c_534]) ).
tcf(c_537,plain,
i(iPr_def_15) = op_c,
inference(demodulation,[status(thm)],[c_229,c_534]) ).
tcf(c_574,plain,
! [X0: $i] : i(ld(X0,iPr_def_13)) = X0,
inference(superposition,[status(thm)],[c_534,c_332]) ).
tcf(c_625,plain,
! [X0: $i] : ld(op_c,X0) = mult(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_430,c_409]) ).
tcf(c_626,plain,
! [X0: $i] : ld(op_d,X0) = mult(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_432,c_409]) ).
tcf(c_628,plain,
! [X0: $i] : ld(iPr_def_12,X0) = mult(op_d,X0),
inference(superposition,[status(thm)],[c_536,c_409]) ).
tcf(c_629,plain,
! [X0: $i] : ld(iPr_def_15,X0) = mult(op_c,X0),
inference(superposition,[status(thm)],[c_537,c_409]) ).
tcf(c_634,plain,
! [X0: $i] : ld(X0,iPr_def_13) = i(X0),
inference(superposition,[status(thm)],[c_409,c_213]) ).
tcf(c_636,plain,
! [X0: $i] : i(i(X0)) = X0,
inference(demodulation,[status(thm)],[c_574,c_634]) ).
tcf(c_674,plain,
! [X0: $i] : mult(X0,i(X0)) = iPr_def_13,
inference(superposition,[status(thm)],[c_634,c_130]) ).
tcf(c_716,plain,
! [X0: $i] : mult(op_c,mult(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_625,c_130]) ).
tcf(c_733,plain,
! [X0: $i] : mult(op_d,mult(iPr_def_12,X0)) = X0,
inference(superposition,[status(thm)],[c_626,c_130]) ).
tcf(c_898,plain,
! [X0: $i,X1: $i] : i(rd(X0,X1)) = rd(X1,X0),
inference(superposition,[status(thm)],[c_410,c_127]) ).
tcf(c_1073,plain,
! [X0: $i,X1: $i,X2: $i] : ld(rd(X0,X1),X2) = mult(rd(X1,X0),X2),
inference(superposition,[status(thm)],[c_898,c_409]) ).
tcf(c_1182,plain,
! [X0: $i] : mult(iPr_def_15,i(X0)) = i(mult(op_c,X0)),
inference(superposition,[status(thm)],[c_430,c_122]) ).
tcf(c_1183,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X1),i(X2)) = i(mult(rd(X1,X0),X2)),
inference(superposition,[status(thm)],[c_898,c_122]) ).
tcf(c_1185,plain,
! [X0: $i] : mult(iPr_def_12,i(X0)) = i(mult(op_d,X0)),
inference(superposition,[status(thm)],[c_432,c_122]) ).
tcf(c_1187,plain,
! [X0: $i] : mult(op_d,i(X0)) = i(mult(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_536,c_122]) ).
tcf(c_1189,plain,
! [X0: $i] : mult(i(X0),iPr_def_15) = i(mult(X0,op_c)),
inference(superposition,[status(thm)],[c_430,c_122]) ).
tcf(c_1191,plain,
! [X0: $i,X1: $i] : i(mult(X0,i(X1))) = mult(i(X0),X1),
inference(superposition,[status(thm)],[c_636,c_122]) ).
tcf(c_1192,plain,
! [X0: $i] : mult(i(X0),iPr_def_12) = i(mult(X0,op_d)),
inference(superposition,[status(thm)],[c_432,c_122]) ).
tcf(c_1194,plain,
! [X0: $i] : mult(i(X0),op_d) = i(mult(X0,iPr_def_12)),
inference(superposition,[status(thm)],[c_536,c_122]) ).
tcf(c_1195,plain,
! [X0: $i] : mult(i(X0),op_c) = i(mult(X0,iPr_def_15)),
inference(superposition,[status(thm)],[c_537,c_122]) ).
tcf(c_1197,plain,
! [X0: $i,X1: $i] : rd(i(mult(X0,X1)),i(X1)) = i(X0),
inference(superposition,[status(thm)],[c_122,c_127]) ).
tcf(c_1199,plain,
! [X0: $i,X1: $i] : ld(X0,i(X1)) = i(mult(X0,X1)),
inference(superposition,[status(thm)],[c_122,c_409]) ).
tcf(c_1201,plain,
! [X0: $i] : i(mult(X0,iPr_def_15)) = ld(X0,op_c),
inference(demodulation,[status(thm)],[c_1195,c_409]) ).
tcf(c_1202,plain,
! [X0: $i] : i(mult(X0,iPr_def_12)) = ld(X0,op_d),
inference(demodulation,[status(thm)],[c_1194,c_409]) ).
tcf(c_1203,plain,
! [X0: $i] : i(mult(X0,op_d)) = ld(X0,iPr_def_12),
inference(demodulation,[status(thm)],[c_1192,c_409]) ).
tcf(c_1204,plain,
! [X0: $i] : i(mult(X0,op_c)) = ld(X0,iPr_def_15),
inference(demodulation,[status(thm)],[c_1189,c_409]) ).
tcf(c_1206,plain,
! [X0: $i,X1: $i] : i(mult(X0,i(X1))) = ld(X0,X1),
inference(demodulation,[status(thm)],[c_1191,c_409]) ).
tcf(c_1225,plain,
! [X0: $i] : ld(rd(X0,iPr_def_15),op_c) = i(X0),
inference(superposition,[status(thm)],[c_128,c_1201]) ).
tcf(c_1229,plain,
ld(iPr_def_15,op_c) = i(iPr_def_14),
inference(superposition,[status(thm)],[c_431,c_1201]) ).
tcf(c_1231,plain,
! [X0: $i,X1: $i] : ld(ld(X0,op_c),X1) = mult(mult(X0,iPr_def_15),X1),
inference(superposition,[status(thm)],[c_1201,c_428]) ).
tcf(c_1236,plain,
i(iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_1229,c_250,c_629]) ).
tcf(c_1237,plain,
! [X0: $i] : mult(rd(iPr_def_15,X0),op_c) = i(X0),
inference(demodulation,[status(thm)],[c_1225,c_1073]) ).
tcf(c_1245,plain,
! [X0: $i] : mult(iPr_def_14,i(X0)) = i(mult(iPr_def_14,X0)),
inference(superposition,[status(thm)],[c_1236,c_122]) ).
tcf(c_1247,plain,
mult(iPr_def_14,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_1236,c_674]) ).
tcf(c_1248,plain,
! [X0: $i] : ld(iPr_def_14,X0) = mult(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_1236,c_409]) ).
tcf(c_1249,plain,
! [X0: $i] : mult(i(X0),iPr_def_14) = i(mult(X0,iPr_def_14)),
inference(superposition,[status(thm)],[c_1236,c_122]) ).
tcf(c_1250,plain,
! [X0: $i] : i(mult(X0,iPr_def_14)) = ld(X0,iPr_def_14),
inference(demodulation,[status(thm)],[c_1249,c_409]) ).
tcf(c_1271,plain,
! [X0: $i] : mult(iPr_def_14,mult(iPr_def_14,X0)) = X0,
inference(superposition,[status(thm)],[c_1248,c_130]) ).
tcf(c_1306,plain,
! [X0: $i] : ld(rd(X0,iPr_def_12),op_d) = i(X0),
inference(superposition,[status(thm)],[c_128,c_1202]) ).
tcf(c_1318,plain,
! [X0: $i] : mult(rd(iPr_def_12,X0),op_d) = i(X0),
inference(demodulation,[status(thm)],[c_1306,c_1073]) ).
tcf(c_1338,plain,
! [X0: $i] : ld(rd(X0,op_d),iPr_def_12) = i(X0),
inference(superposition,[status(thm)],[c_128,c_1203]) ).
tcf(c_1341,plain,
ld(op_c,iPr_def_12) = i(iPr_def_10),
inference(superposition,[status(thm)],[c_252,c_1203]) ).
tcf(c_1347,plain,
! [X0: $i,X1: $i] : ld(ld(X0,iPr_def_12),X1) = mult(mult(X0,op_d),X1),
inference(superposition,[status(thm)],[c_1203,c_428]) ).
tcf(c_1350,plain,
! [X0: $i,X1: $i] : ld(mult(X0,op_d),X1) = mult(ld(X0,iPr_def_12),X1),
inference(superposition,[status(thm)],[c_1203,c_409]) ).
tcf(c_1352,plain,
mult(iPr_def_15,iPr_def_12) = i(iPr_def_10),
inference(demodulation,[status(thm)],[c_1341,c_625]) ).
tcf(c_1353,plain,
! [X0: $i] : mult(rd(op_d,X0),iPr_def_12) = i(X0),
inference(demodulation,[status(thm)],[c_1338,c_1073]) ).
tcf(c_1365,plain,
mult(op_c,i(iPr_def_10)) = iPr_def_12,
inference(superposition,[status(thm)],[c_1352,c_716]) ).
tcf(c_1414,plain,
ld(op_d,iPr_def_15) = i(iPr_def_11),
inference(superposition,[status(thm)],[c_253,c_1204]) ).
tcf(c_1423,plain,
! [X0: $i,X1: $i] : ld(mult(X0,op_c),X1) = mult(ld(X0,iPr_def_15),X1),
inference(superposition,[status(thm)],[c_1204,c_409]) ).
tcf(c_1425,plain,
mult(iPr_def_12,iPr_def_15) = i(iPr_def_11),
inference(demodulation,[status(thm)],[c_1414,c_626]) ).
tcf(c_1489,plain,
! [X0: $i] : rd(i(X0),op_c) = rd(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1237,c_127]) ).
tcf(c_1583,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(rd(X1,X0),mult(X0,X2))) = mult(mult(X0,X1),X2),
inference(superposition,[status(thm)],[c_128,c_124]) ).
tcf(c_1592,plain,
! [X0: $i] : mult(op_c,mult(op_d,mult(op_c,X0))) = mult(mult(op_c,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_253,c_124]) ).
tcf(c_1599,plain,
! [X0: $i,X1: $i] : mult(X0,mult(iPr_def_13,mult(X0,X1))) = mult(mult(X0,X0),X1),
inference(superposition,[status(thm)],[c_211,c_124]) ).
tcf(c_1605,plain,
! [X0: $i] : mult(iPr_def_12,mult(iPr_def_12,mult(iPr_def_12,X0))) = mult(mult(iPr_def_12,op_d),X0),
inference(superposition,[status(thm)],[c_435,c_124]) ).
tcf(c_1624,plain,
! [X0: $i,X1: $i,X2: $i] : rd(mult(X0,mult(X1,mult(X0,X2))),X2) = mult(X0,mult(X1,X0)),
inference(superposition,[status(thm)],[c_124,c_127]) ).
tcf(c_1626,plain,
! [X0: $i,X1: $i,X2: $i] : rd(X0,mult(X1,mult(X2,mult(X1,X0)))) = i(mult(X1,mult(X2,X1))),
inference(superposition,[status(thm)],[c_124,c_429]) ).
tcf(c_1634,plain,
! [X0: $i] : mult(iPr_def_12,mult(iPr_def_12,mult(iPr_def_12,X0))) = X0,
inference(demodulation,[status(thm)],[c_1605,c_211,c_531]) ).
tcf(c_1636,plain,
! [X0: $i,X1: $i] : mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)),
inference(demodulation,[status(thm)],[c_1599,c_211]) ).
tcf(c_1755,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),i(X0)) = i(X1),
inference(superposition,[status(thm)],[c_128,c_1183]) ).
tcf(c_2043,plain,
! [X0: $i,X1: $i] : rd(i(X0),i(X1)) = i(rd(X0,X1)),
inference(superposition,[status(thm)],[c_128,c_1197]) ).
tcf(c_2104,plain,
! [X0: $i,X1: $i] : rd(i(X0),i(X1)) = rd(X1,X0),
inference(demodulation,[status(thm)],[c_2043,c_898]) ).
tcf(c_2178,plain,
! [X0: $i,X1: $i] : mult(X0,i(mult(X0,X1))) = i(X1),
inference(superposition,[status(thm)],[c_1199,c_130]) ).
tcf(c_2222,plain,
! [X0: $i] : ld(rd(X0,iPr_def_14),iPr_def_14) = i(X0),
inference(superposition,[status(thm)],[c_128,c_1250]) ).
tcf(c_2232,plain,
! [X0: $i] : mult(mult(X0,iPr_def_14),ld(X0,iPr_def_14)) = iPr_def_13,
inference(superposition,[status(thm)],[c_1250,c_674]) ).
tcf(c_2234,plain,
! [X0: $i,X1: $i] : ld(mult(X0,iPr_def_14),X1) = mult(ld(X0,iPr_def_14),X1),
inference(superposition,[status(thm)],[c_1250,c_409]) ).
tcf(c_2242,plain,
! [X0: $i] : mult(rd(iPr_def_14,X0),iPr_def_14) = i(X0),
inference(demodulation,[status(thm)],[c_2222,c_1073]) ).
tcf(c_2270,plain,
! [X0: $i] : rd(i(X0),op_d) = rd(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_1318,c_127]) ).
tcf(c_2273,plain,
! [X0: $i] : rd(op_d,i(X0)) = i(rd(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_1318,c_429]) ).
tcf(c_2276,plain,
! [X0: $i] : rd(op_d,i(X0)) = rd(X0,iPr_def_12),
inference(demodulation,[status(thm)],[c_2273,c_898]) ).
tcf(c_2308,plain,
! [X0: $i] : rd(iPr_def_12,i(X0)) = i(rd(op_d,X0)),
inference(superposition,[status(thm)],[c_1353,c_429]) ).
tcf(c_2311,plain,
! [X0: $i] : rd(iPr_def_12,i(X0)) = rd(X0,op_d),
inference(demodulation,[status(thm)],[c_2308,c_898]) ).
tcf(c_3801,plain,
rd(iPr_def_12,iPr_def_14) = rd(iPr_def_14,op_d),
inference(superposition,[status(thm)],[c_1236,c_2270]) ).
tcf(c_3874,plain,
i(rd(iPr_def_12,iPr_def_14)) = rd(op_d,iPr_def_14),
inference(superposition,[status(thm)],[c_3801,c_898]) ).
tcf(c_3879,plain,
rd(op_d,iPr_def_14) = rd(iPr_def_14,iPr_def_12),
inference(demodulation,[status(thm)],[c_3874,c_898]) ).
tcf(c_3902,plain,
! [X0: $i] : rd(mult(X0,op_d),iPr_def_12) = rd(op_d,ld(X0,iPr_def_12)),
inference(superposition,[status(thm)],[c_1203,c_2276]) ).
tcf(c_4052,plain,
! [X0: $i] : rd(mult(X0,iPr_def_14),op_d) = rd(iPr_def_12,ld(X0,iPr_def_14)),
inference(superposition,[status(thm)],[c_1250,c_2311]) ).
tcf(c_4382,plain,
! [X0: $i,X1: $i] : ld(rd(X0,i(X1)),X1) = i(X0),
inference(superposition,[status(thm)],[c_128,c_1206]) ).
tcf(c_4434,plain,
! [X0: $i,X1: $i] : mult(rd(i(X0),X1),X0) = i(X1),
inference(demodulation,[status(thm)],[c_4382,c_1073]) ).
tcf(c_4942,plain,
mult(iPr_def_12,mult(iPr_def_12,op_c)) = iPr_def_11,
inference(superposition,[status(thm)],[c_433,c_1634]) ).
tcf(c_4954,plain,
! [X0: $i] : mult(iPr_def_12,mult(iPr_def_12,X0)) = mult(op_d,X0),
inference(superposition,[status(thm)],[c_1634,c_733]) ).
tcf(c_5005,plain,
mult(op_d,iPr_def_11) = mult(iPr_def_12,op_c),
inference(superposition,[status(thm)],[c_4942,c_733]) ).
tcf(c_5346,plain,
! [X0: $i,X1: $i] : rd(X0,i(X1)) = rd(X1,i(X0)),
inference(superposition,[status(thm)],[c_636,c_2104]) ).
tcf(c_5524,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X1),i(i(mult(rd(X1,X0),X2)))) = i(i(X2)),
inference(superposition,[status(thm)],[c_2178,c_1183]) ).
tcf(c_5528,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X1),mult(rd(X1,X0),X2)) = X2,
inference(demodulation,[status(thm)],[c_5524,c_636]) ).
tcf(c_5576,plain,
mult(mult(op_d,iPr_def_14),mult(iPr_def_12,iPr_def_14)) = iPr_def_13,
inference(superposition,[status(thm)],[c_626,c_2232]) ).
tcf(c_5577,plain,
mult(mult(iPr_def_12,iPr_def_14),mult(op_d,iPr_def_14)) = iPr_def_13,
inference(superposition,[status(thm)],[c_628,c_2232]) ).
tcf(c_5960,plain,
! [X0: $i] : rd(mult(op_d,X0),mult(iPr_def_12,X0)) = iPr_def_12,
inference(superposition,[status(thm)],[c_4954,c_127]) ).
tcf(c_5962,plain,
! [X0: $i] : rd(mult(iPr_def_12,X0),mult(op_d,X0)) = i(iPr_def_12),
inference(superposition,[status(thm)],[c_4954,c_429]) ).
tcf(c_5967,plain,
! [X0: $i] : rd(mult(iPr_def_12,X0),mult(op_d,X0)) = op_d,
inference(demodulation,[status(thm)],[c_5962,c_536]) ).
tcf(c_7791,plain,
! [X0: $i] : ld(mult(op_c,op_c),X0) = mult(mult(iPr_def_15,iPr_def_15),X0),
inference(superposition,[status(thm)],[c_629,c_1231]) ).
tcf(c_7816,plain,
! [X0: $i] : mult(iPr_def_15,mult(iPr_def_15,X0)) = mult(iPr_def_14,X0),
inference(demodulation,[status(thm)],[c_7791,c_431,c_625,c_1423,c_1636]) ).
tcf(c_8004,plain,
mult(iPr_def_14,iPr_def_15) = mult(iPr_def_15,iPr_def_14),
inference(superposition,[status(thm)],[c_431,c_7816]) ).
tcf(c_8005,plain,
mult(iPr_def_14,iPr_def_10) = mult(iPr_def_15,op_d),
inference(superposition,[status(thm)],[c_434,c_7816]) ).
tcf(c_8007,plain,
mult(iPr_def_14,op_c) = mult(iPr_def_15,iPr_def_13),
inference(superposition,[status(thm)],[c_530,c_7816]) ).
tcf(c_8022,plain,
! [X0: $i] : mult(op_c,mult(iPr_def_14,X0)) = mult(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_7816,c_716]) ).
tcf(c_8023,plain,
mult(iPr_def_14,op_c) = iPr_def_15,
inference(demodulation,[status(thm)],[c_8007,c_213]) ).
tcf(c_8024,plain,
mult(iPr_def_14,iPr_def_15) = op_c,
inference(demodulation,[status(thm)],[c_8004,c_436]) ).
tcf(c_10626,plain,
! [X0: $i,X1: $i] : mult(ld(X0,iPr_def_12),mult(mult(X0,op_d),X1)) = X1,
inference(superposition,[status(thm)],[c_1347,c_130]) ).
tcf(c_11084,plain,
! [X0: $i,X1: $i] : rd(mult(X0,mult(X0,X1)),X1) = mult(X0,X0),
inference(superposition,[status(thm)],[c_1636,c_127]) ).
tcf(c_16101,plain,
! [X0: $i] : rd(mult(X0,iPr_def_13),i(X0)) = mult(X0,X0),
inference(superposition,[status(thm)],[c_674,c_11084]) ).
tcf(c_16161,plain,
rd(mult(mult(op_d,iPr_def_14),iPr_def_13),mult(iPr_def_12,iPr_def_14)) = mult(mult(op_d,iPr_def_14),mult(op_d,iPr_def_14)),
inference(superposition,[status(thm)],[c_5576,c_11084]) ).
tcf(c_16162,plain,
rd(mult(mult(iPr_def_12,iPr_def_14),iPr_def_13),mult(op_d,iPr_def_14)) = mult(mult(iPr_def_12,iPr_def_14),mult(iPr_def_12,iPr_def_14)),
inference(superposition,[status(thm)],[c_5577,c_11084]) ).
tcf(c_16195,plain,
! [X0: $i] : rd(X0,i(X0)) = mult(X0,X0),
inference(demodulation,[status(thm)],[c_16101,c_213,c_5346]) ).
tcf(c_16209,plain,
mult(mult(iPr_def_12,iPr_def_14),mult(iPr_def_12,iPr_def_14)) = op_d,
inference(demodulation,[status(thm)],[c_16162,c_213,c_5967]) ).
tcf(c_16210,plain,
mult(mult(op_d,iPr_def_14),mult(op_d,iPr_def_14)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_16161,c_213,c_5960]) ).
tcf(c_16813,plain,
rd(mult(mult(iPr_def_12,iPr_def_14),op_d),mult(iPr_def_12,iPr_def_14)) = op_d,
inference(superposition,[status(thm)],[c_16209,c_11084]) ).
tcf(c_16815,plain,
mult(mult(iPr_def_12,iPr_def_14),i(op_d)) = i(mult(iPr_def_12,iPr_def_14)),
inference(superposition,[status(thm)],[c_16209,c_2178]) ).
tcf(c_16817,plain,
rd(op_d,mult(iPr_def_12,iPr_def_14)) = mult(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_16209,c_127]) ).
tcf(c_16819,plain,
rd(mult(iPr_def_12,iPr_def_14),op_d) = i(mult(iPr_def_12,iPr_def_14)),
inference(superposition,[status(thm)],[c_16209,c_429]) ).
tcf(c_16823,plain,
rd(iPr_def_12,mult(op_d,iPr_def_14)) = mult(op_d,iPr_def_14),
inference(demodulation,[status(thm)],[c_16819,c_628,c_1187,c_1236,c_4052]) ).
tcf(c_16824,plain,
mult(mult(iPr_def_12,iPr_def_14),iPr_def_12) = mult(op_d,iPr_def_14),
inference(demodulation,[status(thm)],[c_16815,c_432,c_1187,c_1236]) ).
tcf(c_16908,plain,
! [X0: $i] : mult(mult(op_d,iPr_def_14),mult(mult(op_d,iPr_def_14),mult(mult(op_d,iPr_def_14),X0))) = mult(mult(mult(op_d,iPr_def_14),iPr_def_12),X0),
inference(superposition,[status(thm)],[c_16210,c_124]) ).
tcf(c_16911,plain,
! [X0: $i] : mult(mult(op_d,iPr_def_14),mult(mult(op_d,iPr_def_14),X0)) = mult(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_16210,c_1636]) ).
tcf(c_16914,plain,
! [X0: $i] : mult(mult(mult(op_d,iPr_def_14),iPr_def_12),X0) = mult(iPr_def_12,mult(mult(op_d,iPr_def_14),X0)),
inference(demodulation,[status(thm)],[c_16908,c_16911]) ).
tcf(c_17097,plain,
! [X0: $i] : mult(mult(iPr_def_12,iPr_def_14),mult(rd(mult(iPr_def_12,iPr_def_14),op_d),X0)) = X0,
inference(superposition,[status(thm)],[c_16817,c_5528]) ).
tcf(c_17114,plain,
! [X0: $i] : mult(mult(iPr_def_12,iPr_def_14),mult(mult(op_d,iPr_def_14),X0)) = X0,
inference(demodulation,[status(thm)],[c_17097,c_628,c_4052,c_16823]) ).
tcf(c_18262,plain,
mult(mult(iPr_def_12,iPr_def_14),op_d) = mult(op_d,mult(iPr_def_12,iPr_def_14)),
inference(superposition,[status(thm)],[c_16813,c_128]) ).
tcf(c_18267,plain,
mult(mult(iPr_def_12,iPr_def_14),op_d) = iPr_def_14,
inference(demodulation,[status(thm)],[c_18262,c_733]) ).
tcf(c_18285,plain,
mult(mult(iPr_def_12,iPr_def_14),i(iPr_def_14)) = i(op_d),
inference(superposition,[status(thm)],[c_18267,c_2178]) ).
tcf(c_18287,plain,
mult(iPr_def_12,iPr_def_14) = rd(iPr_def_14,op_d),
inference(superposition,[status(thm)],[c_18267,c_127]) ).
tcf(c_18289,plain,
i(mult(iPr_def_12,iPr_def_14)) = rd(op_d,iPr_def_14),
inference(superposition,[status(thm)],[c_18267,c_429]) ).
tcf(c_18291,plain,
! [X0: $i] : mult(ld(mult(iPr_def_12,iPr_def_14),iPr_def_12),mult(iPr_def_14,X0)) = X0,
inference(superposition,[status(thm)],[c_18267,c_10626]) ).
tcf(c_18294,plain,
rd(op_d,ld(mult(iPr_def_12,iPr_def_14),iPr_def_12)) = rd(iPr_def_14,iPr_def_12),
inference(superposition,[status(thm)],[c_18267,c_3902]) ).
tcf(c_18296,plain,
! [X0: $i] : mult(ld(mult(iPr_def_12,iPr_def_14),iPr_def_12),X0) = ld(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_18267,c_1350]) ).
tcf(c_18300,plain,
ld(mult(iPr_def_12,iPr_def_14),iPr_def_12) = i(iPr_def_14),
inference(superposition,[status(thm)],[c_18267,c_1203]) ).
tcf(c_18305,plain,
mult(mult(op_d,iPr_def_14),iPr_def_12) = iPr_def_14,
inference(demodulation,[status(thm)],[c_18300,c_628,c_1236,c_2234]) ).
tcf(c_18306,plain,
mult(op_d,iPr_def_14) = rd(iPr_def_14,iPr_def_12),
inference(demodulation,[status(thm)],[c_18289,c_1187,c_1236,c_3879]) ).
tcf(c_18309,plain,
mult(mult(iPr_def_12,iPr_def_14),iPr_def_14) = iPr_def_12,
inference(demodulation,[status(thm)],[c_18285,c_432,c_1236]) ).
tcf(c_18310,plain,
! [X0: $i] : mult(iPr_def_12,mult(mult(op_d,iPr_def_14),X0)) = mult(iPr_def_14,X0),
inference(demodulation,[status(thm)],[c_18296,c_628,c_1248,c_2234,c_16914]) ).
tcf(c_18312,plain,
rd(op_d,ld(mult(iPr_def_12,iPr_def_14),iPr_def_12)) = mult(op_d,iPr_def_14),
inference(demodulation,[status(thm)],[c_18294,c_18306]) ).
tcf(c_18313,plain,
rd(op_d,mult(mult(op_d,iPr_def_14),iPr_def_12)) = mult(op_d,iPr_def_14),
inference(demodulation,[status(thm)],[c_18312,c_628,c_2234]) ).
tcf(c_18316,plain,
! [X0: $i] : mult(iPr_def_12,mult(mult(op_d,iPr_def_14),mult(iPr_def_14,X0))) = X0,
inference(demodulation,[status(thm)],[c_18291,c_628,c_2234,c_16914]) ).
tcf(c_18321,plain,
mult(iPr_def_12,iPr_def_14) = rd(iPr_def_12,iPr_def_14),
inference(demodulation,[status(thm)],[c_3801,c_18287]) ).
tcf(c_18772,plain,
! [X0: $i] : mult(iPr_def_12,mult(mult(op_d,iPr_def_14),mult(iPr_def_12,X0))) = mult(mult(iPr_def_12,iPr_def_14),X0),
inference(superposition,[status(thm)],[c_18305,c_124]) ).
tcf(c_18787,plain,
! [X0: $i] : mult(mult(iPr_def_12,iPr_def_14),X0) = mult(iPr_def_14,mult(iPr_def_12,X0)),
inference(demodulation,[status(thm)],[c_18772,c_18310]) ).
tcf(c_18789,plain,
mult(iPr_def_14,mult(iPr_def_12,iPr_def_12)) = mult(op_d,iPr_def_14),
inference(demodulation,[status(thm)],[c_16824,c_18787]) ).
tcf(c_18793,plain,
mult(op_d,iPr_def_14) = mult(iPr_def_14,op_d),
inference(demodulation,[status(thm)],[c_18789,c_435]) ).
tcf(c_20425,plain,
mult(mult(op_c,iPr_def_11),op_c) = mult(op_c,mult(op_d,iPr_def_14)),
inference(superposition,[status(thm)],[c_250,c_1592]) ).
tcf(c_20435,plain,
mult(mult(op_c,iPr_def_11),i(iPr_def_10)) = mult(op_c,mult(op_d,iPr_def_12)),
inference(superposition,[status(thm)],[c_1365,c_1592]) ).
tcf(c_20461,plain,
mult(mult(op_c,iPr_def_11),op_c) = mult(iPr_def_14,iPr_def_10),
inference(demodulation,[status(thm)],[c_20425,c_8005,c_8022,c_18793]) ).
tcf(c_20462,plain,
mult(mult(op_c,iPr_def_11),i(iPr_def_10)) = op_c,
inference(demodulation,[status(thm)],[c_20435,c_213,c_254]) ).
tcf(c_20748,plain,
mult(iPr_def_14,op_d) = rd(iPr_def_14,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_18306,c_18793]) ).
tcf(c_20755,plain,
! [X0: $i] : ld(mult(iPr_def_14,op_d),X0) = mult(rd(iPr_def_12,iPr_def_14),X0),
inference(superposition,[status(thm)],[c_20748,c_1073]) ).
tcf(c_20758,plain,
i(mult(iPr_def_14,op_d)) = rd(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_20748,c_898]) ).
tcf(c_20766,plain,
mult(iPr_def_12,iPr_def_14) = mult(iPr_def_14,iPr_def_12),
inference(demodulation,[status(thm)],[c_20758,c_432,c_1245,c_18321]) ).
tcf(c_20769,plain,
! [X0: $i] : mult(mult(iPr_def_14,iPr_def_12),X0) = mult(iPr_def_14,mult(iPr_def_12,X0)),
inference(demodulation,[status(thm)],[c_20755,c_1248,c_1350,c_18321,c_18787]) ).
tcf(c_20790,plain,
! [X0: $i] : mult(iPr_def_14,mult(mult(iPr_def_12,iPr_def_14),mult(iPr_def_14,X0))) = mult(mult(iPr_def_14,iPr_def_12),X0),
inference(superposition,[status(thm)],[c_18309,c_124]) ).
tcf(c_20802,plain,
! [X0: $i] : mult(iPr_def_12,mult(iPr_def_14,X0)) = mult(iPr_def_14,mult(iPr_def_12,X0)),
inference(demodulation,[status(thm)],[c_20790,c_1271,c_18787,c_20769]) ).
tcf(c_20969,plain,
! [X0: $i] : mult(mult(iPr_def_12,mult(iPr_def_12,iPr_def_14)),X0) = mult(iPr_def_12,mult(iPr_def_14,mult(iPr_def_12,X0))),
inference(superposition,[status(thm)],[c_20766,c_124]) ).
tcf(c_20985,plain,
mult(op_c,mult(iPr_def_12,iPr_def_14)) = mult(iPr_def_15,iPr_def_12),
inference(superposition,[status(thm)],[c_20766,c_8022]) ).
tcf(c_20990,plain,
mult(op_c,mult(iPr_def_12,iPr_def_14)) = i(iPr_def_10),
inference(demodulation,[status(thm)],[c_20985,c_1352]) ).
tcf(c_20991,plain,
! [X0: $i] : mult(mult(iPr_def_14,op_d),X0) = mult(op_d,mult(iPr_def_14,X0)),
inference(demodulation,[status(thm)],[c_20969,c_4954,c_18793,c_20802]) ).
tcf(c_21175,plain,
rd(i(iPr_def_10),op_c) = i(mult(op_c,iPr_def_11)),
inference(superposition,[status(thm)],[c_20462,c_429]) ).
tcf(c_21181,plain,
mult(iPr_def_15,i(iPr_def_11)) = rd(iPr_def_15,iPr_def_10),
inference(demodulation,[status(thm)],[c_21175,c_1182,c_1489]) ).
tcf(c_21501,plain,
mult(op_c,rd(iPr_def_15,iPr_def_10)) = i(iPr_def_11),
inference(superposition,[status(thm)],[c_21181,c_716]) ).
tcf(c_21812,plain,
rd(op_c,mult(iPr_def_14,iPr_def_10)) = i(mult(op_c,iPr_def_11)),
inference(superposition,[status(thm)],[c_20461,c_429]) ).
tcf(c_21826,plain,
rd(op_c,mult(iPr_def_14,iPr_def_10)) = rd(iPr_def_15,iPr_def_10),
inference(demodulation,[status(thm)],[c_21812,c_1182,c_21181]) ).
tcf(c_22374,plain,
! [X0: $i] : mult(mult(iPr_def_12,iPr_def_14),mult(op_d,mult(iPr_def_14,X0))) = X0,
inference(light_normalisation,[status(thm)],[c_17114,c_18793,c_20991]) ).
tcf(c_22397,plain,
! [X0: $i] : rd(X0,mult(op_d,mult(iPr_def_14,X0))) = mult(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_22374,c_127]) ).
tcf(c_22424,plain,
rd(op_d,mult(mult(iPr_def_14,op_d),iPr_def_12)) = mult(iPr_def_14,op_d),
inference(light_normalisation,[status(thm)],[c_18313,c_18793]) ).
tcf(c_22437,plain,
! [X0: $i] : mult(mult(mult(iPr_def_14,op_d),iPr_def_12),mult(mult(iPr_def_14,op_d),mult(mult(mult(iPr_def_14,op_d),iPr_def_12),X0))) = mult(mult(mult(mult(iPr_def_14,op_d),iPr_def_12),op_d),X0),
inference(superposition,[status(thm)],[c_22424,c_1583]) ).
tcf(c_22442,plain,
! [X0: $i] : mult(op_d,mult(iPr_def_14,X0)) = mult(iPr_def_14,mult(op_d,X0)),
inference(demodulation,[status(thm)],[c_22437,c_733,c_1271,c_20766,c_20991]) ).
tcf(c_22446,plain,
! [X0: $i] : mult(iPr_def_12,mult(mult(iPr_def_14,op_d),mult(iPr_def_14,X0))) = X0,
inference(light_normalisation,[status(thm)],[c_18316,c_18793]) ).
tcf(c_22455,plain,
mult(iPr_def_12,mult(mult(iPr_def_14,op_d),op_c)) = iPr_def_15,
inference(superposition,[status(thm)],[c_8024,c_22446]) ).
tcf(c_22478,plain,
mult(iPr_def_12,mult(iPr_def_14,iPr_def_11)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_22455,c_253,c_20991,c_22442]) ).
tcf(c_29180,plain,
! [X0: $i] : rd(X0,mult(iPr_def_14,mult(op_d,X0))) = mult(iPr_def_12,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_22397,c_22442]) ).
tcf(c_29199,plain,
rd(iPr_def_11,mult(iPr_def_14,mult(iPr_def_12,op_c))) = mult(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_5005,c_29180]) ).
tcf(c_29222,plain,
i(mult(iPr_def_14,mult(op_d,iPr_def_12))) = mult(mult(iPr_def_12,iPr_def_14),op_d),
inference(superposition,[status(thm)],[c_29180,c_1318]) ).
tcf(c_29225,plain,
i(mult(iPr_def_14,mult(op_d,iPr_def_14))) = mult(mult(iPr_def_12,iPr_def_14),iPr_def_14),
inference(superposition,[status(thm)],[c_29180,c_2242]) ).
tcf(c_29228,plain,
! [X0: $i] : i(mult(iPr_def_14,mult(op_d,i(X0)))) = mult(mult(iPr_def_12,iPr_def_14),X0),
inference(superposition,[status(thm)],[c_29180,c_4434]) ).
tcf(c_29229,plain,
mult(iPr_def_11,iPr_def_11) = mult(iPr_def_12,iPr_def_14),
inference(demodulation,[status(thm)],[c_29199,c_1425,c_8023,c_16195,c_20802]) ).
tcf(c_29237,plain,
i(mult(iPr_def_14,mult(op_d,iPr_def_14))) = mult(mult(iPr_def_11,iPr_def_11),iPr_def_14),
inference(demodulation,[status(thm)],[c_29225,c_29229]) ).
tcf(c_29238,plain,
mult(iPr_def_11,mult(iPr_def_11,iPr_def_14)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_29237,c_213,c_1185,c_1236,c_1245,c_1247,c_1636,c_20802]) ).
tcf(c_29243,plain,
i(mult(iPr_def_14,mult(op_d,iPr_def_12))) = mult(mult(iPr_def_11,iPr_def_11),op_d),
inference(demodulation,[status(thm)],[c_29222,c_29229]) ).
tcf(c_29244,plain,
mult(iPr_def_11,mult(iPr_def_11,op_d)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_29243,c_213,c_674,c_1185,c_1245,c_1636]) ).
tcf(c_29250,plain,
! [X0: $i] : i(mult(iPr_def_14,mult(op_d,i(X0)))) = mult(mult(iPr_def_11,iPr_def_11),X0),
inference(demodulation,[status(thm)],[c_29228,c_29229]) ).
tcf(c_29251,plain,
! [X0: $i] : mult(iPr_def_11,mult(iPr_def_11,X0)) = mult(iPr_def_12,mult(iPr_def_14,X0)),
inference(demodulation,[status(thm)],[c_29250,c_636,c_1185,c_1245,c_1636,c_20802]) ).
tcf(c_29291,plain,
mult(op_c,mult(iPr_def_11,iPr_def_11)) = i(iPr_def_10),
inference(demodulation,[status(thm)],[c_20990,c_29229]) ).
tcf(c_29301,plain,
mult(iPr_def_11,mult(iPr_def_11,iPr_def_11)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_22478,c_29251]) ).
tcf(c_29383,plain,
rd(mult(iPr_def_11,iPr_def_11),iPr_def_14) = iPr_def_12,
inference(superposition,[status(thm)],[c_29229,c_127]) ).
tcf(c_29403,plain,
i(mult(iPr_def_11,iPr_def_11)) = ld(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_29229,c_1250]) ).
tcf(c_29405,plain,
i(mult(iPr_def_11,iPr_def_11)) = mult(iPr_def_14,op_d),
inference(demodulation,[status(thm)],[c_29403,c_628,c_18793]) ).
tcf(c_29461,plain,
mult(iPr_def_11,i(iPr_def_12)) = i(mult(iPr_def_11,iPr_def_14)),
inference(superposition,[status(thm)],[c_29238,c_2178]) ).
tcf(c_29462,plain,
ld(iPr_def_11,iPr_def_12) = mult(iPr_def_11,iPr_def_14),
inference(superposition,[status(thm)],[c_29238,c_129]) ).
tcf(c_29470,plain,
ld(iPr_def_11,iPr_def_14) = mult(iPr_def_11,op_d),
inference(demodulation,[status(thm)],[c_29461,c_536,c_1250]) ).
tcf(c_29629,plain,
mult(iPr_def_11,i(iPr_def_15)) = i(mult(iPr_def_11,iPr_def_11)),
inference(superposition,[status(thm)],[c_29301,c_2178]) ).
tcf(c_29630,plain,
ld(iPr_def_11,iPr_def_15) = mult(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_29301,c_129]) ).
tcf(c_29638,plain,
mult(iPr_def_11,op_c) = mult(iPr_def_14,op_d),
inference(demodulation,[status(thm)],[c_29629,c_537,c_29405]) ).
tcf(c_29659,plain,
mult(iPr_def_12,i(mult(iPr_def_11,iPr_def_11))) = i(iPr_def_14),
inference(superposition,[status(thm)],[c_29383,c_1755]) ).
tcf(c_29668,plain,
mult(iPr_def_12,mult(iPr_def_11,op_c)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_29659,c_1236,c_29405,c_29638]) ).
tcf(c_31825,plain,
mult(iPr_def_11,mult(iPr_def_11,iPr_def_11)) = rd(mult(iPr_def_11,iPr_def_14),op_d),
inference(superposition,[status(thm)],[c_29244,c_1624]) ).
tcf(c_32006,plain,
rd(iPr_def_12,mult(iPr_def_11,op_d)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_31825,c_4052,c_29301,c_29470]) ).
tcf(c_34095,plain,
i(mult(iPr_def_11,mult(iPr_def_12,iPr_def_11))) = rd(op_c,mult(iPr_def_11,iPr_def_14)),
inference(superposition,[status(thm)],[c_29668,c_1626]) ).
tcf(c_34291,plain,
rd(op_c,mult(iPr_def_11,iPr_def_14)) = mult(iPr_def_11,iPr_def_11),
inference(demodulation,[status(thm)],[c_34095,c_433,c_1204,c_29630]) ).
tcf(c_54060,plain,
i(mult(iPr_def_11,op_d)) = mult(iPr_def_15,op_d),
inference(superposition,[status(thm)],[c_32006,c_1318]) ).
tcf(c_54061,plain,
mult(iPr_def_11,iPr_def_14) = mult(iPr_def_14,iPr_def_10),
inference(demodulation,[status(thm)],[c_54060,c_1203,c_8005,c_29462]) ).
tcf(c_54064,plain,
rd(op_c,mult(iPr_def_11,iPr_def_14)) = rd(iPr_def_15,iPr_def_10),
inference(demodulation,[status(thm)],[c_21826,c_54061]) ).
tcf(c_54109,plain,
mult(iPr_def_11,iPr_def_11) = rd(iPr_def_15,iPr_def_10),
inference(demodulation,[status(thm)],[c_54064,c_34291]) ).
tcf(c_54114,plain,
mult(op_c,mult(iPr_def_11,iPr_def_11)) = i(iPr_def_11),
inference(demodulation,[status(thm)],[c_21501,c_54109]) ).
tcf(c_54116,plain,
i(iPr_def_10) = i(iPr_def_11),
inference(demodulation,[status(thm)],[c_54114,c_29291]) ).
tcf(c_54161,plain,
i(i(iPr_def_10)) = iPr_def_11,
inference(superposition,[status(thm)],[c_54116,c_636]) ).
tcf(c_54172,plain,
iPr_def_10 = iPr_def_11,
inference(demodulation,[status(thm)],[c_54161,c_636]) ).
tcf(c_54173,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_54172,c_119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP688-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.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 15:42:48 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.38 Running UEQ theorem proving
% 0.13/0.38 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.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 45.18/7.26 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 45.18/7.26 % SZS status Started for theBenchmark.p
% 45.18/7.26 % SZS status Unsatisfiable for theBenchmark.p
% 45.18/7.26
% 45.18/7.26 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 45.18/7.26
% 45.18/7.26 % ------ iProver source info
% 45.18/7.26
% 45.18/7.26 % git: date: 2026-07-19 20:42:38 +0200
% 45.18/7.26 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 45.18/7.26 % git: non_committed_changes: false
% 45.18/7.26
% 45.18/7.26 % ------ Parsing...% successful
% 45.18/7.26
% 45.18/7.26
% 45.18/7.26 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 45.18/7.26
% 45.18/7.26 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 45.18/7.26
% 45.18/7.26 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 45.18/7.26
% 45.18/7.26 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 45.18/7.26 % ------ Proving...
% 45.18/7.26 % ------ Problem Properties
% 45.18/7.26
% 45.18/7.26 %
% 45.18/7.26 % clauses 19
% 45.18/7.26 % conjectures 1
% 45.18/7.26 % EPR 3
% 45.18/7.26 % Horn 19
% 45.18/7.26 % unary 19
% 45.18/7.26 % binary 0
% 45.18/7.26 % lits 19
% 45.18/7.26 % lits eq 19
% 45.18/7.26 % fd_pure 0
% 45.18/7.26 % fd_pseudo 0
% 45.18/7.26 % fd_cond 0
% 45.18/7.26 % fd_pseudo_cond 0
% 45.18/7.26 % AC symbols 0
% 45.18/7.26
% 45.18/7.26 % ------ Input Options Time Limit: Unbounded
% 45.18/7.26
% 45.18/7.26
% 45.18/7.26 % ------
% 45.18/7.26 % Current options:
% 45.18/7.26 % ------
% 45.18/7.26
% 45.18/7.26
% 45.18/7.26 %
% 45.18/7.26
% 45.18/7.26 % ------ Proving...
% 45.18/7.26 %
% 45.18/7.26
% 45.18/7.26 % SZS status Unsatisfiable for theBenchmark.p
% 45.18/7.26
% 45.18/7.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 45.18/7.26
% 45.18/7.26
%------------------------------------------------------------------------------