%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP769-1 : TPTP v9.3.1. Released v4.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:22 PM UTC 2026
% Result : Unsatisfiable 113.85s 28.94s
% Output : CNFRefutation 113.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 31
% Syntax : Number of formulae : 145 ( 145 unt; 12 def)
% Number of atoms : 236 ( 144 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 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 : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 180 ( 0 sgn 180 !; 0 ?; 127 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : product(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos01) ).
fof(f2,axiom,
! [X0] : product(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos02) ).
fof(f3,axiom,
! [X0,X1] : product(X0,difference(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos03) ).
fof(f4,axiom,
! [X0,X1] : difference(X0,product(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos04) ).
fof(f5,axiom,
! [X0,X1] : quotient(product(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos05) ).
fof(f6,axiom,
! [X0,X1] : product(quotient(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos06) ).
fof(f7,axiom,
! [X2,X0,X1] : difference(X0,product(product(X0,X1),X2)) = quotient(product(X1,product(X2,X0)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos07) ).
fof(f8,axiom,
! [X2,X0,X1] : difference(product(X0,X1),product(X0,product(X1,X2))) = quotient(quotient(product(X2,product(X0,X1)),X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos08) ).
fof(f9,axiom,
! [X0] : i(X0) = difference(X0,one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos09) ).
fof(f10,axiom,
! [X0] : j(X0) = quotient(one,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos10) ).
fof(f11,axiom,
! [X0] : product(i(X0),X0) = product(X0,j(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos11) ).
fof(f12,axiom,
! [X0] : eta(X0) = product(i(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos12) ).
fof(f13,plain,
! [X0] : product(i(X0),X0) = eta(X0),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0,X1] : product(i(i(X0)),X1) = product(eta(X0),product(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos13) ).
fof(f17,axiom,
! [X2,X0,X1] : product(eta(X0),product(X1,X2)) = product(product(eta(X0),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos16) ).
fof(f22,axiom,
! [X0,X1] : product(i(product(X0,X1)),i(i(X0))) = i(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos21) ).
fof(f23,axiom,
! [X0,X1] : product(j(j(X0)),j(product(X1,X0))) = j(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos22) ).
fof(f24,axiom,
! [X0,X1] : product(X0,i(product(X1,X0))) = i(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos23) ).
fof(f25,plain,
! [X0,X1] : i(X1) = product(X0,i(product(X1,X0))),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
! [X0,X1] : product(j(product(X0,X1)),X0) = j(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos24) ).
fof(f27,plain,
! [X0,X1] : j(X1) = product(j(product(X0,X1)),X0),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
product(product(x0,x1),x2) != product(product(x0,x2),difference(x2,product(x1,x2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f29,plain,
! [X0] : eta(X0) = product(difference(X0,one),X0),
inference(definition_unfolding,[],[f13,f9]) ).
fof(f30,plain,
! [X0] : product(difference(X0,one),X0) = product(X0,quotient(one,X0)),
inference(definition_unfolding,[],[f11,f9,f10]) ).
fof(f31,plain,
! [X0,X1] : product(difference(difference(X0,one),one),X1) = product(product(difference(X0,one),X0),product(X0,X1)),
inference(definition_unfolding,[],[f14,f9,f9,f29]) ).
fof(f34,plain,
! [X2,X0,X1] : product(product(difference(X0,one),X0),product(X1,X2)) = product(product(product(difference(X0,one),X0),X1),X2),
inference(definition_unfolding,[],[f17,f29,f29]) ).
fof(f38,plain,
! [X0,X1] : product(difference(product(X0,X1),one),difference(difference(X0,one),one)) = difference(X1,one),
inference(definition_unfolding,[],[f22,f9,f9,f9,f9]) ).
fof(f39,plain,
! [X0,X1] : product(quotient(one,quotient(one,X0)),quotient(one,product(X1,X0))) = quotient(one,X1),
inference(definition_unfolding,[],[f23,f10,f10,f10,f10]) ).
fof(f40,plain,
! [X0,X1] : difference(X1,one) = product(X0,difference(product(X1,X0),one)),
inference(definition_unfolding,[],[f25,f9,f9]) ).
fof(f41,plain,
! [X0,X1] : quotient(one,X1) = product(quotient(one,product(X0,X1)),X0),
inference(definition_unfolding,[],[f27,f10,f10]) ).
tcf(c_74,plain,
! [X0: $i] : product(X0,one) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_75,plain,
! [X0: $i] : product(one,X0) = X0,
inference(cnf_transformation,[],[f2]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] : product(X0,difference(X0,X1)) = X1,
inference(cnf_transformation,[],[f3]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] : difference(X0,product(X0,X1)) = X1,
inference(cnf_transformation,[],[f4]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] : quotient(product(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] : product(quotient(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] : difference(X0,product(product(X0,X1),X2)) = quotient(product(X1,product(X2,X0)),X0),
inference(cnf_transformation,[],[f7]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] : difference(product(X0,X1),product(X0,product(X1,X2))) = quotient(quotient(product(X2,product(X0,X1)),X1),X0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_82,plain,
! [X0: $i] : product(difference(X0,one),X0) = product(X0,quotient(one,X0)),
inference(cnf_transformation,[],[f30]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] : product(product(difference(X0,one),X0),product(X0,X1)) = product(difference(difference(X0,one),one),X1),
inference(cnf_transformation,[],[f31]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(product(difference(X0,one),X0),X1),X2) = product(product(difference(X0,one),X0),product(X1,X2)),
inference(cnf_transformation,[],[f34]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] : product(difference(product(X0,X1),one),difference(difference(X0,one),one)) = difference(X1,one),
inference(cnf_transformation,[],[f38]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,X0)),quotient(one,product(X1,X0))) = quotient(one,X1),
inference(cnf_transformation,[],[f39]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] : product(X0,difference(product(X1,X0),one)) = difference(X1,one),
inference(cnf_transformation,[],[f40]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] : product(quotient(one,product(X0,X1)),X0) = quotient(one,X1),
inference(cnf_transformation,[],[f41]) ).
tcf(c_94,negated_conjecture,
product(product(x0,x2),difference(x2,product(x1,x2))) != product(product(x0,x1),x2),
inference(cnf_transformation,[],[f28]) ).
tcf(c_161,definition,
iPr_def_10 = product(x0,x2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_162,definition,
iPr_def_11 = product(x1,x2),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_163,definition,
iPr_def_12 = difference(x2,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_164,definition,
iPr_def_13 = product(iPr_def_10,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_165,definition,
iPr_def_14 = product(x0,x1),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_166,definition,
iPr_def_15 = product(iPr_def_14,x2),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_167,negated_conjecture,
iPr_def_13 != iPr_def_15,
inference(demodulation,[status(thm)],[c_94,c_165,c_166,c_162,c_163,c_161,c_164]) ).
tcf(c_168,definition,
iPr_def_16 = product(x0,x1),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_169,definition,
iPr_def_17 = product(iPr_def_14,x2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_170,definition,
iPr_def_18 = product(x1,x2),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_171,definition,
iPr_def_19 = difference(x2,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_172,definition,
iPr_def_20 = product(x0,x2),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_173,definition,
iPr_def_21 = product(iPr_def_10,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_174,negated_conjecture,
iPr_def_13 != iPr_def_15,
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_175,plain,
iPr_def_14 = iPr_def_16,
inference(demodulation,[status(thm)],[c_165,c_168]) ).
tcf(c_176,plain,
iPr_def_15 = iPr_def_17,
inference(demodulation,[status(thm)],[c_166,c_169]) ).
tcf(c_177,plain,
iPr_def_11 = iPr_def_18,
inference(demodulation,[status(thm)],[c_162,c_170]) ).
tcf(c_178,plain,
iPr_def_12 = iPr_def_19,
inference(demodulation,[status(thm)],[c_163,c_171]) ).
tcf(c_179,plain,
iPr_def_10 = iPr_def_20,
inference(demodulation,[status(thm)],[c_161,c_172]) ).
tcf(c_180,plain,
iPr_def_13 = iPr_def_21,
inference(demodulation,[status(thm)],[c_164,c_173]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i] : product(quotient(one,product(X0,X1)),X0) = quotient(one,X1),
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i] : product(X0,difference(product(X1,X0),one)) = difference(X1,one),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,X0)),quotient(one,product(X1,X0))) = quotient(one,X1),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i] : product(difference(product(X0,X1),one),difference(difference(X0,one),one)) = difference(X1,one),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(product(difference(X0,one),X0),X1),X2) = product(product(difference(X0,one),X0),product(X1,X2)),
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i] : product(product(difference(X0,one),X0),product(X0,X1)) = product(difference(difference(X0,one),one),X1),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_192,plain,
! [X0: $i] : product(difference(X0,one),X0) = product(X0,quotient(one,X0)),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i,X2: $i] : difference(product(X0,X1),product(X0,product(X1,X2))) = quotient(quotient(product(X2,product(X0,X1)),X1),X0),
inference(demodulation,[status(thm)],[c_81]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i,X2: $i] : difference(X0,product(product(X0,X1),X2)) = quotient(product(X1,product(X2,X0)),X0),
inference(demodulation,[status(thm)],[c_80]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i] : product(quotient(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i] : quotient(product(X0,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_78]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i] : difference(X0,product(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_77]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i] : product(X0,difference(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_199,plain,
! [X0: $i] : product(one,X0) = X0,
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_200,plain,
! [X0: $i] : product(X0,one) = X0,
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i] : product(quotient(one,X0),quotient(X0,X1)) = quotient(one,X1),
inference(superposition,[status(thm)],[c_195,c_181]) ).
tcf(c_477,plain,
! [X0: $i,X1: $i] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_198,c_196]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i] : difference(quotient(one,X0),quotient(one,X1)) = quotient(X0,X1),
inference(superposition,[status(thm)],[c_360,c_197]) ).
tcf(c_1550,plain,
! [X0: $i,X1: $i] : difference(quotient(one,X0),X1) = quotient(X0,difference(X1,one)),
inference(superposition,[status(thm)],[c_477,c_770]) ).
tcf(c_2290,plain,
product(x0,x1) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_168,c_175]) ).
tcf(c_2292,plain,
product(x1,difference(iPr_def_14,one)) = difference(x0,one),
inference(superposition,[status(thm)],[c_2290,c_182]) ).
tcf(c_2295,plain,
! [X0: $i,X1: $i] : product(quotient(one,difference(X0,one)),X1) = quotient(one,difference(product(X0,X1),one)),
inference(superposition,[status(thm)],[c_182,c_181]) ).
tcf(c_2298,plain,
product(iPr_def_14,x2) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_169,c_176]) ).
tcf(c_2300,plain,
product(x2,difference(iPr_def_15,one)) = difference(iPr_def_14,one),
inference(superposition,[status(thm)],[c_2298,c_182]) ).
tcf(c_2301,plain,
product(x1,x2) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_170,c_177]) ).
tcf(c_2304,plain,
difference(x2,iPr_def_11) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_171,c_178]) ).
tcf(c_2305,plain,
product(x0,x2) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_172,c_179]) ).
tcf(c_2308,plain,
product(iPr_def_10,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_173,c_180]) ).
tcf(c_2309,plain,
product(quotient(one,iPr_def_13),iPr_def_10) = quotient(one,iPr_def_12),
inference(superposition,[status(thm)],[c_2308,c_181]) ).
tcf(c_2326,plain,
product(quotient(one,quotient(one,x2)),quotient(one,iPr_def_11)) = quotient(one,x1),
inference(superposition,[status(thm)],[c_2301,c_183]) ).
tcf(c_2332,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,X0)),quotient(one,quotient(one,X1))) = quotient(one,quotient(one,product(X0,X1))),
inference(superposition,[status(thm)],[c_183,c_181]) ).
tcf(c_2343,plain,
product(difference(iPr_def_14,one),difference(difference(x0,one),one)) = difference(x1,one),
inference(superposition,[status(thm)],[c_2292,c_182]) ).
tcf(c_2350,plain,
! [X0: $i] : quotient(X0,one) = X0,
inference(superposition,[status(thm)],[c_195,c_200]) ).
tcf(c_2352,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,X0)),quotient(one,X1)) = quotient(one,quotient(X1,X0)),
inference(superposition,[status(thm)],[c_195,c_183]) ).
tcf(c_2353,plain,
! [X0: $i,X1: $i] : product(X0,difference(X1,one)) = difference(quotient(X1,X0),one),
inference(superposition,[status(thm)],[c_195,c_182]) ).
tcf(c_2371,plain,
! [X0: $i,X1: $i] : quotient(quotient(one,X0),X1) = quotient(one,product(X1,X0)),
inference(superposition,[status(thm)],[c_181,c_196]) ).
tcf(c_2399,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,difference(difference(X0,one),one))),quotient(one,difference(X1,one))) = quotient(one,difference(product(X0,X1),one)),
inference(superposition,[status(thm)],[c_184,c_183]) ).
tcf(c_2401,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,difference(difference(X0,one),one))),quotient(one,difference(X1,one))) = product(quotient(one,difference(X0,one)),X1),
inference(demodulation,[status(thm)],[c_2399,c_2295]) ).
tcf(c_2410,plain,
! [X0: $i] : difference(one,X0) = X0,
inference(superposition,[status(thm)],[c_199,c_197]) ).
tcf(c_2411,plain,
! [X0: $i,X1: $i] : difference(quotient(X0,X1),X0) = X1,
inference(superposition,[status(thm)],[c_195,c_197]) ).
tcf(c_2417,plain,
! [X0: $i,X1: $i] : difference(product(X0,X1),one) = difference(X1,difference(X0,one)),
inference(superposition,[status(thm)],[c_182,c_197]) ).
tcf(c_2458,plain,
product(x2,iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_2304,c_198]) ).
tcf(c_2467,plain,
! [X0: $i,X1: $i] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_198,c_196]) ).
tcf(c_2468,plain,
! [X0: $i,X1: $i] : product(quotient(one,X0),X1) = quotient(one,difference(X1,X0)),
inference(superposition,[status(thm)],[c_198,c_181]) ).
tcf(c_2475,plain,
! [X0: $i,X1: $i] : product(quotient(one,quotient(one,difference(difference(X0,one),one))),quotient(one,difference(X1,one))) = product(X0,X1),
inference(demodulation,[status(thm)],[c_2401,c_2467]) ).
tcf(c_2480,plain,
! [X0: $i,X1: $i] : product(quotient(one,product(quotient(one,one),difference(X0,one))),product(quotient(one,one),X1)) = product(X0,X1),
inference(demodulation,[status(thm)],[c_2475,c_2468]) ).
tcf(c_2481,plain,
! [X0: $i,X1: $i] : product(quotient(one,difference(X0,one)),X1) = product(X0,X1),
inference(demodulation,[status(thm)],[c_2480,c_199,c_2350]) ).
tcf(c_2485,plain,
product(quotient(one,iPr_def_11),x2) = quotient(one,iPr_def_12),
inference(superposition,[status(thm)],[c_2458,c_181]) ).
tcf(c_2546,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(product(X0,quotient(one,X0)),X1),X2) = product(product(X0,quotient(one,X0)),product(X1,X2)),
inference(light_normalisation,[status(thm)],[c_188,c_192]) ).
tcf(c_2562,plain,
! [X0: $i,X1: $i,X2: $i] : product(quotient(one,quotient(one,X0)),quotient(one,product(product(X1,quotient(one,X1)),product(X2,X0)))) = quotient(one,product(product(X1,quotient(one,X1)),X2)),
inference(superposition,[status(thm)],[c_2546,c_183]) ).
tcf(c_2578,plain,
quotient(quotient(one,iPr_def_12),x2) = quotient(one,iPr_def_11),
inference(superposition,[status(thm)],[c_2485,c_196]) ).
tcf(c_2799,plain,
! [X0: $i,X1: $i] : product(difference(X0,X1),difference(X1,one)) = difference(X0,one),
inference(superposition,[status(thm)],[c_2467,c_2353]) ).
tcf(c_2812,plain,
! [X0: $i,X1: $i] : quotient(one,product(X0,difference(X1,one))) = quotient(X1,X0),
inference(superposition,[status(thm)],[c_2353,c_2467]) ).
tcf(c_2819,plain,
! [X0: $i,X1: $i] : product(product(X0,quotient(one,X0)),product(X0,X1)) = product(difference(difference(X0,one),one),X1),
inference(light_normalisation,[status(thm)],[c_191,c_192]) ).
tcf(c_2843,plain,
product(product(x2,quotient(one,x2)),difference(iPr_def_14,one)) = product(difference(difference(x2,one),one),difference(iPr_def_15,one)),
inference(superposition,[status(thm)],[c_2300,c_2819]) ).
tcf(c_2989,plain,
! [X0: $i] : difference(iPr_def_10,product(x0,product(x2,X0))) = quotient(quotient(product(X0,iPr_def_10),x2),x0),
inference(superposition,[status(thm)],[c_2305,c_193]) ).
tcf(c_3082,plain,
product(product(quotient(one,quotient(one,x2)),quotient(one,quotient(one,quotient(one,x2)))),quotient(one,x1)) = product(difference(difference(quotient(one,quotient(one,x2)),one),one),quotient(one,iPr_def_11)),
inference(superposition,[status(thm)],[c_2326,c_2819]) ).
tcf(c_3089,plain,
quotient(one,quotient(x1,product(x2,quotient(one,x2)))) = product(x2,quotient(one,iPr_def_11)),
inference(demodulation,[status(thm)],[c_3082,c_199,c_2332,c_2350,c_2352,c_2371,c_2410,c_1550]) ).
tcf(c_3142,plain,
! [X0: $i,X1: $i] : product(quotient(one,X0),quotient(one,X1)) = quotient(one,quotient(X1,difference(X0,one))),
inference(superposition,[status(thm)],[c_1550,c_2468]) ).
tcf(c_3267,plain,
! [X0: $i] : quotient(product(x2,product(X0,x0)),x0) = difference(x0,product(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_2305,c_194]) ).
tcf(c_4708,plain,
! [X0: $i] : product(difference(x0,product(iPr_def_10,X0)),x0) = product(x2,product(X0,x0)),
inference(superposition,[status(thm)],[c_3267,c_195]) ).
tcf(c_6977,plain,
! [X0: $i] : product(x2,product(difference(iPr_def_10,X0),x0)) = product(difference(x0,X0),x0),
inference(superposition,[status(thm)],[c_198,c_4708]) ).
tcf(c_12309,plain,
! [X0: $i] : product(quotient(one,quotient(one,difference(difference(x0,one),one))),quotient(one,product(product(X0,quotient(one,X0)),difference(x1,one)))) = quotient(one,product(product(X0,quotient(one,X0)),difference(iPr_def_14,one))),
inference(superposition,[status(thm)],[c_2343,c_2562]) ).
tcf(c_12335,plain,
! [X0: $i,X1: $i,X2: $i] : product(quotient(one,quotient(one,difference(X0,one))),quotient(one,product(product(X1,quotient(one,X1)),difference(X2,one)))) = quotient(one,product(product(X1,quotient(one,X1)),difference(X2,X0))),
inference(superposition,[status(thm)],[c_2799,c_2562]) ).
tcf(c_12461,plain,
! [X0: $i,X1: $i,X2: $i] : product(quotient(one,X0),quotient(X1,product(X2,quotient(one,X2)))) = quotient(one,product(product(X2,quotient(one,X2)),difference(X1,X0))),
inference(demodulation,[status(thm)],[c_12335,c_200,c_2350,c_2812,c_3142]) ).
tcf(c_12526,plain,
! [X0: $i] : product(quotient(one,quotient(one,difference(difference(x0,one),one))),product(quotient(one,one),quotient(x1,product(X0,quotient(one,X0))))) = product(quotient(one,one),quotient(iPr_def_14,product(X0,quotient(one,X0)))),
inference(demodulation,[status(thm)],[c_12309,c_12461]) ).
tcf(c_12527,plain,
! [X0: $i] : product(x0,quotient(x1,product(X0,quotient(one,X0)))) = quotient(iPr_def_14,product(X0,quotient(one,X0))),
inference(demodulation,[status(thm)],[c_12526,c_200,c_199,c_2350,c_2481,c_3142]) ).
tcf(c_21555,plain,
difference(product(x2,quotient(one,iPr_def_11)),one) = quotient(x1,product(x2,quotient(one,x2))),
inference(superposition,[status(thm)],[c_3089,c_2411]) ).
tcf(c_21929,plain,
! [X0: $i] : product(x2,product(quotient(quotient(product(X0,iPr_def_10),x2),x0),x0)) = product(difference(x0,product(x0,product(x2,X0))),x0),
inference(superposition,[status(thm)],[c_2989,c_6977]) ).
tcf(c_21935,plain,
! [X0: $i] : product(x2,quotient(product(X0,iPr_def_10),x2)) = product(product(x2,X0),x0),
inference(demodulation,[status(thm)],[c_21929,c_197,c_195]) ).
tcf(c_21950,plain,
product(product(x2,quotient(one,iPr_def_13)),x0) = product(x2,quotient(quotient(one,iPr_def_12),x2)),
inference(superposition,[status(thm)],[c_2309,c_21935]) ).
tcf(c_21990,plain,
product(product(x2,quotient(one,iPr_def_13)),x0) = product(x2,quotient(one,iPr_def_11)),
inference(demodulation,[status(thm)],[c_21950,c_2578]) ).
tcf(c_22318,plain,
difference(product(x2,quotient(one,iPr_def_13)),product(x2,quotient(one,iPr_def_11))) = x0,
inference(superposition,[status(thm)],[c_21990,c_197]) ).
tcf(c_22349,plain,
product(x0,difference(product(x2,quotient(one,iPr_def_11)),one)) = difference(product(x2,quotient(one,iPr_def_13)),one),
inference(superposition,[status(thm)],[c_22318,c_2799]) ).
tcf(c_22354,plain,
quotient(iPr_def_13,difference(difference(x2,one),one)) = quotient(iPr_def_14,product(x2,quotient(one,x2))),
inference(demodulation,[status(thm)],[c_22349,c_2417,c_1550,c_12527,c_21555]) ).
tcf(c_30562,plain,
product(quotient(one,product(product(x2,quotient(one,x2)),difference(iPr_def_14,one))),difference(difference(x2,one),one)) = quotient(one,difference(iPr_def_15,one)),
inference(superposition,[status(thm)],[c_2843,c_181]) ).
tcf(c_30575,plain,
iPr_def_13 = iPr_def_15,
inference(demodulation,[status(thm)],[c_30562,c_199,c_195,c_2350,c_2468,c_12461,c_22354]) ).
tcf(c_31683,plain,
iPr_def_13 != iPr_def_13,
inference(demodulation,[status(thm)],[c_174,c_30575]) ).
tcf(c_31685,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_31683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP769-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 16:05:35 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.41 Running UEQ theorem proving
% 0.11/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.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 113.85/28.94 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 113.85/28.94 % SZS status Started for theBenchmark.p
% 113.85/28.94 % SZS status Unsatisfiable for theBenchmark.p
% 113.85/28.94
% 113.85/28.94 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 113.85/28.94
% 113.85/28.94 % ------ iProver source info
% 113.85/28.94
% 113.85/28.94 % git: date: 2026-07-19 20:42:38 +0200
% 113.85/28.94 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 113.85/28.94 % git: non_committed_changes: false
% 113.85/28.94
% 113.85/28.94 % ------ Parsing...% successful
% 113.85/28.94
% 113.85/28.94
% 113.85/28.94 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 113.85/28.94
% 113.85/28.94 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 113.85/28.94
% 113.85/28.94 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 113.85/28.94
% 113.85/28.94 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 113.85/28.94 % ------ Proving...
% 113.85/28.94 % ------ Problem Properties
% 113.85/28.94
% 113.85/28.94 %
% 113.85/28.94 % clauses 33
% 113.85/28.94 % conjectures 1
% 113.85/28.94 % EPR 7
% 113.85/28.94 % Horn 33
% 113.85/28.94 % unary 33
% 113.85/28.94 % binary 0
% 113.85/28.95 % lits 33
% 113.85/28.95 % lits eq 33
% 113.85/28.95 % fd_pure 0
% 113.85/28.95 % fd_pseudo 0
% 113.85/28.95 % fd_cond 0
% 113.85/28.95 % fd_pseudo_cond 0
% 113.85/28.95 % AC symbols 0
% 113.85/28.95
% 113.85/28.95 % ------ Input Options Time Limit: Unbounded
% 113.85/28.95
% 113.85/28.95
% 113.85/28.95 % ------
% 113.85/28.95 % Current options:
% 113.85/28.95 % ------
% 113.85/28.95
% 113.85/28.95
% 113.85/28.95 %
% 113.85/28.95
% 113.85/28.95 % ------ Proving...
% 113.85/28.95 %
% 113.85/28.95
% 113.85/28.95 % SZS status Unsatisfiable for theBenchmark.p
% 113.85/28.95
% 113.85/28.95 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 113.85/28.95
% 113.85/28.95
%------------------------------------------------------------------------------