%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP705-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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:16 PM UTC 2026
% Result : Unsatisfiable 26.49s 4.32s
% Output : CNFRefutation 26.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 21
% Syntax : Number of formulae : 212 ( 212 unt; 12 def)
% Number of atoms : 611 ( 211 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 143 ( 0 sgn 143 !; 0 ?; 130 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X1,X2))) = mult(mult(mult(X0,X1),X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c07) ).
fof(f10,axiom,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c09) ).
fof(f11,plain,
unit = mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = X1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_63,plain,
! [X0: $i] : mult(X0,unit) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_64,plain,
! [X0: $i] : mult(unit,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(mult(X0,X1),X1),X2) = mult(X0,mult(X1,mult(X1,X2))),
inference(cnf_transformation,[],[f7]) ).
tcf(c_67,plain,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = unit,
inference(cnf_transformation,[],[f11]) ).
tcf(c_68,negated_conjecture,
mult(mult(op_a,op_b),a) != mult(op_a,mult(op_b,a)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_101,definition,
iPr_def_10 = mult(op_a,op_b),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_102,definition,
iPr_def_11 = mult(iPr_def_10,a),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_103,definition,
iPr_def_12 = mult(op_b,a),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_104,definition,
iPr_def_13 = mult(op_a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_105,definition,
iPr_def_14 = mult(op_b,op_b),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_106,definition,
iPr_def_15 = mult(op_b,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_107,definition,
iPr_def_16 = mult(op_b,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_108,definition,
iPr_def_17 = mult(op_b,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_109,definition,
iPr_def_18 = mult(op_b,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_110,definition,
iPr_def_19 = mult(op_b,iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_111,definition,
iPr_def_20 = mult(op_b,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_112,definition,
iPr_def_21 = mult(op_b,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_116,negated_conjecture,
iPr_def_11 != iPr_def_13,
inference(demodulation,[status(thm)],[c_68,c_103,c_104,c_101,c_102]) ).
tcf(c_117,plain,
iPr_def_21 = unit,
inference(demodulation,[status(thm)],[c_67,c_105,c_106,c_107,c_108,c_109,c_110,c_111,c_112]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(mult(X0,X1),X1),X2) = mult(X0,mult(X1,mult(X1,X2))),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_120,plain,
! [X0: $i] : mult(unit,X0) = X0,
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_121,plain,
! [X0: $i] : mult(X0,unit) = X0,
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_59]) ).
tcf(c_211,plain,
! [X0: $i] : mult(iPr_def_21,X0) = X0,
inference(light_normalisation,[status(thm)],[c_120,c_117]) ).
tcf(c_213,plain,
! [X0: $i] : mult(X0,iPr_def_21) = X0,
inference(light_normalisation,[status(thm)],[c_121,c_117]) ).
tcf(c_216,plain,
rd(iPr_def_14,op_b) = op_b,
inference(superposition,[status(thm)],[c_105,c_122]) ).
tcf(c_221,plain,
rd(iPr_def_15,iPr_def_14) = op_b,
inference(superposition,[status(thm)],[c_106,c_122]) ).
tcf(c_227,plain,
rd(iPr_def_21,iPr_def_20) = op_b,
inference(superposition,[status(thm)],[c_112,c_122]) ).
tcf(c_257,plain,
mult(op_b,op_b) = iPr_def_14,
inference(superposition,[status(thm)],[c_216,c_123]) ).
tcf(c_262,plain,
mult(op_b,iPr_def_14) = iPr_def_15,
inference(superposition,[status(thm)],[c_221,c_123]) ).
tcf(c_268,plain,
mult(op_b,iPr_def_20) = iPr_def_21,
inference(superposition,[status(thm)],[c_227,c_123]) ).
tcf(c_514,plain,
! [X0: $i,X1: $i,X2: $i] : mult(rd(X0,X1),mult(X1,mult(X1,X2))) = mult(mult(X0,X1),X2),
inference(superposition,[status(thm)],[c_123,c_119]) ).
tcf(c_518,plain,
! [X0: $i] : mult(op_b,mult(op_b,mult(op_b,X0))) = mult(mult(iPr_def_14,op_b),X0),
inference(superposition,[status(thm)],[c_257,c_119]) ).
tcf(c_545,plain,
! [X0: $i,X1: $i] : mult(iPr_def_21,mult(X0,mult(X0,X1))) = mult(mult(X0,X0),X1),
inference(superposition,[status(thm)],[c_211,c_119]) ).
tcf(c_552,plain,
! [X0: $i,X1: $i] : mult(X0,mult(X1,mult(X1,iPr_def_21))) = mult(mult(X0,X1),X1),
inference(superposition,[status(thm)],[c_119,c_213]) ).
tcf(c_553,plain,
! [X0: $i,X1: $i] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(demodulation,[status(thm)],[c_552,c_213]) ).
tcf(c_554,plain,
! [X0: $i,X1: $i] : mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)),
inference(demodulation,[status(thm)],[c_545,c_211]) ).
tcf(c_561,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,mult(X1,X1)),X2) = mult(X0,mult(X1,mult(X1,X2))),
inference(demodulation,[status(thm)],[c_119,c_553]) ).
tcf(c_622,plain,
mult(op_b,iPr_def_14) = mult(iPr_def_14,op_b),
inference(superposition,[status(thm)],[c_257,c_553]) ).
tcf(c_655,plain,
mult(iPr_def_14,op_b) = iPr_def_15,
inference(demodulation,[status(thm)],[c_622,c_262]) ).
tcf(c_1063,plain,
! [X0: $i] : mult(rd(X0,op_b),mult(op_b,iPr_def_21)) = mult(mult(X0,op_b),iPr_def_20),
inference(superposition,[status(thm)],[c_268,c_514]) ).
tcf(c_1090,plain,
! [X0: $i] : mult(mult(X0,op_b),iPr_def_20) = X0,
inference(demodulation,[status(thm)],[c_1063,c_123,c_213]) ).
tcf(c_1266,plain,
! [X0: $i] : mult(op_b,mult(op_b,mult(op_b,X0))) = mult(iPr_def_15,X0),
inference(light_normalisation,[status(thm)],[c_518,c_655]) ).
tcf(c_1268,plain,
! [X0: $i] : mult(op_b,mult(op_b,X0)) = mult(iPr_def_15,ld(op_b,X0)),
inference(superposition,[status(thm)],[c_125,c_1266]) ).
tcf(c_1831,plain,
! [X0: $i] : mult(X0,iPr_def_20) = rd(X0,op_b),
inference(superposition,[status(thm)],[c_123,c_1090]) ).
tcf(c_1843,plain,
! [X0: $i] : mult(X0,op_b) = rd(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_1090,c_122]) ).
tcf(c_1954,plain,
! [X0: $i] : mult(iPr_def_21,X0) = X0,
inference(light_normalisation,[status(thm)],[c_120,c_117]) ).
tcf(c_1955,plain,
! [X0: $i] : mult(X0,iPr_def_21) = X0,
inference(light_normalisation,[status(thm)],[c_121,c_117]) ).
tcf(c_1957,plain,
rd(iPr_def_14,op_b) = op_b,
inference(superposition,[status(thm)],[c_105,c_122]) ).
tcf(c_1958,plain,
rd(iPr_def_12,a) = op_b,
inference(superposition,[status(thm)],[c_103,c_122]) ).
tcf(c_1959,plain,
rd(iPr_def_10,op_b) = op_a,
inference(superposition,[status(thm)],[c_101,c_122]) ).
tcf(c_1960,plain,
rd(iPr_def_11,a) = iPr_def_10,
inference(superposition,[status(thm)],[c_102,c_122]) ).
tcf(c_1961,plain,
rd(iPr_def_13,iPr_def_12) = op_a,
inference(superposition,[status(thm)],[c_104,c_122]) ).
tcf(c_1962,plain,
rd(iPr_def_15,iPr_def_14) = op_b,
inference(superposition,[status(thm)],[c_106,c_122]) ).
tcf(c_1963,plain,
rd(iPr_def_16,iPr_def_15) = op_b,
inference(superposition,[status(thm)],[c_107,c_122]) ).
tcf(c_1964,plain,
rd(iPr_def_17,iPr_def_16) = op_b,
inference(superposition,[status(thm)],[c_108,c_122]) ).
tcf(c_1965,plain,
rd(iPr_def_18,iPr_def_17) = op_b,
inference(superposition,[status(thm)],[c_109,c_122]) ).
tcf(c_1966,plain,
rd(iPr_def_19,iPr_def_18) = op_b,
inference(superposition,[status(thm)],[c_110,c_122]) ).
tcf(c_1967,plain,
rd(iPr_def_20,iPr_def_19) = op_b,
inference(superposition,[status(thm)],[c_111,c_122]) ).
tcf(c_1971,plain,
! [X0: $i] : rd(X0,X0) = iPr_def_21,
inference(superposition,[status(thm)],[c_1954,c_122]) ).
tcf(c_1972,plain,
! [X0: $i] : rd(X0,iPr_def_21) = X0,
inference(superposition,[status(thm)],[c_1955,c_122]) ).
tcf(c_1973,plain,
mult(iPr_def_10,iPr_def_20) = op_a,
inference(demodulation,[status(thm)],[c_1959,c_1831]) ).
tcf(c_1974,plain,
mult(iPr_def_14,iPr_def_20) = op_b,
inference(demodulation,[status(thm)],[c_1957,c_1831]) ).
tcf(c_1981,plain,
mult(op_b,a) = iPr_def_12,
inference(superposition,[status(thm)],[c_1958,c_123]) ).
tcf(c_1982,plain,
mult(iPr_def_10,a) = iPr_def_11,
inference(superposition,[status(thm)],[c_1960,c_123]) ).
tcf(c_1983,plain,
mult(op_a,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_1961,c_123]) ).
tcf(c_1984,plain,
mult(op_b,iPr_def_14) = iPr_def_15,
inference(superposition,[status(thm)],[c_1962,c_123]) ).
tcf(c_1985,plain,
mult(op_b,iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_1963,c_123]) ).
tcf(c_1986,plain,
mult(op_b,iPr_def_16) = iPr_def_17,
inference(superposition,[status(thm)],[c_1964,c_123]) ).
tcf(c_1987,plain,
mult(op_b,iPr_def_17) = iPr_def_18,
inference(superposition,[status(thm)],[c_1965,c_123]) ).
tcf(c_1988,plain,
mult(op_b,iPr_def_18) = iPr_def_19,
inference(superposition,[status(thm)],[c_1966,c_123]) ).
tcf(c_1989,plain,
mult(op_b,iPr_def_19) = iPr_def_20,
inference(superposition,[status(thm)],[c_1967,c_123]) ).
tcf(c_2006,plain,
! [X0: $i,X1: $i] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[status(thm)],[c_123,c_124]) ).
tcf(c_2009,plain,
ld(op_b,iPr_def_14) = op_b,
inference(superposition,[status(thm)],[c_105,c_124]) ).
tcf(c_2017,plain,
ld(op_b,iPr_def_15) = iPr_def_14,
inference(superposition,[status(thm)],[c_1984,c_124]) ).
tcf(c_2019,plain,
ld(op_b,iPr_def_16) = iPr_def_15,
inference(superposition,[status(thm)],[c_1985,c_124]) ).
tcf(c_2021,plain,
ld(op_b,iPr_def_17) = iPr_def_16,
inference(superposition,[status(thm)],[c_1986,c_124]) ).
tcf(c_2023,plain,
ld(op_b,iPr_def_18) = iPr_def_17,
inference(superposition,[status(thm)],[c_1987,c_124]) ).
tcf(c_2029,plain,
ld(op_b,iPr_def_21) = iPr_def_20,
inference(superposition,[status(thm)],[c_112,c_124]) ).
tcf(c_2035,plain,
ld(iPr_def_14,op_b) = iPr_def_20,
inference(superposition,[status(thm)],[c_1974,c_124]) ).
tcf(c_2036,plain,
ld(iPr_def_10,op_a) = iPr_def_20,
inference(superposition,[status(thm)],[c_1973,c_124]) ).
tcf(c_2041,plain,
mult(op_b,op_b) = iPr_def_14,
inference(superposition,[status(thm)],[c_2009,c_125]) ).
tcf(c_2052,plain,
mult(op_b,iPr_def_20) = iPr_def_21,
inference(superposition,[status(thm)],[c_2029,c_125]) ).
tcf(c_2059,plain,
! [X0: $i,X1: $i] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_125,c_122]) ).
tcf(c_2071,plain,
! [X0: $i] : mult(mult(X0,op_b),iPr_def_20) = X0,
inference(superposition,[status(thm)],[c_1831,c_122]) ).
tcf(c_2078,plain,
mult(iPr_def_20,op_b) = iPr_def_21,
inference(superposition,[status(thm)],[c_1843,c_1971]) ).
tcf(c_2097,plain,
! [X0: $i] : ld(mult(X0,iPr_def_20),X0) = op_b,
inference(superposition,[status(thm)],[c_1831,c_2006]) ).
tcf(c_2098,plain,
! [X0: $i] : ld(mult(X0,op_b),X0) = iPr_def_20,
inference(superposition,[status(thm)],[c_1843,c_2006]) ).
tcf(c_2167,plain,
! [X0: $i] : mult(op_b,mult(op_b,X0)) = mult(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_2041,c_554]) ).
tcf(c_2173,plain,
! [X0: $i,X1: $i] : ld(mult(X0,X0),mult(X0,mult(X0,X1))) = X1,
inference(superposition,[status(thm)],[c_554,c_124]) ).
tcf(c_2174,plain,
! [X0: $i,X1: $i] : rd(mult(X0,mult(X0,X1)),X1) = mult(X0,X0),
inference(superposition,[status(thm)],[c_554,c_122]) ).
tcf(c_2268,plain,
! [X0: $i] : mult(iPr_def_14,ld(op_b,X0)) = mult(op_b,X0),
inference(superposition,[status(thm)],[c_125,c_2167]) ).
tcf(c_2273,plain,
mult(op_b,iPr_def_15) = mult(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_1984,c_2167]) ).
tcf(c_2275,plain,
mult(op_b,iPr_def_16) = mult(iPr_def_14,iPr_def_15),
inference(superposition,[status(thm)],[c_1985,c_2167]) ).
tcf(c_2277,plain,
mult(op_b,iPr_def_17) = mult(iPr_def_14,iPr_def_16),
inference(superposition,[status(thm)],[c_1986,c_2167]) ).
tcf(c_2279,plain,
mult(op_b,iPr_def_18) = mult(iPr_def_14,iPr_def_17),
inference(superposition,[status(thm)],[c_1987,c_2167]) ).
tcf(c_2281,plain,
mult(op_b,iPr_def_19) = mult(iPr_def_14,iPr_def_18),
inference(superposition,[status(thm)],[c_1988,c_2167]) ).
tcf(c_2283,plain,
mult(op_b,iPr_def_20) = mult(iPr_def_14,iPr_def_19),
inference(superposition,[status(thm)],[c_1989,c_2167]) ).
tcf(c_2290,plain,
! [X0: $i] : rd(mult(iPr_def_14,X0),mult(op_b,X0)) = op_b,
inference(superposition,[status(thm)],[c_2167,c_122]) ).
tcf(c_2292,plain,
mult(iPr_def_14,iPr_def_19) = iPr_def_21,
inference(demodulation,[status(thm)],[c_2283,c_2052]) ).
tcf(c_2293,plain,
mult(iPr_def_14,iPr_def_18) = iPr_def_20,
inference(demodulation,[status(thm)],[c_2281,c_1989]) ).
tcf(c_2294,plain,
mult(iPr_def_14,iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_2279,c_1988]) ).
tcf(c_2295,plain,
mult(iPr_def_14,iPr_def_16) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2277,c_1987]) ).
tcf(c_2296,plain,
mult(iPr_def_14,iPr_def_15) = iPr_def_17,
inference(demodulation,[status(thm)],[c_2275,c_1986]) ).
tcf(c_2297,plain,
mult(iPr_def_14,iPr_def_14) = iPr_def_16,
inference(demodulation,[status(thm)],[c_2273,c_1985]) ).
tcf(c_2310,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(X0,X1),mult(ld(X0,X1),X2))) = mult(mult(X1,ld(X0,X1)),X2),
inference(superposition,[status(thm)],[c_125,c_119]) ).
tcf(c_2357,plain,
! [X0: $i] : mult(iPr_def_14,mult(iPr_def_19,mult(iPr_def_19,X0))) = mult(mult(iPr_def_21,iPr_def_19),X0),
inference(superposition,[status(thm)],[c_2292,c_119]) ).
tcf(c_2359,plain,
! [X0: $i] : mult(iPr_def_20,mult(op_b,mult(op_b,X0))) = mult(mult(iPr_def_21,op_b),X0),
inference(superposition,[status(thm)],[c_2078,c_119]) ).
tcf(c_2362,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),X3) = mult(mult(mult(X0,X1),X1),mult(X2,mult(X2,X3))),
inference(superposition,[status(thm)],[c_119,c_119]) ).
tcf(c_2375,plain,
! [X0: $i] : mult(iPr_def_20,mult(iPr_def_14,X0)) = mult(op_b,X0),
inference(demodulation,[status(thm)],[c_2359,c_1954,c_2167]) ).
tcf(c_2376,plain,
! [X0: $i] : mult(iPr_def_14,mult(iPr_def_19,mult(iPr_def_19,X0))) = mult(iPr_def_19,X0),
inference(demodulation,[status(thm)],[c_2357,c_1954]) ).
tcf(c_2397,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),X3) = mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X3))))),
inference(demodulation,[status(thm)],[c_2362,c_119]) ).
tcf(c_2413,plain,
! [X0: $i,X1: $i] : mult(X0,mult(op_b,mult(op_b,X1))) = mult(mult(X0,iPr_def_14),X1),
inference(superposition,[status(thm)],[c_2041,c_561]) ).
tcf(c_2432,plain,
! [X0: $i,X1: $i] : mult(mult(X0,iPr_def_14),X1) = mult(X0,mult(iPr_def_14,X1)),
inference(demodulation,[status(thm)],[c_2413,c_2167]) ).
tcf(c_2454,plain,
! [X0: $i] : mult(iPr_def_15,ld(op_b,X0)) = mult(iPr_def_14,X0),
inference(light_normalisation,[status(thm)],[c_1268,c_2167]) ).
tcf(c_2456,plain,
mult(iPr_def_14,iPr_def_14) = mult(iPr_def_15,op_b),
inference(superposition,[status(thm)],[c_2009,c_2454]) ).
tcf(c_2458,plain,
mult(iPr_def_14,iPr_def_15) = mult(iPr_def_15,iPr_def_14),
inference(superposition,[status(thm)],[c_2017,c_2454]) ).
tcf(c_2459,plain,
mult(iPr_def_14,iPr_def_16) = mult(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_2019,c_2454]) ).
tcf(c_2460,plain,
mult(iPr_def_14,iPr_def_17) = mult(iPr_def_15,iPr_def_16),
inference(superposition,[status(thm)],[c_2021,c_2454]) ).
tcf(c_2461,plain,
mult(iPr_def_14,iPr_def_18) = mult(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_2023,c_2454]) ).
tcf(c_2464,plain,
mult(iPr_def_14,iPr_def_21) = mult(iPr_def_15,iPr_def_20),
inference(superposition,[status(thm)],[c_2029,c_2454]) ).
tcf(c_2468,plain,
mult(iPr_def_15,iPr_def_20) = iPr_def_14,
inference(demodulation,[status(thm)],[c_2464,c_1955]) ).
tcf(c_2470,plain,
mult(iPr_def_15,iPr_def_17) = iPr_def_20,
inference(demodulation,[status(thm)],[c_2461,c_2293]) ).
tcf(c_2471,plain,
mult(iPr_def_15,iPr_def_16) = iPr_def_19,
inference(demodulation,[status(thm)],[c_2460,c_2294]) ).
tcf(c_2472,plain,
mult(iPr_def_15,iPr_def_15) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2459,c_2295]) ).
tcf(c_2473,plain,
mult(iPr_def_15,iPr_def_14) = iPr_def_17,
inference(demodulation,[status(thm)],[c_2458,c_2296]) ).
tcf(c_2474,plain,
mult(iPr_def_15,op_b) = iPr_def_16,
inference(demodulation,[status(thm)],[c_2456,c_2297]) ).
tcf(c_2589,plain,
! [X0: $i,X1: $i] : mult(X0,mult(op_b,mult(op_b,mult(iPr_def_19,mult(iPr_def_19,X1))))) = mult(mult(mult(X0,mult(op_b,iPr_def_20)),iPr_def_19),X1),
inference(superposition,[status(thm)],[c_1989,c_2397]) ).
tcf(c_2647,plain,
! [X0: $i,X1: $i] : mult(mult(X0,iPr_def_19),X1) = mult(X0,mult(iPr_def_19,X1)),
inference(demodulation,[status(thm)],[c_2589,c_1955,c_2052,c_2376,c_2167]) ).
tcf(c_2697,plain,
ld(iPr_def_14,iPr_def_19) = iPr_def_17,
inference(superposition,[status(thm)],[c_2294,c_124]) ).
tcf(c_2738,plain,
rd(iPr_def_17,iPr_def_14) = iPr_def_15,
inference(superposition,[status(thm)],[c_2473,c_122]) ).
tcf(c_2741,plain,
ld(iPr_def_16,iPr_def_15) = iPr_def_20,
inference(superposition,[status(thm)],[c_2474,c_2098]) ).
tcf(c_3078,plain,
rd(mult(iPr_def_14,iPr_def_19),iPr_def_20) = op_b,
inference(superposition,[status(thm)],[c_1989,c_2290]) ).
tcf(c_3087,plain,
mult(iPr_def_14,mult(iPr_def_19,op_b)) = op_b,
inference(demodulation,[status(thm)],[c_3078,c_1843,c_2647]) ).
tcf(c_3105,plain,
ld(iPr_def_14,op_b) = mult(iPr_def_19,op_b),
inference(superposition,[status(thm)],[c_3087,c_124]) ).
tcf(c_3109,plain,
mult(iPr_def_19,op_b) = iPr_def_20,
inference(demodulation,[status(thm)],[c_3105,c_2035]) ).
tcf(c_3116,plain,
mult(iPr_def_20,iPr_def_20) = iPr_def_19,
inference(superposition,[status(thm)],[c_3109,c_2071]) ).
tcf(c_3135,plain,
! [X0: $i] : mult(iPr_def_20,mult(iPr_def_20,X0)) = mult(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_3116,c_554]) ).
tcf(c_3144,plain,
mult(op_b,iPr_def_14) = mult(iPr_def_20,iPr_def_16),
inference(superposition,[status(thm)],[c_2297,c_2375]) ).
tcf(c_3145,plain,
mult(op_b,iPr_def_15) = mult(iPr_def_20,iPr_def_17),
inference(superposition,[status(thm)],[c_2296,c_2375]) ).
tcf(c_3150,plain,
! [X0: $i] : mult(op_b,ld(op_b,X0)) = mult(iPr_def_20,mult(op_b,X0)),
inference(superposition,[status(thm)],[c_2268,c_2375]) ).
tcf(c_3151,plain,
mult(op_b,iPr_def_17) = mult(iPr_def_20,iPr_def_19),
inference(superposition,[status(thm)],[c_2294,c_2375]) ).
tcf(c_3155,plain,
mult(iPr_def_20,iPr_def_19) = iPr_def_18,
inference(demodulation,[status(thm)],[c_3151,c_1987]) ).
tcf(c_3157,plain,
mult(iPr_def_20,iPr_def_17) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3145,c_1985]) ).
tcf(c_3158,plain,
mult(iPr_def_20,iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_3144,c_1984]) ).
tcf(c_3161,plain,
! [X0: $i] : mult(iPr_def_20,mult(op_b,X0)) = X0,
inference(demodulation,[status(thm)],[c_3150,c_125]) ).
tcf(c_3431,plain,
ld(iPr_def_19,mult(iPr_def_20,iPr_def_19)) = iPr_def_20,
inference(superposition,[status(thm)],[c_3116,c_2173]) ).
tcf(c_3434,plain,
ld(mult(iPr_def_15,iPr_def_15),mult(iPr_def_15,iPr_def_16)) = op_b,
inference(superposition,[status(thm)],[c_2474,c_2173]) ).
tcf(c_3448,plain,
ld(mult(iPr_def_15,iPr_def_15),mult(iPr_def_15,iPr_def_20)) = iPr_def_17,
inference(superposition,[status(thm)],[c_2470,c_2173]) ).
tcf(c_3473,plain,
! [X0: $i] : ld(mult(iPr_def_20,iPr_def_20),mult(iPr_def_20,X0)) = mult(op_b,X0),
inference(superposition,[status(thm)],[c_3161,c_2173]) ).
tcf(c_3477,plain,
ld(iPr_def_19,iPr_def_18) = iPr_def_20,
inference(demodulation,[status(thm)],[c_3431,c_3155]) ).
tcf(c_3493,plain,
ld(iPr_def_18,iPr_def_14) = iPr_def_17,
inference(demodulation,[status(thm)],[c_3448,c_2468,c_2472]) ).
tcf(c_3496,plain,
ld(iPr_def_18,iPr_def_19) = op_b,
inference(demodulation,[status(thm)],[c_3434,c_2471,c_2472]) ).
tcf(c_3500,plain,
! [X0: $i] : ld(iPr_def_19,mult(iPr_def_20,X0)) = mult(op_b,X0),
inference(demodulation,[status(thm)],[c_3473,c_3116]) ).
tcf(c_3663,plain,
rd(mult(iPr_def_20,iPr_def_16),iPr_def_17) = mult(iPr_def_20,iPr_def_20),
inference(superposition,[status(thm)],[c_3157,c_2174]) ).
tcf(c_3666,plain,
rd(mult(iPr_def_14,iPr_def_21),iPr_def_19) = mult(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_2292,c_2174]) ).
tcf(c_3700,plain,
rd(iPr_def_14,iPr_def_19) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3666,c_1955,c_2297]) ).
tcf(c_3703,plain,
rd(iPr_def_15,iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_3663,c_3116,c_3158]) ).
tcf(c_3839,plain,
! [X0: $i,X1: $i] : mult(X0,mult(ld(X0,X1),ld(X0,X1))) = mult(mult(X1,ld(X0,X1)),iPr_def_21),
inference(superposition,[status(thm)],[c_1955,c_2310]) ).
tcf(c_3873,plain,
! [X0: $i,X1: $i,X2: $i] : ld(X0,mult(mult(X1,ld(X0,X1)),X2)) = mult(ld(X0,X1),mult(ld(X0,X1),X2)),
inference(superposition,[status(thm)],[c_2310,c_124]) ).
tcf(c_3905,plain,
! [X0: $i,X1: $i] : mult(X0,mult(ld(X0,X1),ld(X0,X1))) = mult(X1,ld(X0,X1)),
inference(demodulation,[status(thm)],[c_3839,c_1955]) ).
tcf(c_4030,plain,
! [X0: $i,X1: $i,X2: $i] : ld(rd(X0,X1),mult(mult(X0,X1),X2)) = mult(X1,mult(X1,X2)),
inference(superposition,[status(thm)],[c_2006,c_3873]) ).
tcf(c_4047,plain,
! [X0: $i] : ld(iPr_def_14,mult(mult(op_b,iPr_def_20),X0)) = mult(iPr_def_20,mult(iPr_def_20,X0)),
inference(superposition,[status(thm)],[c_2035,c_3873]) ).
tcf(c_4075,plain,
! [X0: $i] : ld(iPr_def_14,X0) = mult(iPr_def_19,X0),
inference(demodulation,[status(thm)],[c_4047,c_1954,c_2052,c_3135]) ).
tcf(c_4099,plain,
mult(iPr_def_19,iPr_def_19) = iPr_def_17,
inference(demodulation,[status(thm)],[c_2697,c_4075]) ).
tcf(c_4272,plain,
! [X0: $i] : ld(rd(iPr_def_15,iPr_def_17),mult(iPr_def_20,X0)) = mult(iPr_def_17,mult(iPr_def_17,X0)),
inference(superposition,[status(thm)],[c_2470,c_4030]) ).
tcf(c_4280,plain,
! [X0: $i] : ld(rd(iPr_def_14,iPr_def_19),mult(iPr_def_21,X0)) = mult(iPr_def_19,mult(iPr_def_19,X0)),
inference(superposition,[status(thm)],[c_2292,c_4030]) ).
tcf(c_4302,plain,
! [X0: $i,X1: $i,X2: $i] : rd(mult(mult(X0,X1),X2),mult(X1,mult(X1,X2))) = rd(X0,X1),
inference(superposition,[status(thm)],[c_4030,c_2059]) ).
tcf(c_4312,plain,
! [X0: $i] : mult(iPr_def_19,mult(iPr_def_19,X0)) = ld(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4280,c_1954,c_3700]) ).
tcf(c_4316,plain,
! [X0: $i] : mult(iPr_def_17,mult(iPr_def_17,X0)) = mult(op_b,X0),
inference(demodulation,[status(thm)],[c_4272,c_3703,c_3500]) ).
tcf(c_4992,plain,
! [X0: $i] : rd(mult(mult(X0,iPr_def_14),iPr_def_17),mult(iPr_def_14,iPr_def_19)) = rd(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_2294,c_4302]) ).
tcf(c_5017,plain,
! [X0: $i] : mult(X0,iPr_def_19) = rd(X0,iPr_def_14),
inference(demodulation,[status(thm)],[c_4992,c_1972,c_2292,c_2294,c_2432]) ).
tcf(c_5148,plain,
mult(iPr_def_17,iPr_def_19) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2738,c_5017]) ).
tcf(c_5744,plain,
mult(iPr_def_10,mult(iPr_def_20,iPr_def_20)) = mult(op_a,iPr_def_20),
inference(superposition,[status(thm)],[c_2036,c_3905]) ).
tcf(c_5777,plain,
mult(op_a,iPr_def_20) = mult(iPr_def_10,iPr_def_19),
inference(demodulation,[status(thm)],[c_5744,c_3116]) ).
tcf(c_5916,plain,
mult(iPr_def_19,mult(iPr_def_20,iPr_def_20)) = mult(iPr_def_18,iPr_def_20),
inference(superposition,[status(thm)],[c_3477,c_3905]) ).
tcf(c_5918,plain,
! [X0: $i] : mult(iPr_def_19,mult(iPr_def_20,mult(iPr_def_20,X0))) = mult(mult(iPr_def_18,iPr_def_20),X0),
inference(superposition,[status(thm)],[c_3477,c_2310]) ).
tcf(c_5922,plain,
mult(iPr_def_18,iPr_def_20) = iPr_def_17,
inference(demodulation,[status(thm)],[c_5916,c_3116,c_4099]) ).
tcf(c_5923,plain,
! [X0: $i] : mult(iPr_def_19,mult(iPr_def_20,mult(iPr_def_20,X0))) = mult(iPr_def_17,X0),
inference(demodulation,[status(thm)],[c_5918,c_5922]) ).
tcf(c_5924,plain,
! [X0: $i] : ld(iPr_def_16,X0) = mult(iPr_def_17,X0),
inference(demodulation,[status(thm)],[c_5923,c_3135,c_4312]) ).
tcf(c_5927,plain,
mult(iPr_def_17,iPr_def_15) = iPr_def_20,
inference(demodulation,[status(thm)],[c_2741,c_5924]) ).
tcf(c_6359,plain,
! [X0: $i] : mult(iPr_def_18,mult(iPr_def_17,mult(iPr_def_17,X0))) = mult(mult(iPr_def_14,iPr_def_17),X0),
inference(superposition,[status(thm)],[c_3493,c_2310]) ).
tcf(c_6363,plain,
! [X0: $i] : mult(iPr_def_18,mult(op_b,X0)) = mult(iPr_def_19,X0),
inference(demodulation,[status(thm)],[c_6359,c_2294,c_4316]) ).
tcf(c_6380,plain,
! [X0: $i] : mult(iPr_def_18,mult(op_b,mult(op_b,X0))) = mult(mult(iPr_def_19,op_b),X0),
inference(superposition,[status(thm)],[c_3496,c_2310]) ).
tcf(c_6383,plain,
! [X0: $i] : mult(iPr_def_19,mult(op_b,X0)) = mult(iPr_def_20,X0),
inference(demodulation,[status(thm)],[c_6380,c_3109,c_6363]) ).
tcf(c_6501,plain,
rd(mult(iPr_def_17,iPr_def_15),iPr_def_19) = mult(iPr_def_17,iPr_def_17),
inference(superposition,[status(thm)],[c_5148,c_2174]) ).
tcf(c_6504,plain,
mult(iPr_def_17,iPr_def_17) = op_b,
inference(demodulation,[status(thm)],[c_6501,c_1967,c_5927]) ).
tcf(c_6636,plain,
! [X0: $i,X1: $i] : mult(X0,mult(iPr_def_17,mult(iPr_def_17,X1))) = mult(mult(X0,op_b),X1),
inference(superposition,[status(thm)],[c_6504,c_561]) ).
tcf(c_6638,plain,
! [X0: $i,X1: $i] : mult(mult(X0,op_b),X1) = mult(X0,mult(op_b,X1)),
inference(demodulation,[status(thm)],[c_6636,c_4316]) ).
tcf(c_6896,plain,
ld(mult(iPr_def_10,iPr_def_19),op_a) = op_b,
inference(superposition,[status(thm)],[c_5777,c_2097]) ).
tcf(c_8231,plain,
! [X0: $i] : mult(mult(iPr_def_10,iPr_def_19),mult(op_b,mult(op_b,X0))) = mult(mult(op_a,op_b),X0),
inference(superposition,[status(thm)],[c_6896,c_2310]) ).
tcf(c_8234,plain,
! [X0: $i] : mult(op_a,mult(op_b,X0)) = mult(iPr_def_10,X0),
inference(demodulation,[status(thm)],[c_8231,c_2647,c_3161,c_6383,c_6638]) ).
tcf(c_19910,plain,
mult(op_a,iPr_def_12) = mult(iPr_def_10,a),
inference(superposition,[status(thm)],[c_1981,c_8234]) ).
tcf(c_19953,plain,
iPr_def_11 = iPr_def_13,
inference(demodulation,[status(thm)],[c_19910,c_1982,c_1983]) ).
tcf(c_19954,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_19953,c_116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP705-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 15:47:28 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running UEQ theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 26.49/4.32 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 26.49/4.32 % SZS status Started for theBenchmark.p
% 26.49/4.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.49/4.32
% 26.49/4.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.49/4.32
% 26.49/4.32 % ------ iProver source info
% 26.49/4.32
% 26.49/4.32 % git: date: 2026-07-19 20:42:38 +0200
% 26.49/4.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.49/4.32 % git: non_committed_changes: false
% 26.49/4.32
% 26.49/4.32 % ------ Parsing...% successful
% 26.49/4.32
% 26.49/4.32
% 26.49/4.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.49/4.32
% 26.49/4.32 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 26.49/4.32
% 26.49/4.32 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.49/4.32
% 26.49/4.32 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 26.49/4.32 % ------ Proving...
% 26.49/4.32 % ------ Problem Properties
% 26.49/4.32
% 26.49/4.32 %
% 26.49/4.32 % clauses 25
% 26.49/4.32 % conjectures 1
% 26.49/4.32 % EPR 3
% 26.49/4.32 % Horn 25
% 26.49/4.32 % unary 25
% 26.49/4.32 % binary 0
% 26.49/4.32 % lits 25
% 26.49/4.32 % lits eq 25
% 26.49/4.32 % fd_pure 0
% 26.49/4.32 % fd_pseudo 0
% 26.49/4.32 % fd_cond 0
% 26.49/4.32 % fd_pseudo_cond 0
% 26.49/4.32 % AC symbols 0
% 26.49/4.32
% 26.49/4.32 % ------ Input Options Time Limit: Unbounded
% 26.49/4.32
% 26.49/4.32
% 26.49/4.32 % ------
% 26.49/4.32 % Current options:
% 26.49/4.32 % ------
% 26.49/4.32
% 26.49/4.32
% 26.49/4.32 %
% 26.49/4.32
% 26.49/4.32 % ------ Proving...
% 26.49/4.32 %
% 26.49/4.32
% 26.49/4.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.49/4.32
% 26.49/4.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.49/4.32
% 26.49/4.32
%------------------------------------------------------------------------------