%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n016.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:23 PM UTC 2026
% Result : Unsatisfiable 15.72s 3.16s
% Output : CNFRefutation 15.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 10
% Syntax : Number of formulae : 158 ( 158 unt; 0 def)
% Number of atoms : 158 ( 157 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 157 ( 0 sgn 157 !; 0 ?; 139 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : difference(X0,product(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos01) ).
fof(f2,axiom,
! [X0,X1] : product(X0,difference(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos02) ).
fof(f3,axiom,
! [X0,X1] : quotient(product(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos03) ).
fof(f4,axiom,
! [X0,X1] : product(quotient(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos04) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : product(product(X0,X1),product(X2,X3)) = product(product(X0,X2),product(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos05) ).
fof(f6,axiom,
! [X0] : product(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos06) ).
fof(f7,axiom,
! [X0,X1] : product(product(product(X0,X1),X1),product(X1,product(X1,X0))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos07) ).
fof(f8,axiom,
! [X2,X0,X1] : bigC(X0,X1,X2) = product(product(X0,X1),product(X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos08) ).
fof(f9,axiom,
product(product(a,c),product(c,b)) = product(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos09) ).
fof(f10,negated_conjecture,
bigC(a,b,x0) != bigC(c,c,x0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f11,plain,
product(product(a,b),product(x0,a)) != product(product(c,c),product(x0,c)),
inference(definition_unfolding,[],[f10,f8,f8]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] : difference(X0,product(X0,X1)) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] : product(X0,difference(X0,X1)) = X1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : quotient(product(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : product(quotient(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : product(product(X0,X1),product(X2,X3)) = product(product(X0,X2),product(X1,X3)),
inference(cnf_transformation,[],[f5]) ).
tcf(c_64,plain,
! [X0: $i] : product(X0,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] : product(product(product(X0,X1),X1),product(X1,product(X1,X0))) = X1,
inference(cnf_transformation,[],[f7]) ).
tcf(c_66,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(cnf_transformation,[],[f9]) ).
tcf(c_67,negated_conjecture,
product(product(a,b),product(x0,a)) != product(product(c,c),product(x0,c)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_93,plain,
product(product(a,b),product(x0,a)) != product(c,product(x0,c)),
inference(demodulation,[status(thm)],[c_67,c_64]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_60,c_61]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] : difference(quotient(X0,X1),X0) = X1,
inference(superposition,[status(thm)],[c_62,c_59]) ).
tcf(c_161,plain,
quotient(product(a,b),product(c,b)) = product(a,c),
inference(superposition,[status(thm)],[c_66,c_61]) ).
tcf(c_162,plain,
difference(product(a,c),product(a,b)) = product(c,b),
inference(superposition,[status(thm)],[c_66,c_59]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] : product(product(X0,X1),product(X1,product(X1,quotient(X0,X1)))) = X1,
inference(superposition,[status(thm)],[c_62,c_65]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i] : product(product(product(difference(X0,X1),X0),X0),product(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_60,c_65]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : product(product(quotient(X0,X1),X2),product(X1,X3)) = product(X0,product(X2,X3)),
inference(superposition,[status(thm)],[c_62,c_63]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(X0,X1),product(X0,X2)) = product(X0,product(X1,X2)),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : product(product(X0,quotient(X1,X2)),product(X3,X2)) = product(product(X0,X3),X1),
inference(superposition,[status(thm)],[c_62,c_63]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(X0,X1),product(X2,X1)) = product(product(X0,X2),X1),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i] : product(X0,product(X0,quotient(X1,X0))) = difference(product(X1,X0),X0),
inference(superposition,[status(thm)],[c_164,c_59]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] : product(product(difference(X0,X1),X0),X0) = quotient(X0,product(X0,X1)),
inference(superposition,[status(thm)],[c_167,c_61]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i] : product(X0,product(difference(X0,X1),X2)) = product(X1,product(X0,X2)),
inference(superposition,[status(thm)],[c_60,c_203]) ).
tcf(c_461,plain,
! [X0: $i,X1: $i,X2: $i] : product(X0,product(X1,difference(X0,X2))) = product(product(X0,X1),X2),
inference(superposition,[status(thm)],[c_60,c_203]) ).
tcf(c_465,plain,
! [X0: $i,X1: $i] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(superposition,[status(thm)],[c_64,c_203]) ).
tcf(c_474,plain,
! [X0: $i,X1: $i,X2: $i] : quotient(product(X0,product(X1,X2)),product(X0,X2)) = product(X0,X1),
inference(superposition,[status(thm)],[c_203,c_61]) ).
tcf(c_475,plain,
! [X0: $i,X1: $i,X2: $i] : difference(product(X0,X1),product(X0,product(X1,X2))) = product(X0,X2),
inference(superposition,[status(thm)],[c_203,c_59]) ).
tcf(c_559,plain,
! [X0: $i,X1: $i] : quotient(product(X0,product(X1,X0)),X0) = product(X0,X1),
inference(superposition,[status(thm)],[c_465,c_61]) ).
tcf(c_665,plain,
! [X0: $i,X1: $i] : product(X0,quotient(X1,X0)) = quotient(product(X0,X1),X0),
inference(superposition,[status(thm)],[c_62,c_559]) ).
tcf(c_732,plain,
! [X0: $i,X1: $i] : product(X0,quotient(difference(X0,X1),X0)) = quotient(X1,X0),
inference(superposition,[status(thm)],[c_60,c_665]) ).
tcf(c_743,plain,
! [X0: $i,X1: $i] : difference(product(X0,quotient(X1,X0)),product(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_665,c_156]) ).
tcf(c_818,plain,
! [X0: $i,X1: $i] : difference(X0,quotient(X1,X0)) = quotient(difference(X0,X1),X0),
inference(superposition,[status(thm)],[c_732,c_59]) ).
tcf(c_887,plain,
! [X0: $i,X1: $i] : difference(product(X0,product(X0,quotient(X1,X0))),product(X0,product(X0,X1))) = X0,
inference(superposition,[status(thm)],[c_665,c_743]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i] : difference(difference(product(X0,X1),X1),product(X1,product(X1,X0))) = X1,
inference(light_normalisation,[status(thm)],[c_887,c_297]) ).
tcf(c_927,plain,
! [X0: $i,X1: $i] : product(difference(X0,quotient(X1,X0)),X0) = difference(X0,X1),
inference(superposition,[status(thm)],[c_818,c_62]) ).
tcf(c_1002,plain,
! [X0: $i,X1: $i] : product(difference(X0,X1),X0) = difference(X0,product(X1,X0)),
inference(superposition,[status(thm)],[c_61,c_927]) ).
tcf(c_1316,plain,
! [X0: $i,X1: $i,X2: $i] : product(product(quotient(X0,X1),X2),X1) = product(X0,product(X2,X1)),
inference(superposition,[status(thm)],[c_62,c_210]) ).
tcf(c_1348,plain,
! [X0: $i,X1: $i,X2: $i] : quotient(product(product(X0,X1),X2),product(X1,X2)) = product(X0,X2),
inference(superposition,[status(thm)],[c_210,c_61]) ).
tcf(c_1487,plain,
! [X0: $i,X1: $i] : quotient(difference(product(X0,X1),X1),product(X1,quotient(X0,X1))) = X1,
inference(superposition,[status(thm)],[c_297,c_61]) ).
tcf(c_1582,plain,
! [X0: $i,X1: $i] : quotient(X0,product(X0,quotient(X1,X0))) = product(difference(X0,X1),X0),
inference(superposition,[status(thm)],[c_927,c_347]) ).
tcf(c_1806,plain,
! [X0: $i,X1: $i,X2: $i] : difference(X0,product(product(X0,X1),X2)) = product(X1,difference(X0,X2)),
inference(superposition,[status(thm)],[c_461,c_59]) ).
tcf(c_1924,plain,
! [X0: $i,X1: $i,X2: $i] : quotient(product(X0,X1),product(X0,X2)) = product(X0,quotient(X1,X2)),
inference(superposition,[status(thm)],[c_62,c_474]) ).
tcf(c_2162,plain,
! [X0: $i,X1: $i,X2: $i] : difference(product(X0,X1),product(X0,X2)) = product(X0,difference(X1,X2)),
inference(superposition,[status(thm)],[c_60,c_475]) ).
tcf(c_2197,plain,
product(a,difference(c,b)) = product(c,b),
inference(demodulation,[status(thm)],[c_162,c_2162]) ).
tcf(c_2319,plain,
product(a,product(difference(c,b),a)) = product(product(c,b),a),
inference(superposition,[status(thm)],[c_2197,c_465]) ).
tcf(c_2334,plain,
product(product(c,a),b) = product(c,product(c,b)),
inference(superposition,[status(thm)],[c_2197,c_461]) ).
tcf(c_2770,plain,
! [X0: $i,X1: $i,X2: $i] : quotient(product(X0,product(X1,X2)),X2) = product(quotient(X0,X2),X1),
inference(superposition,[status(thm)],[c_1316,c_61]) ).
tcf(c_3079,plain,
quotient(product(c,product(c,b)),b) = product(c,a),
inference(superposition,[status(thm)],[c_2334,c_61]) ).
tcf(c_3124,plain,
product(quotient(c,b),c) = product(c,a),
inference(demodulation,[status(thm)],[c_3079,c_2770]) ).
tcf(c_3134,plain,
quotient(product(c,a),c) = quotient(c,b),
inference(superposition,[status(thm)],[c_3124,c_61]) ).
tcf(c_3135,plain,
difference(quotient(c,b),product(c,a)) = c,
inference(superposition,[status(thm)],[c_3124,c_59]) ).
tcf(c_3209,plain,
product(c,quotient(a,c)) = quotient(c,b),
inference(demodulation,[status(thm)],[c_3134,c_665]) ).
tcf(c_3470,plain,
! [X0: $i,X1: $i,X2: $i] : quotient(product(X0,X1),product(X2,X1)) = product(quotient(X0,X2),X1),
inference(superposition,[status(thm)],[c_62,c_1348]) ).
tcf(c_3541,plain,
product(quotient(a,c),b) = product(a,c),
inference(demodulation,[status(thm)],[c_161,c_3470]) ).
tcf(c_3761,plain,
product(product(a,c),c) = product(a,product(b,c)),
inference(superposition,[status(thm)],[c_3541,c_1316]) ).
tcf(c_3833,plain,
difference(product(a,c),product(a,product(b,c))) = c,
inference(superposition,[status(thm)],[c_3761,c_59]) ).
tcf(c_3877,plain,
product(a,product(difference(c,b),c)) = c,
inference(demodulation,[status(thm)],[c_3833,c_1002,c_2162]) ).
tcf(c_3887,plain,
product(difference(c,b),c) = difference(a,c),
inference(superposition,[status(thm)],[c_3877,c_59]) ).
tcf(c_3938,plain,
quotient(difference(a,c),c) = difference(c,b),
inference(superposition,[status(thm)],[c_3887,c_61]) ).
tcf(c_3946,plain,
product(difference(a,c),c) = quotient(c,product(c,b)),
inference(superposition,[status(thm)],[c_3887,c_347]) ).
tcf(c_3949,plain,
product(c,difference(a,c)) = product(b,product(c,c)),
inference(superposition,[status(thm)],[c_3887,c_454]) ).
tcf(c_4037,plain,
difference(product(difference(a,c),c),c) = product(c,b),
inference(superposition,[status(thm)],[c_3946,c_156]) ).
tcf(c_4058,plain,
product(c,difference(a,c)) = product(b,c),
inference(demodulation,[status(thm)],[c_3949,c_64]) ).
tcf(c_4062,plain,
! [X0: $i] : product(product(b,c),product(c,X0)) = product(c,product(difference(a,c),X0)),
inference(superposition,[status(thm)],[c_4058,c_203]) ).
tcf(c_4625,plain,
! [X0: $i,X1: $i] : difference(difference(product(quotient(X0,X1),X1),X1),difference(product(X0,X1),X1)) = X1,
inference(superposition,[status(thm)],[c_297,c_905]) ).
tcf(c_4667,plain,
! [X0: $i,X1: $i] : difference(difference(X0,X1),difference(product(X0,X1),X1)) = X1,
inference(light_normalisation,[status(thm)],[c_4625,c_62]) ).
tcf(c_4881,plain,
difference(difference(difference(a,c),c),product(c,b)) = c,
inference(superposition,[status(thm)],[c_4037,c_4667]) ).
tcf(c_4883,plain,
! [X0: $i,X1: $i] : difference(difference(quotient(X0,X1),X1),difference(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_62,c_4667]) ).
tcf(c_4915,plain,
! [X0: $i,X1: $i] : product(difference(X0,X1),X1) = difference(product(X0,X1),X1),
inference(superposition,[status(thm)],[c_4667,c_60]) ).
tcf(c_5058,plain,
difference(difference(a,c),c) = quotient(product(c,b),c),
inference(superposition,[status(thm)],[c_4881,c_151]) ).
tcf(c_5076,plain,
! [X0: $i,X1: $i] : difference(difference(quotient(quotient(X0,X1),X0),X0),X1) = X0,
inference(superposition,[status(thm)],[c_156,c_4883]) ).
tcf(c_5092,plain,
! [X0: $i,X1: $i] : product(difference(quotient(X0,X1),X1),X1) = difference(X0,X1),
inference(superposition,[status(thm)],[c_4883,c_60]) ).
tcf(c_5095,plain,
! [X0: $i,X1: $i] : difference(quotient(X0,X1),X1) = quotient(difference(X0,X1),X1),
inference(superposition,[status(thm)],[c_4883,c_151]) ).
tcf(c_5098,plain,
difference(quotient(a,c),c) = difference(c,b),
inference(demodulation,[status(thm)],[c_3938,c_5095]) ).
tcf(c_5245,plain,
product(quotient(a,c),difference(c,b)) = c,
inference(superposition,[status(thm)],[c_5098,c_60]) ).
tcf(c_5479,plain,
! [X0: $i,X1: $i] : product(quotient(X0,X1),difference(X0,X1)) = product(X1,product(quotient(X0,X1),X1)),
inference(superposition,[status(thm)],[c_5092,c_454]) ).
tcf(c_5482,plain,
! [X0: $i,X1: $i] : product(quotient(X0,X1),difference(X0,X1)) = product(X1,X0),
inference(light_normalisation,[status(thm)],[c_5479,c_62]) ).
tcf(c_5681,plain,
product(c,quotient(b,c)) = difference(difference(a,c),c),
inference(demodulation,[status(thm)],[c_5058,c_665]) ).
tcf(c_5769,plain,
! [X0: $i,X1: $i] : difference(quotient(quotient(X0,X1),X0),X0) = quotient(X1,X0),
inference(superposition,[status(thm)],[c_5076,c_151]) ).
tcf(c_6502,plain,
! [X0: $i,X1: $i] : difference(quotient(X0,X1),product(X1,X0)) = difference(X0,X1),
inference(superposition,[status(thm)],[c_5482,c_59]) ).
tcf(c_6753,plain,
! [X0: $i,X1: $i] : quotient(quotient(X0,X1),X0) = quotient(X0,quotient(X1,X0)),
inference(superposition,[status(thm)],[c_5769,c_151]) ).
tcf(c_7084,plain,
! [X0: $i] : product(a,product(difference(c,b),X0)) = product(c,product(c,X0)),
inference(superposition,[status(thm)],[c_5245,c_200]) ).
tcf(c_8866,plain,
! [X0: $i,X1: $i] : quotient(product(difference(X0,X1),X1),product(X1,quotient(X0,X1))) = X1,
inference(light_normalisation,[status(thm)],[c_1487,c_4915]) ).
tcf(c_9359,plain,
product(difference(c,a),c) = quotient(c,quotient(c,b)),
inference(superposition,[status(thm)],[c_3209,c_1582]) ).
tcf(c_9500,plain,
product(product(difference(c,a),c),quotient(c,b)) = c,
inference(superposition,[status(thm)],[c_9359,c_62]) ).
tcf(c_11310,plain,
! [X0: $i,X1: $i,X2: $i] : product(X0,difference(quotient(X1,X0),X2)) = difference(quotient(X1,X0),product(X1,X2)),
inference(superposition,[status(thm)],[c_62,c_1806]) ).
tcf(c_11369,plain,
product(b,difference(quotient(c,b),a)) = c,
inference(demodulation,[status(thm)],[c_3135,c_11310]) ).
tcf(c_11675,plain,
difference(quotient(c,b),a) = difference(b,c),
inference(superposition,[status(thm)],[c_11369,c_59]) ).
tcf(c_11713,plain,
product(quotient(c,b),difference(b,c)) = a,
inference(superposition,[status(thm)],[c_11675,c_60]) ).
tcf(c_11718,plain,
quotient(a,difference(b,c)) = quotient(c,b),
inference(superposition,[status(thm)],[c_11675,c_151]) ).
tcf(c_12308,plain,
! [X0: $i,X1: $i] : product(X0,quotient(X0,X1)) = quotient(X0,product(X0,X1)),
inference(superposition,[status(thm)],[c_64,c_1924]) ).
tcf(c_12856,plain,
product(c,quotient(c,quotient(a,c))) = quotient(c,quotient(c,b)),
inference(superposition,[status(thm)],[c_3209,c_12308]) ).
tcf(c_12870,plain,
! [X0: $i,X1: $i] : quotient(product(X0,quotient(X0,X1)),X0) = quotient(X0,quotient(product(X0,X1),X0)),
inference(superposition,[status(thm)],[c_12308,c_6753]) ).
tcf(c_12885,plain,
product(c,quotient(c,quotient(a,c))) = product(difference(c,a),c),
inference(light_normalisation,[status(thm)],[c_12856,c_9359]) ).
tcf(c_12886,plain,
! [X0: $i,X1: $i] : quotient(product(X0,quotient(X0,X1)),X0) = quotient(X0,product(X0,quotient(X1,X0))),
inference(light_normalisation,[status(thm)],[c_12870,c_665]) ).
tcf(c_14246,plain,
! [X0: $i] : product(quotient(c,b),difference(difference(b,c),X0)) = difference(a,product(quotient(c,b),X0)),
inference(superposition,[status(thm)],[c_11713,c_2162]) ).
tcf(c_15069,plain,
product(product(c,b),a) = product(c,product(c,a)),
inference(demodulation,[status(thm)],[c_2319,c_7084]) ).
tcf(c_15085,plain,
quotient(product(c,product(c,a)),a) = product(c,b),
inference(superposition,[status(thm)],[c_15069,c_61]) ).
tcf(c_15086,plain,
difference(product(c,b),product(c,product(c,a))) = a,
inference(superposition,[status(thm)],[c_15069,c_59]) ).
tcf(c_15184,plain,
product(quotient(c,a),c) = product(c,b),
inference(demodulation,[status(thm)],[c_15085,c_2770]) ).
tcf(c_15200,plain,
quotient(product(c,b),c) = quotient(c,a),
inference(superposition,[status(thm)],[c_15184,c_61]) ).
tcf(c_15951,plain,
product(c,quotient(b,c)) = quotient(c,a),
inference(demodulation,[status(thm)],[c_15200,c_665]) ).
tcf(c_15952,plain,
difference(difference(a,c),c) = quotient(c,a),
inference(demodulation,[status(thm)],[c_5681,c_15951]) ).
tcf(c_15981,plain,
quotient(product(difference(b,c),c),quotient(c,a)) = c,
inference(superposition,[status(thm)],[c_15951,c_8866]) ).
tcf(c_16193,plain,
product(difference(a,c),quotient(c,a)) = c,
inference(superposition,[status(thm)],[c_15952,c_60]) ).
tcf(c_16525,plain,
product(c,difference(b,product(c,a))) = a,
inference(demodulation,[status(thm)],[c_15086,c_2162]) ).
tcf(c_16559,plain,
product(product(b,c),product(c,a)) = product(b,a),
inference(superposition,[status(thm)],[c_16525,c_461]) ).
tcf(c_16802,plain,
product(difference(b,c),c) = product(c,quotient(c,a)),
inference(superposition,[status(thm)],[c_15981,c_62]) ).
tcf(c_17073,plain,
quotient(product(c,quotient(c,a)),c) = difference(b,c),
inference(superposition,[status(thm)],[c_16802,c_61]) ).
tcf(c_17074,plain,
difference(difference(b,c),product(c,quotient(c,a))) = c,
inference(superposition,[status(thm)],[c_16802,c_59]) ).
tcf(c_17201,plain,
product(difference(c,a),c) = difference(b,c),
inference(demodulation,[status(thm)],[c_17073,c_12308,c_12885,c_12886]) ).
tcf(c_17202,plain,
product(difference(b,c),quotient(c,b)) = c,
inference(demodulation,[status(thm)],[c_9500,c_17201]) ).
tcf(c_17237,plain,
product(a,product(c,c)) = product(c,difference(b,c)),
inference(superposition,[status(thm)],[c_17201,c_454]) ).
tcf(c_17383,plain,
! [X0: $i] : product(quotient(c,b),difference(difference(b,c),X0)) = difference(difference(b,c),product(c,X0)),
inference(superposition,[status(thm)],[c_17202,c_1806]) ).
tcf(c_17394,plain,
difference(difference(b,c),c) = quotient(c,b),
inference(superposition,[status(thm)],[c_17202,c_59]) ).
tcf(c_17417,plain,
! [X0: $i] : difference(difference(b,c),product(c,X0)) = difference(a,product(quotient(c,b),X0)),
inference(light_normalisation,[status(thm)],[c_17383,c_14246]) ).
tcf(c_17968,plain,
product(c,product(difference(a,c),a)) = product(b,a),
inference(demodulation,[status(thm)],[c_16559,c_4062]) ).
tcf(c_17984,plain,
quotient(product(b,a),product(difference(a,c),a)) = c,
inference(superposition,[status(thm)],[c_17968,c_61]) ).
tcf(c_18207,plain,
difference(a,product(quotient(c,b),quotient(c,a))) = c,
inference(demodulation,[status(thm)],[c_17074,c_17417]) ).
tcf(c_18217,plain,
product(quotient(c,b),quotient(c,a)) = product(a,c),
inference(superposition,[status(thm)],[c_18207,c_60]) ).
tcf(c_18531,plain,
product(quotient(b,difference(a,c)),a) = c,
inference(demodulation,[status(thm)],[c_17984,c_3470]) ).
tcf(c_18547,plain,
quotient(b,difference(a,c)) = quotient(c,a),
inference(superposition,[status(thm)],[c_18531,c_61]) ).
tcf(c_18639,plain,
product(quotient(c,a),difference(a,c)) = b,
inference(superposition,[status(thm)],[c_18547,c_62]) ).
tcf(c_18803,plain,
product(quotient(c,a),product(difference(a,c),quotient(c,a))) = product(b,quotient(c,a)),
inference(superposition,[status(thm)],[c_18639,c_465]) ).
tcf(c_18827,plain,
product(b,quotient(c,a)) = product(c,b),
inference(light_normalisation,[status(thm)],[c_18803,c_15184,c_16193]) ).
tcf(c_18898,plain,
difference(b,product(c,b)) = quotient(c,a),
inference(superposition,[status(thm)],[c_18827,c_59]) ).
tcf(c_19090,plain,
product(difference(b,c),b) = quotient(c,a),
inference(demodulation,[status(thm)],[c_18898,c_1002]) ).
tcf(c_19107,plain,
difference(difference(b,c),quotient(c,a)) = b,
inference(superposition,[status(thm)],[c_19090,c_59]) ).
tcf(c_19863,plain,
difference(quotient(c,b),product(a,c)) = quotient(c,a),
inference(superposition,[status(thm)],[c_18217,c_59]) ).
tcf(c_20695,plain,
product(c,difference(b,c)) = product(a,c),
inference(demodulation,[status(thm)],[c_17237,c_64]) ).
tcf(c_20722,plain,
product(difference(difference(b,c),c),difference(b,c)) = difference(difference(b,c),product(a,c)),
inference(superposition,[status(thm)],[c_20695,c_1002]) ).
tcf(c_20736,plain,
difference(difference(b,c),product(a,c)) = a,
inference(light_normalisation,[status(thm)],[c_20722,c_11713,c_17394]) ).
tcf(c_20825,plain,
product(difference(b,c),a) = product(a,c),
inference(superposition,[status(thm)],[c_20736,c_60]) ).
tcf(c_20829,plain,
quotient(product(a,c),a) = difference(b,c),
inference(superposition,[status(thm)],[c_20736,c_151]) ).
tcf(c_20861,plain,
difference(quotient(a,difference(b,c)),product(a,c)) = difference(a,difference(b,c)),
inference(superposition,[status(thm)],[c_20825,c_6502]) ).
tcf(c_20872,plain,
difference(a,difference(b,c)) = quotient(c,a),
inference(light_normalisation,[status(thm)],[c_20861,c_11718,c_19863]) ).
tcf(c_21197,plain,
product(a,quotient(c,a)) = difference(b,c),
inference(demodulation,[status(thm)],[c_20829,c_665]) ).
tcf(c_21213,plain,
quotient(difference(b,c),quotient(c,a)) = a,
inference(superposition,[status(thm)],[c_21197,c_61]) ).
tcf(c_21417,plain,
product(a,difference(difference(b,c),quotient(c,a))) = product(quotient(c,a),difference(b,c)),
inference(superposition,[status(thm)],[c_21213,c_5482]) ).
tcf(c_21430,plain,
product(quotient(c,a),difference(b,c)) = product(a,b),
inference(light_normalisation,[status(thm)],[c_21417,c_19107]) ).
tcf(c_21614,plain,
quotient(product(quotient(c,a),difference(b,c)),product(difference(b,c),quotient(a,difference(b,c)))) = difference(b,c),
inference(superposition,[status(thm)],[c_20872,c_8866]) ).
tcf(c_21632,plain,
quotient(product(a,b),c) = difference(b,c),
inference(light_normalisation,[status(thm)],[c_21614,c_11718,c_17202,c_21430]) ).
tcf(c_21709,plain,
product(difference(b,c),c) = product(a,b),
inference(superposition,[status(thm)],[c_21632,c_62]) ).
tcf(c_21722,plain,
product(c,quotient(c,a)) = product(a,b),
inference(demodulation,[status(thm)],[c_16802,c_21709]) ).
tcf(c_22161,plain,
! [X0: $i] : product(product(a,b),product(X0,a)) = product(product(c,X0),c),
inference(superposition,[status(thm)],[c_21722,c_207]) ).
tcf(c_22179,plain,
product(product(c,x0),c) != product(c,product(x0,c)),
inference(demodulation,[status(thm)],[c_93,c_22161]) ).
tcf(c_22180,plain,
$false,
inference(ground_joinability,[status(thm)],[c_22179,c_465]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n016.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 16:06:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.42 Running UEQ theorem proving
% 0.16/0.42 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.16/0.43
% 0.16/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.43
% 0.16/0.43 % Detected problem language: tptp
% 0.16/0.44 % Proving...
% 15.72/3.16 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 15.72/3.16 % SZS status Started for theBenchmark.p
% 15.72/3.16 % SZS status Unsatisfiable for theBenchmark.p
% 15.72/3.16
% 15.72/3.16 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.72/3.16
% 15.72/3.16 % ------ iProver source info
% 15.72/3.16
% 15.72/3.16 % git: date: 2026-07-19 20:42:38 +0200
% 15.72/3.16 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.72/3.16 % git: non_committed_changes: false
% 15.72/3.16
% 15.72/3.16 % ------ Parsing...% successful
% 15.72/3.16
% 15.72/3.16
% 15.72/3.16 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.72/3.16
% 15.72/3.16 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.72/3.16
% 15.72/3.16 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.72/3.16
% 15.72/3.16 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.72/3.16 % ------ Proving...
% 15.72/3.16 % ------ Problem Properties
% 15.72/3.16
% 15.72/3.16 %
% 15.72/3.16 % clauses 9
% 15.72/3.16 % conjectures 0
% 15.72/3.16 % EPR 0
% 15.72/3.16 % Horn 9
% 15.72/3.16 % unary 9
% 15.72/3.16 % binary 0
% 15.72/3.16 % lits 9
% 15.72/3.16 % lits eq 9
% 15.72/3.16 % fd_pure 0
% 15.72/3.16 % fd_pseudo 0
% 15.72/3.16 % fd_cond 0
% 15.72/3.16 % fd_pseudo_cond 0
% 15.72/3.16 % AC symbols 0
% 15.72/3.16
% 15.72/3.16 % ------ Input Options Time Limit: Unbounded
% 15.72/3.16
% 15.72/3.16
% 15.72/3.16 % ------
% 15.72/3.16 % Current options:
% 15.72/3.16 % ------
% 15.72/3.16
% 15.72/3.16
% 15.72/3.16 %
% 15.72/3.16
% 15.72/3.16 % ------ Proving...
% 15.72/3.16 %
% 15.72/3.16
% 15.72/3.16 % SZS status Unsatisfiable for theBenchmark.p
% 15.72/3.16
% 15.72/3.16 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.72/3.16
% 15.72/3.16
%------------------------------------------------------------------------------