%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP764-1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:27:14 PM UTC 2026
% Result : Unsatisfiable 101.11s 77.93s
% Output : CNFRefutation 104.41s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_14)
% Comments :
%------------------------------------------------------------------------------
cnf(sos12,axiom,
eta(X1) = product(i(X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos12) ).
cnf(sos09,axiom,
i(X1) = difference(X1,one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos09) ).
cnf(goals,negated_conjecture,
product(x0,product(eta(x0),x1)) != product(j(j(x0)),x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
cnf(sos10,axiom,
j(X1) = quotient(one,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos10) ).
cnf(sos11,axiom,
product(i(X1),X1) = product(X1,j(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos11) ).
cnf(sos08,axiom,
difference(product(X1,X2),product(X1,product(X2,X3))) = quotient(quotient(product(X3,product(X1,X2)),X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos08) ).
cnf(sos07,axiom,
difference(X1,product(product(X1,X2),X3)) = quotient(product(X2,product(X3,X1)),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos07) ).
cnf(sos05,axiom,
quotient(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos05) ).
cnf(sos06,axiom,
product(quotient(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos06) ).
cnf(sos04,axiom,
difference(X1,product(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos04) ).
cnf(sos03,axiom,
product(X1,difference(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos03) ).
cnf(sos02,axiom,
product(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos02) ).
cnf(sos01,axiom,
product(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos01) ).
cnf(i_0_13,axiom,
eta(X1) = product(i(X1),X1),
sos12 ).
cnf(i_0_14,axiom,
i(X1) = difference(X1,one),
sos09 ).
cnf(i_0_15,negated_conjecture,
product(x0,product(eta(x0),x1)) != product(j(j(x0)),x1),
goals ).
cnf(i_0_16,axiom,
j(X1) = quotient(one,X1),
sos10 ).
cnf(i_0_17,plain,
eta(X1) = product(difference(X1,one),X1),
inference(rw,[status(thm)],[i_0_13,c_0_14]) ).
cnf(i_0_18,axiom,
product(i(X1),X1) = product(X1,j(X1)),
sos11 ).
cnf(i_0_19,negated_conjecture,
product(x0,product(product(difference(x0,one),x0),x1)) != product(quotient(one,quotient(one,x0)),x1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_15,c_0_16]),c_0_16]),c_0_17]),
[final] ).
cnf(i_0_20,axiom,
difference(product(X1,X2),product(X1,product(X2,X3))) = quotient(quotient(product(X3,product(X1,X2)),X2),X1),
sos08,
[final] ).
cnf(i_0_21,axiom,
difference(X1,product(product(X1,X2),X3)) = quotient(product(X2,product(X3,X1)),X1),
sos07,
[final] ).
cnf(i_0_22,plain,
product(difference(X1,one),X1) = product(X1,quotient(one,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_18,c_0_14]),c_0_16]),
[final] ).
cnf(i_0_23,axiom,
quotient(product(X1,X2),X2) = X1,
sos05,
[final] ).
cnf(i_0_24,axiom,
product(quotient(X1,X2),X2) = X1,
sos06,
[final] ).
cnf(i_0_25,axiom,
difference(X1,product(X1,X2)) = X2,
sos04,
[final] ).
cnf(i_0_26,axiom,
product(X1,difference(X1,X2)) = X2,
sos03,
[final] ).
cnf(i_0_27,axiom,
product(one,X1) = X1,
sos02,
[final] ).
cnf(i_0_28,axiom,
product(X1,one) = X1,
sos01,
[final] ).
cnf(i_0_29,axiom,
X1 = X1 ).
cnf(i_0_30,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_31,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_32,axiom,
( X1 != X2
| product(X1,X3) = product(X2,X3) ) ).
cnf(i_0_33,axiom,
( X1 != X2
| product(X3,X1) = product(X3,X2) ) ).
cnf(i_0_34,axiom,
( X1 != X2
| difference(X1,X3) = difference(X2,X3) ) ).
cnf(i_0_35,axiom,
( X1 != X2
| difference(X3,X1) = difference(X3,X2) ) ).
cnf(i_0_36,axiom,
( X1 != X2
| quotient(X1,X3) = quotient(X2,X3) ) ).
cnf(i_0_37,axiom,
( X1 != X2
| quotient(X3,X1) = quotient(X3,X2) ) ).
cnf(i_0_444,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = quotient(product(X2,X4),X4),
inference(scs_inference,[],[i_0_25,i_0_183,i_0_31]) ).
cnf(i_0_446,plain,
quotient(product(X1,X2),X2) = difference(X3,product(X3,product(quotient(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_183,i_0_31,i_0_30]) ).
cnf(i_0_453,plain,
difference(X1,product(X1,product(X2,one))) = quotient(product(X2,X3),X3),
inference(scs_inference,[],[i_0_25,i_0_169,i_0_31]) ).
cnf(i_0_455,plain,
quotient(product(X1,X2),X2) = difference(X3,product(X3,product(X1,one))),
inference(scs_inference,[],[i_0_25,i_0_169,i_0_31,i_0_30]) ).
cnf(i_0_459,plain,
difference(X1,product(X1,product(one,X2))) = quotient(product(X2,X3),X3),
inference(scs_inference,[],[i_0_25,i_0_195,i_0_31]) ).
cnf(i_0_461,plain,
quotient(product(X1,X2),X2) = difference(X3,product(X3,product(one,X1))),
inference(scs_inference,[],[i_0_25,i_0_195,i_0_31,i_0_30]) ).
cnf(i_0_468,plain,
difference(X1,product(X1,product(X2,quotient(one,X2)))) = product(one,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_25,i_0_41,i_0_31]) ).
cnf(i_0_470,plain,
product(one,product(difference(X1,one),X1)) = difference(X2,product(X2,product(X1,quotient(one,X1)))),
inference(scs_inference,[],[i_0_25,i_0_41,i_0_31,i_0_30]) ).
cnf(i_0_474,plain,
difference(X1,product(X1,product(X2,difference(X2,X3)))) = difference(X4,product(X4,X3)),
inference(scs_inference,[],[i_0_25,i_0_473,i_0_31]) ).
cnf(i_0_476,plain,
difference(X1,product(X1,X2)) = difference(X3,product(X3,product(X4,difference(X4,X2)))),
inference(scs_inference,[],[i_0_25,i_0_473,i_0_31,i_0_30]) ).
cnf(i_0_480,plain,
difference(X1,product(X1,product(X2,one))) = difference(X3,product(X3,X2)),
inference(scs_inference,[],[i_0_25,i_0_479,i_0_31]) ).
cnf(i_0_482,plain,
difference(X1,product(X1,X2)) = difference(X3,product(X3,product(X2,one))),
inference(scs_inference,[],[i_0_25,i_0_479,i_0_31,i_0_30]) ).
cnf(i_0_494,plain,
difference(X1,product(X1,product(one,X2))) = difference(X3,product(X3,X2)),
inference(scs_inference,[],[i_0_25,i_0_493,i_0_31]) ).
cnf(i_0_496,plain,
difference(X1,product(X1,X2)) = difference(X3,product(X3,product(one,X2))),
inference(scs_inference,[],[i_0_25,i_0_493,i_0_31,i_0_30]) ).
cnf(i_0_500,plain,
difference(X1,product(X1,difference(X2,product(X2,X3)))) = product(X4,difference(X4,X3)),
inference(scs_inference,[],[i_0_25,i_0_471,i_0_31]) ).
cnf(i_0_502,plain,
product(X1,difference(X1,X2)) = difference(X3,product(X3,difference(X4,product(X4,X2)))),
inference(scs_inference,[],[i_0_25,i_0_471,i_0_31,i_0_30]) ).
cnf(i_0_503,plain,
difference(X1,product(X1,difference(X2,product(X2,X3)))) = product(X3,one),
inference(scs_inference,[],[i_0_25,i_0_477,i_0_31]) ).
cnf(i_0_505,plain,
product(X1,one) = difference(X2,product(X2,difference(X3,product(X3,X1)))),
inference(scs_inference,[],[i_0_25,i_0_477,i_0_31,i_0_30]) ).
cnf(i_0_506,plain,
difference(X1,product(X1,difference(X2,product(X2,X3)))) = product(one,X3),
inference(scs_inference,[],[i_0_25,i_0_491,i_0_31]) ).
cnf(i_0_508,plain,
product(one,X1) = difference(X2,product(X2,difference(X3,product(X3,X1)))),
inference(scs_inference,[],[i_0_25,i_0_491,i_0_31,i_0_30]) ).
cnf(i_0_509,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = product(X4,difference(X4,X2)),
inference(scs_inference,[],[i_0_25,i_0_292,i_0_31]) ).
cnf(i_0_511,plain,
product(X1,difference(X1,X2)) = difference(X3,product(X3,product(quotient(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_292,i_0_31,i_0_30]) ).
cnf(i_0_512,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = difference(X4,product(X4,X2)),
inference(scs_inference,[],[i_0_25,i_0_312,i_0_31]) ).
cnf(i_0_514,plain,
difference(X1,product(X1,X2)) = difference(X3,product(X3,product(quotient(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_312,i_0_31,i_0_30]) ).
cnf(i_0_515,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = product(X2,one),
inference(scs_inference,[],[i_0_25,i_0_298,i_0_31]) ).
cnf(i_0_517,plain,
product(X1,one) = difference(X2,product(X2,product(quotient(X1,X3),X3))),
inference(scs_inference,[],[i_0_25,i_0_298,i_0_31,i_0_30]) ).
cnf(i_0_518,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = product(one,X2),
inference(scs_inference,[],[i_0_25,i_0_318,i_0_31]) ).
cnf(i_0_520,plain,
product(one,X1) = difference(X2,product(X2,product(quotient(X1,X3),X3))),
inference(scs_inference,[],[i_0_25,i_0_318,i_0_31,i_0_30]) ).
cnf(i_0_524,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(X4,difference(X4,X2)),
inference(scs_inference,[],[i_0_25,i_0_161,i_0_31]) ).
cnf(i_0_526,plain,
product(X1,difference(X1,X2)) = difference(X3,product(X3,quotient(product(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_161,i_0_31,i_0_30]) ).
cnf(i_0_527,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(quotient(X2,X4),X4),
inference(scs_inference,[],[i_0_25,i_0_181,i_0_31]) ).
cnf(i_0_529,plain,
product(quotient(X1,X2),X2) = difference(X3,product(X3,quotient(product(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_181,i_0_31,i_0_30]) ).
cnf(i_0_530,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = difference(X4,product(X4,X2)),
inference(scs_inference,[],[i_0_25,i_0_187,i_0_31]) ).
cnf(i_0_532,plain,
difference(X1,product(X1,X2)) = difference(X3,product(X3,quotient(product(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_187,i_0_31,i_0_30]) ).
cnf(i_0_536,plain,
difference(X1,product(X1,X2)) = product(quotient(difference(X3,product(X3,X2)),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_107,i_0_31]) ).
cnf(i_0_537,plain,
X1 = product(quotient(difference(X2,product(X2,X1)),X3),X3),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_538,plain,
product(quotient(difference(X1,product(X1,X2)),X3),X3) = difference(X4,product(X4,X2)),
inference(scs_inference,[],[i_0_25,i_0_107,i_0_31,i_0_30]) ).
cnf(i_0_539,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(X2,one),
inference(scs_inference,[],[i_0_25,i_0_167,i_0_31]) ).
cnf(i_0_541,plain,
product(X1,one) = difference(X2,product(X2,quotient(product(X1,X3),X3))),
inference(scs_inference,[],[i_0_25,i_0_167,i_0_31,i_0_30]) ).
cnf(i_0_542,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(one,X2),
inference(scs_inference,[],[i_0_25,i_0_193,i_0_31]) ).
cnf(i_0_544,plain,
product(one,X1) = difference(X2,product(X2,quotient(product(X1,X3),X3))),
inference(scs_inference,[],[i_0_25,i_0_193,i_0_31,i_0_30]) ).
cnf(i_0_551,plain,
difference(X1,product(X1,product(difference(X2,one),X2))) = product(product(X2,quotient(one,X2)),one),
inference(scs_inference,[],[i_0_25,i_0_128,i_0_31]) ).
cnf(i_0_553,plain,
product(product(X1,quotient(one,X1)),one) = difference(X2,product(X2,product(difference(X1,one),X1))),
inference(scs_inference,[],[i_0_25,i_0_128,i_0_31,i_0_30]) ).
cnf(i_0_554,plain,
difference(X1,product(X1,product(difference(X2,one),X2))) = product(one,product(X2,quotient(one,X2))),
inference(scs_inference,[],[i_0_25,i_0_143,i_0_31]) ).
cnf(i_0_556,plain,
product(one,product(X1,quotient(one,X1))) = difference(X2,product(X2,product(difference(X1,one),X1))),
inference(scs_inference,[],[i_0_25,i_0_143,i_0_31,i_0_30]) ).
cnf(i_0_569,plain,
difference(X1,product(X1,X2)) = product(one,quotient(product(X2,X3),X3)),
inference(scs_inference,[],[i_0_25,i_0_99,i_0_31]) ).
cnf(i_0_570,plain,
X1 = product(one,quotient(product(X1,X2),X2)),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_571,plain,
product(one,quotient(product(X1,X2),X2)) = difference(X3,product(X3,X1)),
inference(scs_inference,[],[i_0_25,i_0_99,i_0_31,i_0_30]) ).
cnf(i_0_593,plain,
product(X1,difference(X1,product(X2,difference(X2,X3)))) = product(quotient(X3,X4),X4),
inference(scs_inference,[],[i_0_26,i_0_294,i_0_31]) ).
cnf(i_0_595,plain,
product(quotient(X1,X2),X2) = product(X3,difference(X3,product(X4,difference(X4,X1)))),
inference(scs_inference,[],[i_0_26,i_0_294,i_0_31,i_0_30]) ).
cnf(i_0_596,plain,
product(X1,difference(X1,product(X2,difference(X2,X3)))) = difference(X4,product(X4,X3)),
inference(scs_inference,[],[i_0_26,i_0_473,i_0_31]) ).
cnf(i_0_598,plain,
difference(X1,product(X1,X2)) = product(X3,difference(X3,product(X4,difference(X4,X2)))),
inference(scs_inference,[],[i_0_26,i_0_473,i_0_31,i_0_30]) ).
cnf(i_0_617,plain,
product(X1,difference(X1,product(X2,one))) = difference(X3,product(X3,X2)),
inference(scs_inference,[],[i_0_26,i_0_479,i_0_31]) ).
cnf(i_0_619,plain,
difference(X1,product(X1,X2)) = product(X3,difference(X3,product(X2,one))),
inference(scs_inference,[],[i_0_26,i_0_479,i_0_31,i_0_30]) ).
cnf(i_0_623,plain,
product(X1,difference(X1,product(one,X2))) = difference(X3,product(X3,X2)),
inference(scs_inference,[],[i_0_26,i_0_493,i_0_31]) ).
cnf(i_0_625,plain,
difference(X1,product(X1,X2)) = product(X3,difference(X3,product(one,X2))),
inference(scs_inference,[],[i_0_26,i_0_493,i_0_31,i_0_30]) ).
cnf(i_0_641,plain,
product(X1,difference(X1,product(X2,difference(X2,X3)))) = quotient(product(X3,X4),X4),
inference(scs_inference,[],[i_0_26,i_0_163,i_0_31]) ).
cnf(i_0_643,plain,
quotient(product(X1,X2),X2) = product(X3,difference(X3,product(X4,difference(X4,X1)))),
inference(scs_inference,[],[i_0_26,i_0_163,i_0_31,i_0_30]) ).
cnf(i_0_644,plain,
product(X1,difference(X1,difference(X2,product(X2,X3)))) = quotient(product(X3,X4),X4),
inference(scs_inference,[],[i_0_26,i_0_189,i_0_31]) ).
cnf(i_0_646,plain,
quotient(product(X1,X2),X2) = product(X3,difference(X3,difference(X4,product(X4,X1)))),
inference(scs_inference,[],[i_0_26,i_0_189,i_0_31,i_0_30]) ).
cnf(i_0_647,plain,
product(X1,difference(X1,difference(X2,product(X2,X3)))) = product(quotient(X3,X4),X4),
inference(scs_inference,[],[i_0_26,i_0_314,i_0_31]) ).
cnf(i_0_649,plain,
product(quotient(X1,X2),X2) = product(X3,difference(X3,difference(X4,product(X4,X1)))),
inference(scs_inference,[],[i_0_26,i_0_314,i_0_31,i_0_30]) ).
cnf(i_0_662,plain,
product(X1,difference(X1,product(X2,one))) = product(quotient(X2,X3),X3),
inference(scs_inference,[],[i_0_26,i_0_300,i_0_31]) ).
cnf(i_0_664,plain,
product(quotient(X1,X2),X2) = product(X3,difference(X3,product(X1,one))),
inference(scs_inference,[],[i_0_26,i_0_300,i_0_31,i_0_30]) ).
cnf(i_0_668,plain,
product(X1,difference(X1,product(one,X2))) = product(quotient(X2,X3),X3),
inference(scs_inference,[],[i_0_26,i_0_320,i_0_31]) ).
cnf(i_0_670,plain,
product(quotient(X1,X2),X2) = product(X3,difference(X3,product(one,X1))),
inference(scs_inference,[],[i_0_26,i_0_320,i_0_31,i_0_30]) ).
cnf(i_0_686,plain,
product(X1,difference(X1,product(quotient(X2,X3),X3))) = quotient(product(X2,X4),X4),
inference(scs_inference,[],[i_0_26,i_0_183,i_0_31]) ).
cnf(i_0_688,plain,
quotient(product(X1,X2),X2) = product(X3,difference(X3,product(quotient(X1,X4),X4))),
inference(scs_inference,[],[i_0_26,i_0_183,i_0_31,i_0_30]) ).
cnf(i_0_695,plain,
product(X1,difference(X1,product(X2,one))) = quotient(product(X2,X3),X3),
inference(scs_inference,[],[i_0_26,i_0_169,i_0_31]) ).
cnf(i_0_697,plain,
quotient(product(X1,X2),X2) = product(X3,difference(X3,product(X1,one))),
inference(scs_inference,[],[i_0_26,i_0_169,i_0_31,i_0_30]) ).
cnf(i_0_701,plain,
product(X1,difference(X1,product(one,X2))) = quotient(product(X2,X3),X3),
inference(scs_inference,[],[i_0_26,i_0_195,i_0_31]) ).
cnf(i_0_703,plain,
quotient(product(X1,X2),X2) = product(X3,difference(X3,product(one,X1))),
inference(scs_inference,[],[i_0_26,i_0_195,i_0_31,i_0_30]) ).
cnf(i_0_710,plain,
product(X1,difference(X1,product(X2,quotient(one,X2)))) = product(one,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_26,i_0_41,i_0_31]) ).
cnf(i_0_712,plain,
product(one,product(difference(X1,one),X1)) = product(X2,difference(X2,product(X1,quotient(one,X1)))),
inference(scs_inference,[],[i_0_26,i_0_41,i_0_31,i_0_30]) ).
cnf(i_0_718,plain,
product(X1,difference(X1,product(X2,one))) = product(X3,difference(X3,X2)),
inference(scs_inference,[],[i_0_26,i_0_717,i_0_31]) ).
cnf(i_0_720,plain,
product(X1,difference(X1,X2)) = product(X3,difference(X3,product(X2,one))),
inference(scs_inference,[],[i_0_26,i_0_717,i_0_31,i_0_30]) ).
cnf(i_0_730,plain,
product(X1,difference(X1,product(one,X2))) = product(X3,difference(X3,X2)),
inference(scs_inference,[],[i_0_26,i_0_729,i_0_31]) ).
cnf(i_0_732,plain,
product(X1,difference(X1,X2)) = product(X3,difference(X3,product(one,X2))),
inference(scs_inference,[],[i_0_26,i_0_729,i_0_31,i_0_30]) ).
cnf(i_0_736,plain,
product(product(X1,difference(X1,X2)),X3) = product(product(X2,one),X3),
inference(scs_inference,[],[i_0_715,i_0_32]) ).
cnf(i_0_737,plain,
difference(product(X1,difference(X1,X2)),X3) = difference(product(X2,one),X3),
inference(scs_inference,[],[i_0_715,i_0_32,i_0_34]) ).
cnf(i_0_738,plain,
difference(X1,product(X2,difference(X2,X3))) = difference(X1,product(X3,one)),
inference(scs_inference,[],[i_0_715,i_0_32,i_0_34,i_0_35]) ).
cnf(i_0_739,plain,
quotient(product(X1,difference(X1,X2)),X3) = quotient(product(X2,one),X3),
inference(scs_inference,[],[i_0_715,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_740,plain,
quotient(X1,product(X2,difference(X2,X3))) = quotient(X1,product(X3,one)),
inference(scs_inference,[],[i_0_715,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_741,plain,
product(X1,product(X2,difference(X2,X3))) = product(X1,product(X3,one)),
inference(scs_inference,[],[i_0_715,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_742,plain,
product(quotient(one,quotient(one,X1)),X2) != product(X1,product(product(difference(X1,one),X1),X2)),
inference(scs_inference,[],[i_0_19,i_0_715,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33,i_0_30]) ).
cnf(i_0_743,plain,
product(X1,difference(X1,quotient(X2,one))) = product(quotient(X2,X3),X3),
inference(scs_inference,[],[i_0_19,i_0_715,i_0_310,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33,i_0_30,i_0_31]) ).
cnf(i_0_744,plain,
product(X1,difference(X1,X2)) = product(X2,one),
inference(rename_variables,[],[i_0_715]) ).
cnf(i_0_745,plain,
product(quotient(X1,X2),X2) = product(quotient(X1,X3),X3),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_746,plain,
product(product(X1,difference(X1,X2)),X3) = product(product(one,X2),X3),
inference(scs_inference,[],[i_0_727,i_0_32]) ).
cnf(i_0_747,plain,
difference(product(X1,difference(X1,X2)),X3) = difference(product(one,X2),X3),
inference(scs_inference,[],[i_0_727,i_0_32,i_0_34]) ).
cnf(i_0_748,plain,
difference(X1,product(X2,difference(X2,X3))) = difference(X1,product(one,X3)),
inference(scs_inference,[],[i_0_727,i_0_32,i_0_34,i_0_35]) ).
cnf(i_0_749,plain,
quotient(product(X1,difference(X1,X2)),X3) = quotient(product(one,X2),X3),
inference(scs_inference,[],[i_0_727,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_750,plain,
quotient(X1,product(X2,difference(X2,X3))) = quotient(X1,product(one,X3)),
inference(scs_inference,[],[i_0_727,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_751,plain,
product(X1,product(X2,difference(X2,X3))) = product(X1,product(one,X3)),
inference(scs_inference,[],[i_0_727,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_753,plain,
product(quotient(product(X1,X2),X2),X3) = product(quotient(product(X1,X4),X4),X3),
inference(scs_inference,[],[i_0_179,i_0_32]) ).
cnf(i_0_754,plain,
difference(quotient(product(X1,X2),X2),X3) = difference(quotient(product(X1,X4),X4),X3),
inference(scs_inference,[],[i_0_179,i_0_32,i_0_34]) ).
cnf(i_0_755,plain,
difference(X1,quotient(product(X2,X3),X3)) = difference(X1,quotient(product(X2,X4),X4)),
inference(scs_inference,[],[i_0_179,i_0_32,i_0_34,i_0_35]) ).
cnf(i_0_756,plain,
quotient(quotient(product(X1,X2),X2),X3) = quotient(quotient(product(X1,X4),X4),X3),
inference(scs_inference,[],[i_0_179,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_757,plain,
quotient(X1,quotient(product(X2,X3),X3)) = quotient(X1,quotient(product(X2,X4),X4)),
inference(scs_inference,[],[i_0_179,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_758,plain,
product(X1,quotient(product(X2,X3),X3)) = product(X1,quotient(product(X2,X4),X4)),
inference(scs_inference,[],[i_0_179,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_760,plain,
product(difference(X1,product(X1,X2)),X3) = product(difference(X4,product(X4,X2)),X3),
inference(scs_inference,[],[i_0_489,i_0_32]) ).
cnf(i_0_761,plain,
difference(difference(X1,product(X1,X2)),X3) = difference(difference(X4,product(X4,X2)),X3),
inference(scs_inference,[],[i_0_489,i_0_32,i_0_34]) ).
cnf(i_0_762,plain,
difference(X1,difference(X2,product(X2,X3))) = difference(X1,difference(X4,product(X4,X3))),
inference(scs_inference,[],[i_0_489,i_0_32,i_0_34,i_0_35]) ).
cnf(i_0_763,plain,
quotient(difference(X1,product(X1,X2)),X3) = quotient(difference(X4,product(X4,X2)),X3),
inference(scs_inference,[],[i_0_489,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_764,plain,
quotient(X1,difference(X2,product(X2,X3))) = quotient(X1,difference(X4,product(X4,X3))),
inference(scs_inference,[],[i_0_489,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_765,plain,
product(X1,difference(X2,product(X2,X3))) = product(X1,difference(X4,product(X4,X3))),
inference(scs_inference,[],[i_0_489,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_766,plain,
product(product(X1,difference(X1,X2)),X3) = product(product(X4,difference(X4,X2)),X3),
inference(scs_inference,[],[i_0_713,i_0_32]) ).
cnf(i_0_767,plain,
difference(product(X1,difference(X1,X2)),X3) = difference(product(X4,difference(X4,X2)),X3),
inference(scs_inference,[],[i_0_713,i_0_32,i_0_34]) ).
cnf(i_0_768,plain,
difference(X1,product(X2,difference(X2,X3))) = difference(X1,product(X4,difference(X4,X3))),
inference(scs_inference,[],[i_0_713,i_0_32,i_0_34,i_0_35]) ).
cnf(i_0_769,plain,
quotient(product(X1,difference(X1,X2)),X3) = quotient(product(X4,difference(X4,X2)),X3),
inference(scs_inference,[],[i_0_713,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_770,plain,
quotient(X1,product(X2,difference(X2,X3))) = quotient(X1,product(X4,difference(X4,X3))),
inference(scs_inference,[],[i_0_713,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_771,plain,
product(X1,product(X2,difference(X2,X3))) = product(X1,product(X4,difference(X4,X3))),
inference(scs_inference,[],[i_0_713,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_1002,plain,
product(product(product(X1,quotient(one,X1)),one),X2) = product(product(difference(X1,one),X1),X2),
inference(scs_inference,[],[i_0_130,i_0_32]) ).
cnf(i_0_1005,plain,
quotient(product(product(X1,quotient(one,X1)),one),X2) = quotient(product(difference(X1,one),X1),X2),
inference(scs_inference,[],[i_0_130,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_1006,plain,
quotient(X1,product(product(X2,quotient(one,X2)),one)) = quotient(X1,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_130,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_1007,plain,
product(X1,product(product(X2,quotient(one,X2)),one)) = product(X1,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_130,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_1009,plain,
product(product(X1,quotient(one,X1)),one) = product(difference(X1,one),X1),
inference(rename_variables,[],[i_0_130]) ).
cnf(i_0_1011,plain,
product(product(one,product(X1,quotient(one,X1))),X2) = product(product(difference(X1,one),X1),X2),
inference(scs_inference,[],[i_0_145,i_0_32]) ).
cnf(i_0_1014,plain,
quotient(product(one,product(X1,quotient(one,X1))),X2) = quotient(product(difference(X1,one),X1),X2),
inference(scs_inference,[],[i_0_145,i_0_32,i_0_34,i_0_35,i_0_36]) ).
cnf(i_0_1015,plain,
quotient(X1,product(one,product(X2,quotient(one,X2)))) = quotient(X1,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_145,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37]) ).
cnf(i_0_1016,plain,
product(X1,product(one,product(X2,quotient(one,X2)))) = product(X1,product(difference(X2,one),X2)),
inference(scs_inference,[],[i_0_145,i_0_32,i_0_34,i_0_35,i_0_36,i_0_37,i_0_33]) ).
cnf(i_0_1417,plain,
X1 = product(quotient(difference(X2,product(X2,X1)),X3),X3),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_1494,plain,
X1 = product(one,quotient(product(X1,X2),X2)),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_1977,plain,
product(X1,difference(X1,product(X2,quotient(one,X2)))) = product(difference(X2,one),X2),
inference(rename_variables,[],[i_0_127]) ).
cnf(i_0_1996,plain,
product(one,X1) = product(X2,difference(X2,X1)),
inference(rename_variables,[],[i_0_729]) ).
cnf(i_0_2009,plain,
quotient(product(product(X1,quotient(one,X1)),X2),X2) = product(difference(X1,one),X1),
inference(rename_variables,[],[i_0_136]) ).
cnf(i_0_48,plain,
product(one,product(difference(one,one),one)) = quotient(one,one),
inference(scs_inference,[],[i_0_45,i_0_30]) ).
cnf(i_0_49,plain,
product(one,product(X1,quotient(one,X1))) = product(one,product(one,product(difference(X1,one),X1))),
inference(scs_inference,[],[i_0_44,i_0_38,i_0_45,i_0_30,i_0_31]) ).
cnf(i_0_104,plain,
quotient(product(product(quotient(X1,X2),X2),X3),X3) = X1,
inference(scs_inference,[],[i_0_102,i_0_30]) ).
cnf(i_0_112,plain,
difference(X1,product(X1,product(X2,difference(X2,X3)))) = X3,
inference(scs_inference,[],[i_0_110,i_0_30]) ).
cnf(i_0_173,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = quotient(product(product(X1,one),X4),X4),
inference(scs_inference,[],[i_0_23,i_0_172,i_0_31]) ).
cnf(i_0_175,plain,
quotient(product(product(X1,one),X2),X2) = quotient(product(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_23,i_0_172,i_0_31,i_0_30]) ).
cnf(i_0_199,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = quotient(product(product(one,X1),X4),X4),
inference(scs_inference,[],[i_0_23,i_0_198,i_0_31]) ).
cnf(i_0_201,plain,
quotient(product(product(one,X1),X2),X2) = quotient(product(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_23,i_0_198,i_0_31,i_0_30]) ).
cnf(i_0_229,plain,
quotient(product(X1,X2),X2) = difference(X3,product(X3,product(X4,difference(X4,X1)))),
inference(scs_inference,[],[i_0_23,i_0_110,i_0_31]) ).
cnf(i_0_230,plain,
X1 = difference(X2,product(X2,product(X3,difference(X3,X1)))),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_231,plain,
difference(X1,product(X1,product(X2,difference(X2,X3)))) = quotient(product(X3,X4),X4),
inference(scs_inference,[],[i_0_23,i_0_110,i_0_31,i_0_30]) ).
cnf(i_0_235,plain,
quotient(product(quotient(one,one),X1),X1) = product(one,product(difference(one,one),one)),
inference(scs_inference,[],[i_0_23,i_0_45,i_0_31]) ).
cnf(i_0_237,plain,
product(one,product(difference(one,one),one)) = quotient(product(quotient(one,one),X1),X1),
inference(scs_inference,[],[i_0_23,i_0_45,i_0_31,i_0_30]) ).
cnf(i_0_247,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = product(one,quotient(product(X1,X4),X4)),
inference(scs_inference,[],[i_0_23,i_0_244,i_0_31]) ).
cnf(i_0_249,plain,
product(one,quotient(product(X1,X2),X2)) = quotient(product(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_23,i_0_244,i_0_31,i_0_30]) ).
cnf(i_0_250,plain,
product(quotient(product(X1,one),X2),X2) = quotient(product(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_213,i_0_31]) ).
cnf(i_0_252,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = product(quotient(product(X1,one),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_213,i_0_31,i_0_30]) ).
cnf(i_0_253,plain,
product(quotient(product(one,X1),X2),X2) = quotient(product(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_216,i_0_31]) ).
cnf(i_0_255,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = product(quotient(product(one,X1),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_216,i_0_31,i_0_30]) ).
cnf(i_0_268,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = quotient(product(product(X1,one),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_172,i_0_31]) ).
cnf(i_0_270,plain,
quotient(product(product(X1,one),X2),X2) = product(quotient(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_172,i_0_31,i_0_30]) ).
cnf(i_0_271,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = quotient(product(product(one,X1),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_198,i_0_31]) ).
cnf(i_0_273,plain,
quotient(product(product(one,X1),X2),X2) = product(quotient(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_198,i_0_31,i_0_30]) ).
cnf(i_0_277,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = product(quotient(product(X1,one),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_276,i_0_31]) ).
cnf(i_0_279,plain,
product(quotient(product(X1,one),X2),X2) = product(quotient(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_276,i_0_31,i_0_30]) ).
cnf(i_0_283,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = product(quotient(product(one,X1),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_282,i_0_31]) ).
cnf(i_0_285,plain,
product(quotient(product(one,X1),X2),X2) = product(quotient(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_282,i_0_31,i_0_30]) ).
cnf(i_0_304,plain,
product(quotient(product(quotient(X1,X2),X2),X3),X3) = product(quotient(product(X1,one),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_303,i_0_31]) ).
cnf(i_0_306,plain,
product(quotient(product(X1,one),X2),X2) = product(quotient(product(quotient(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_303,i_0_31,i_0_30]) ).
cnf(i_0_324,plain,
product(quotient(product(quotient(X1,X2),X2),X3),X3) = product(quotient(product(one,X1),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_323,i_0_31]) ).
cnf(i_0_326,plain,
product(quotient(product(one,X1),X2),X2) = product(quotient(product(quotient(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_323,i_0_31,i_0_30]) ).
cnf(i_0_348,plain,
product(quotient(X1,X2),X2) = quotient(product(product(quotient(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_102,i_0_31]) ).
cnf(i_0_349,plain,
X1 = quotient(product(product(quotient(X1,X2),X2),X3),X3),
inference(rename_variables,[],[i_0_102]) ).
cnf(i_0_350,plain,
quotient(product(product(quotient(X1,X2),X2),X3),X3) = product(quotient(X1,X4),X4),
inference(scs_inference,[],[i_0_24,i_0_102,i_0_31,i_0_30]) ).
cnf(i_0_357,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = product(one,quotient(product(X1,X4),X4)),
inference(scs_inference,[],[i_0_24,i_0_244,i_0_31]) ).
cnf(i_0_359,plain,
product(one,quotient(product(X1,X2),X2)) = product(quotient(quotient(product(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_244,i_0_31,i_0_30]) ).
cnf(i_0_372,plain,
product(quotient(quotient(one,one),X1),X1) = product(one,product(difference(one,one),one)),
inference(scs_inference,[],[i_0_24,i_0_45,i_0_31]) ).
cnf(i_0_374,plain,
product(one,product(difference(one,one),one)) = product(quotient(quotient(one,one),X1),X1),
inference(scs_inference,[],[i_0_24,i_0_45,i_0_31,i_0_30]) ).
cnf(i_0_381,plain,
product(quotient(X1,X2),X2) = difference(X3,product(X3,product(X4,difference(X4,X1)))),
inference(scs_inference,[],[i_0_24,i_0_110,i_0_31]) ).
cnf(i_0_382,plain,
X1 = difference(X2,product(X2,product(X3,difference(X3,X1)))),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_383,plain,
difference(X1,product(X1,product(X2,difference(X2,X3)))) = product(quotient(X3,X4),X4),
inference(scs_inference,[],[i_0_24,i_0_110,i_0_31,i_0_30]) ).
cnf(i_0_387,plain,
product(quotient(product(quotient(X1,X2),X2),X3),X3) = product(one,quotient(product(X1,X4),X4)),
inference(scs_inference,[],[i_0_24,i_0_384,i_0_31]) ).
cnf(i_0_389,plain,
product(one,quotient(product(X1,X2),X2)) = product(quotient(product(quotient(X1,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_24,i_0_384,i_0_31,i_0_30]) ).
cnf(i_0_390,plain,
difference(X1,product(X1,product(X2,one))) = product(quotient(product(quotient(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_335,i_0_31]) ).
cnf(i_0_392,plain,
product(quotient(product(quotient(X1,X2),X2),X3),X3) = difference(X4,product(X4,product(X1,one))),
inference(scs_inference,[],[i_0_25,i_0_335,i_0_31,i_0_30]) ).
cnf(i_0_393,plain,
difference(X1,product(X1,product(one,X2))) = product(quotient(product(quotient(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_338,i_0_31]) ).
cnf(i_0_395,plain,
product(quotient(product(quotient(X1,X2),X2),X3),X3) = difference(X4,product(X4,product(one,X1))),
inference(scs_inference,[],[i_0_25,i_0_338,i_0_31,i_0_30]) ).
cnf(i_0_396,plain,
difference(X1,product(X1,product(X2,one))) = product(quotient(quotient(product(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_353,i_0_31]) ).
cnf(i_0_398,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = difference(X4,product(X4,product(X1,one))),
inference(scs_inference,[],[i_0_25,i_0_353,i_0_31,i_0_30]) ).
cnf(i_0_399,plain,
difference(X1,product(X1,product(one,X2))) = product(quotient(quotient(product(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_356,i_0_31]) ).
cnf(i_0_401,plain,
product(quotient(quotient(product(X1,X2),X2),X3),X3) = difference(X4,product(X4,product(one,X1))),
inference(scs_inference,[],[i_0_25,i_0_356,i_0_31,i_0_30]) ).
cnf(i_0_408,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(quotient(product(X2,one),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_276,i_0_31]) ).
cnf(i_0_410,plain,
product(quotient(product(X1,one),X2),X2) = difference(X3,product(X3,quotient(product(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_276,i_0_31,i_0_30]) ).
cnf(i_0_411,plain,
difference(X1,product(X1,quotient(product(X2,X3),X3))) = product(quotient(product(one,X2),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_282,i_0_31]) ).
cnf(i_0_413,plain,
product(quotient(product(one,X1),X2),X2) = difference(X3,product(X3,quotient(product(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_282,i_0_31,i_0_30]) ).
cnf(i_0_414,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = product(quotient(product(X2,one),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_303,i_0_31]) ).
cnf(i_0_416,plain,
product(quotient(product(X1,one),X2),X2) = difference(X3,product(X3,product(quotient(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_303,i_0_31,i_0_30]) ).
cnf(i_0_417,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = product(quotient(product(one,X2),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_323,i_0_31]) ).
cnf(i_0_419,plain,
product(quotient(product(one,X1),X2),X2) = difference(X3,product(X3,product(quotient(X1,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_323,i_0_31,i_0_30]) ).
cnf(i_0_423,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = difference(X4,product(X4,product(X2,one))),
inference(scs_inference,[],[i_0_25,i_0_422,i_0_31]) ).
cnf(i_0_425,plain,
difference(X1,product(X1,product(X2,one))) = difference(X3,product(X3,product(quotient(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_422,i_0_31,i_0_30]) ).
cnf(i_0_429,plain,
difference(X1,product(X1,product(quotient(X2,X3),X3))) = difference(X4,product(X4,product(one,X2))),
inference(scs_inference,[],[i_0_25,i_0_428,i_0_31]) ).
cnf(i_0_431,plain,
difference(X1,product(X1,product(one,X2))) = difference(X3,product(X3,product(quotient(X2,X4),X4))),
inference(scs_inference,[],[i_0_25,i_0_428,i_0_31,i_0_30]) ).
cnf(i_0_432,plain,
difference(X1,product(X1,product(X2,one))) = quotient(product(quotient(product(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_213,i_0_31]) ).
cnf(i_0_434,plain,
quotient(product(quotient(product(X1,X2),X2),X3),X3) = difference(X4,product(X4,product(X1,one))),
inference(scs_inference,[],[i_0_25,i_0_213,i_0_31,i_0_30]) ).
cnf(i_0_435,plain,
difference(X1,product(X1,product(one,X2))) = quotient(product(quotient(product(X2,X3),X3),X4),X4),
inference(scs_inference,[],[i_0_25,i_0_216,i_0_31]) ).
cnf(c_0_750,plain,
product(quotient(one,quotient(one,X1)),X2) != product(X1,product(product(difference(X1,one),X1),X2)),
i_0_742 ).
cnf(c_0_751,plain,
product(difference(X1,one),X1) = product(X1,quotient(one,X1)),
i_0_22 ).
cnf(c_0_752,plain,
product(X1,difference(X1,quotient(X2,one))) = product(quotient(X2,X3),X3),
i_0_743 ).
cnf(c_0_753,axiom,
product(X1,difference(X1,X2)) = X2,
i_0_26 ).
cnf(c_0_754,axiom,
product(quotient(X1,X2),X2) = X1,
i_0_24 ).
cnf(c_0_755,plain,
product(X1,product(product(X1,quotient(one,X1)),X2)) != product(quotient(one,quotient(one,X1)),X2),
inference(rw,[status(thm)],[c_0_750,c_0_751]) ).
cnf(c_0_756,plain,
quotient(X1,one) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_752,c_0_753]),c_0_754]) ).
cnf(c_0_757,axiom,
product(one,X1) = X1,
i_0_27 ).
cnf(c_0_758,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_755,c_0_756]),c_0_757]),c_0_757]),c_0_757]),c_0_756]),c_0_757])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP764-1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.12/0.32 % Computer : n019.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon May 4 19:05:59 EDT 2026
% 0.12/0.32 % CPUTime :
% 0.12/0.33 % start to proof: theBenchmark
% 101.11/77.93 % Version : CSE_E---1.7
% 101.11/77.93 % Problem : theBenchmark.p
% 101.11/77.93 % SZS status Unsatisfiable for theBenchmark.p
% 101.11/77.93 % SZS output start CNFRefutation
% See solution above
% 104.41/81.23 % Total time : 77.594s
%------------------------------------------------------------------------------