%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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:28:23 PM UTC 2026
% Result : Theorem 7.79s 1.73s
% Output : Proof 7.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 10
% Syntax : Number of formulae : 248 ( 248 unt; 0 def)
% Number of atoms : 248 ( 247 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% 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 : 372 ( 0 sgn 56 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [C,B,A] : bigC(A,B,C) = product(product(A,B),product(C,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos08) ).
fof(f7_nnf,plain,
! [C,B,A] : bigC(A,B,C) = product(product(A,B),product(C,A)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C] : bigC(A,B,C) = product(product(A,B),product(C,A)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
bigC(X2,X1,X0) = product(product(X2,X1),product(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t6,plain,
product(product(X1,X2),product(X3,X1)) = bigC(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t43,plain,
product(product(X1,X2),product(X3,X1)) = bigC(X1,X2,X3),
inference(orient,[status(thm)],[t6]) ).
fof(f4,axiom,
! [D,C,B,A] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos05) ).
fof(f4_nnf,plain,
! [D,C,B,A] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t8,plain,
product(product(X1,X2),product(X3,X4)) = product(product(X1,X3),product(X2,X4)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t27,plain,
product(product(X1,X2),product(X3,X4)) = product(product(X1,X3),product(X2,X4)),
inference(orient,[status(thm)],[t8]) ).
cnf(t46,plain,
bigC(X1,X2,X3) = product(product(X1,X3),product(X2,X1)),
inference(cp,[status(thm)],[t43,t27]) ).
cnf(t5988,plain,
bigC(X1,X2,X3) = bigC(X1,X3,X2),
inference(step,[status(thm)],[t46,t43]) ).
cnf(t127,plain,
bigC(X1,X2,X3) = bigC(X1,X3,X2),
inference(orient,[status(thm)],[t5988]) ).
fof(f1,axiom,
! [B,A] : product(A,difference(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos02) ).
fof(f1_nnf,plain,
! [B,A] : product(A,difference(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] : product(A,difference(A,B)) = B,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
product(X1,difference(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
product(X1,difference(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t9,plain,
product(X1,difference(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t29,plain,
product(product(X1,X2),product(difference(X1,X3),X4)) = product(X3,product(X2,X4)),
inference(cp,[status(thm)],[t27,t9]) ).
cnf(t5762,plain,
product(product(X1,X2),product(difference(X1,X3),X4)) = product(X3,product(X2,X4)),
inference(orient,[status(thm)],[t29]) ).
fof(f2,axiom,
! [B,A] : quotient(product(A,B),B) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos03) ).
fof(f2_nnf,plain,
! [B,A] : quotient(product(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : quotient(product(A,B),B) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
quotient(product(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
quotient(product(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t19,plain,
quotient(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
fof(f5,axiom,
! [A] : product(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos06) ).
fof(f5_nnf,plain,
! [A] : product(A,A) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : product(A,A) = A,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
product(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
product(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t10,plain,
product(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t52,plain,
bigC(X1,X2,X1) = product(product(X1,X2),X1),
inference(cp,[status(thm)],[t43,t10]) ).
cnf(t98,plain,
product(product(X1,X2),X1) = bigC(X1,X2,X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t112,plain,
product(X1,X2) = quotient(bigC(X1,X2,X1),X1),
inference(cp,[status(thm)],[t19,t98]) ).
cnf(t124,plain,
quotient(bigC(X1,X2,X1),X1) = product(X1,X2),
inference(orient,[status(thm)],[t112]) ).
cnf(t128,plain,
product(X1,X2) = quotient(bigC(X1,X1,X2),X1),
inference(cp,[status(thm)],[t124,t127]) ).
cnf(t131,plain,
quotient(bigC(X1,X1,X2),X1) = product(X1,X2),
inference(orient,[status(thm)],[t128]) ).
cnf(t47,plain,
bigC(X1,X1,X2) = product(X1,product(X2,X1)),
inference(cp,[status(thm)],[t43,t10]) ).
cnf(t81,plain,
product(X1,product(X2,X1)) = bigC(X1,X1,X2),
inference(orient,[status(thm)],[t47]) ).
fof(f3,axiom,
! [B,A] : product(quotient(A,B),B) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos04) ).
fof(f3_nnf,plain,
! [B,A] : product(quotient(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : product(quotient(A,B),B) = A,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
product(quotient(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t3,plain,
product(quotient(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
product(quotient(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t85,plain,
bigC(X1,X1,quotient(X2,X1)) = product(X1,X2),
inference(cp,[status(thm)],[t81,t16]) ).
cnf(t117,plain,
bigC(X1,X1,quotient(X2,X1)) = product(X1,X2),
inference(orient,[status(thm)],[t85]) ).
cnf(t132,plain,
product(X1,quotient(X2,X1)) = quotient(product(X1,X2),X1),
inference(cp,[status(thm)],[t131,t117]) ).
cnf(t136,plain,
product(X1,quotient(X2,X1)) = quotient(product(X1,X2),X1),
inference(orient,[status(thm)],[t132]) ).
cnf(t21,plain,
X1 = quotient(X2,difference(X1,X2)),
inference(cp,[status(thm)],[t19,t9]) ).
cnf(t79,plain,
quotient(X1,difference(X2,X1)) = X2,
inference(orient,[status(thm)],[t21]) ).
fof(f0,axiom,
! [B,A] : difference(A,product(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos01) ).
fof(f0_nnf,plain,
! [B,A] : difference(A,product(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : difference(A,product(A,B)) = B,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
difference(X1,product(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
difference(X1,product(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t23,plain,
difference(X1,product(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
fof(f6,axiom,
! [B,A] : product(product(product(A,B),B),product(B,product(B,A))) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos07) ).
fof(f6_nnf,plain,
! [B,A] : product(product(product(A,B),B),product(B,product(B,A))) = B,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] : product(product(product(A,B),B),product(B,product(B,A))) = B,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t7,plain,
product(product(product(X1,X2),X2),product(X2,product(X2,X1))) = X2,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t11,plain,
product(product(product(X1,X2),X2),product(X2,product(X2,X1))) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t26,plain,
product(X1,product(X1,X2)) = difference(product(product(X2,X1),X1),X1),
inference(cp,[status(thm)],[t23,t11]) ).
cnf(t360,plain,
difference(product(product(X1,X2),X2),X2) = product(X2,product(X2,X1)),
inference(orient,[status(thm)],[t26]) ).
cnf(t371,plain,
product(X1,product(X1,quotient(X2,X1))) = difference(product(X2,X1),X1),
inference(cp,[status(thm)],[t360,t16]) ).
cnf(t5994,plain,
product(X1,quotient(product(X1,X2),X1)) = difference(product(X2,X1),X1),
inference(step,[status(thm)],[t371,t136]) ).
cnf(t5995,plain,
quotient(product(X1,product(X1,X2)),X1) = difference(product(X2,X1),X1),
inference(step,[status(thm)],[t5994,t136]) ).
cnf(t757,plain,
quotient(product(X1,product(X1,X2)),X1) = difference(product(X2,X1),X1),
inference(orient,[status(thm)],[t5995]) ).
cnf(t762,plain,
difference(product(quotient(X1,X2),X2),X2) = quotient(product(X2,quotient(product(X2,X1),X2)),X2),
inference(cp,[status(thm)],[t757,t136]) ).
cnf(t5996,plain,
difference(X1,X2) = quotient(product(X2,quotient(product(X2,X1),X2)),X2),
inference(step,[status(thm)],[t762,t16]) ).
cnf(t5997,plain,
difference(X1,X2) = quotient(quotient(product(X2,product(X2,X1)),X2),X2),
inference(step,[status(thm)],[t5996,t136]) ).
cnf(t5998,plain,
difference(X1,X2) = quotient(difference(product(X1,X2),X2),X2),
inference(step,[status(thm)],[t5997,t757]) ).
cnf(t785,plain,
quotient(difference(product(X1,X2),X2),X2) = difference(X1,X2),
inference(orient,[status(thm)],[t5998]) ).
cnf(t797,plain,
difference(quotient(X1,X2),X2) = quotient(difference(X1,X2),X2),
inference(cp,[status(thm)],[t785,t16]) ).
cnf(t812,plain,
difference(quotient(X1,X2),X2) = quotient(difference(X1,X2),X2),
inference(orient,[status(thm)],[t797]) ).
cnf(t828,plain,
quotient(X1,X2) = quotient(X2,quotient(difference(X1,X2),X2)),
inference(cp,[status(thm)],[t79,t812]) ).
cnf(t865,plain,
quotient(X1,quotient(difference(X2,X1),X1)) = quotient(X2,X1),
inference(orient,[status(thm)],[t828]) ).
cnf(t25,plain,
X1 = difference(quotient(X2,X1),X2),
inference(cp,[status(thm)],[t23,t16]) ).
cnf(t80,plain,
difference(quotient(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t878,plain,
quotient(quotient(X1,X2),X1) = quotient(X1,quotient(X2,X1)),
inference(cp,[status(thm)],[t865,t80]) ).
cnf(t887,plain,
quotient(quotient(X1,X2),X1) = quotient(X1,quotient(X2,X1)),
inference(orient,[status(thm)],[t878]) ).
cnf(t28,plain,
product(product(X1,X2),product(X1,X3)) = product(X1,product(X2,X3)),
inference(cp,[status(thm)],[t27,t10]) ).
cnf(t378,plain,
product(product(X1,X2),product(X1,X3)) = product(X1,product(X2,X3)),
inference(orient,[status(thm)],[t28]) ).
cnf(t399,plain,
product(X1,product(X2,difference(X1,X3))) = product(product(X1,X2),X3),
inference(cp,[status(thm)],[t378,t9]) ).
cnf(t1050,plain,
product(X1,product(X2,difference(X1,X3))) = product(product(X1,X2),X3),
inference(orient,[status(thm)],[t399]) ).
cnf(t1090,plain,
product(X1,difference(X2,X3)) = difference(X2,product(product(X2,X1),X3)),
inference(cp,[status(thm)],[t23,t1050]) ).
cnf(t1676,plain,
difference(X1,product(product(X1,X2),X3)) = product(X2,difference(X1,X3)),
inference(orient,[status(thm)],[t1090]) ).
fof(f8,axiom,
product(product(a,c),product(c,b)) = product(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos09) ).
fof(f8_nnf,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t5,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t67,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(orient,[status(thm)],[t5]) ).
cnf(t1684,plain,
product(c,difference(a,product(c,b))) = difference(a,product(a,b)),
inference(cp,[status(thm)],[t1676,t67]) ).
cnf(t6021,plain,
product(c,difference(a,product(c,b))) = b,
inference(step,[status(thm)],[t1684,t23]) ).
cnf(t1740,plain,
product(c,difference(a,product(c,b))) = b,
inference(orient,[status(thm)],[t6021]) ).
cnf(t1758,plain,
difference(a,product(c,b)) = difference(c,b),
inference(cp,[status(thm)],[t23,t1740]) ).
cnf(t1770,plain,
difference(a,product(c,b)) = difference(c,b),
inference(orient,[status(thm)],[t1758]) ).
cnf(t1771,plain,
product(c,b) = product(a,difference(c,b)),
inference(cp,[status(thm)],[t9,t1770]) ).
cnf(t1790,plain,
product(a,difference(c,b)) = product(c,b),
inference(orient,[status(thm)],[t1771]) ).
cnf(t1815,plain,
product(product(c,a),b) = product(c,product(c,b)),
inference(cp,[status(thm)],[t1050,t1790]) ).
cnf(t1820,plain,
product(product(c,a),b) = product(c,product(c,b)),
inference(orient,[status(thm)],[t1815]) ).
cnf(t1839,plain,
product(c,a) = quotient(product(c,product(c,b)),b),
inference(cp,[status(thm)],[t19,t1820]) ).
cnf(t1871,plain,
quotient(product(c,product(c,b)),b) = product(c,a),
inference(orient,[status(thm)],[t1839]) ).
cnf(t32,plain,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
inference(cp,[status(thm)],[t27,t10]) ).
cnf(t427,plain,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
inference(orient,[status(thm)],[t32]) ).
cnf(t439,plain,
product(product(quotient(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(cp,[status(thm)],[t427,t16]) ).
cnf(t1100,plain,
product(product(quotient(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(orient,[status(thm)],[t439]) ).
cnf(t1144,plain,
product(quotient(X1,X2),X3) = quotient(product(X1,product(X3,X2)),X2),
inference(cp,[status(thm)],[t19,t1100]) ).
cnf(t1951,plain,
quotient(product(X1,product(X2,X3)),X3) = product(quotient(X1,X3),X2),
inference(orient,[status(thm)],[t1144]) ).
cnf(t6023,plain,
product(quotient(c,b),c) = product(c,a),
inference(step,[status(thm)],[t1871,t1951]) ).
cnf(t811,plain,
difference(product(X1,X2),X2) = product(difference(X1,X2),X2),
inference(cp,[status(thm)],[t16,t785]) ).
cnf(t835,plain,
difference(product(X1,X2),X2) = product(difference(X1,X2),X2),
inference(orient,[status(thm)],[t811]) ).
cnf(t857,plain,
product(X1,X2) = quotient(X2,product(difference(X1,X2),X2)),
inference(cp,[status(thm)],[t79,t835]) ).
cnf(t906,plain,
quotient(X1,product(difference(X2,X1),X1)) = product(X2,X1),
inference(orient,[status(thm)],[t857]) ).
cnf(t919,plain,
product(quotient(X1,X2),X1) = quotient(X1,product(X2,X1)),
inference(cp,[status(thm)],[t906,t80]) ).
cnf(t927,plain,
product(quotient(X1,X2),X1) = quotient(X1,product(X2,X1)),
inference(orient,[status(thm)],[t919]) ).
cnf(t6024,plain,
quotient(c,product(b,c)) = product(c,a),
inference(step,[status(thm)],[t6023,t927]) ).
cnf(t2016,plain,
quotient(c,product(b,c)) = product(c,a),
inference(rw,[status(thm)],[t6024]) ).
cnf(t2017,plain,
quotient(c,product(b,c)) = product(c,a),
inference(orient,[status(thm)],[t2016]) ).
cnf(t2021,plain,
quotient(c,quotient(product(b,c),c)) = quotient(product(c,a),c),
inference(cp,[status(thm)],[t887,t2017]) ).
cnf(t6027,plain,
quotient(c,b) = quotient(product(c,a),c),
inference(step,[status(thm)],[t2021,t19]) ).
cnf(t2034,plain,
quotient(product(c,a),c) = quotient(c,b),
inference(orient,[status(thm)],[t6027]) ).
cnf(t2045,plain,
quotient(product(c,product(c,a)),c) = product(c,quotient(c,b)),
inference(cp,[status(thm)],[t136,t2034]) ).
cnf(t5999,plain,
quotient(product(X1,product(X1,X2)),X1) = product(difference(X2,X1),X1),
inference(step,[status(thm)],[t757,t835]) ).
cnf(t836,plain,
quotient(product(X1,product(X1,X2)),X1) = product(difference(X2,X1),X1),
inference(orient,[status(thm)],[t5999]) ).
cnf(t6051,plain,
product(difference(a,c),c) = product(c,quotient(c,b)),
inference(step,[status(thm)],[t2045,t836]) ).
cnf(t92,plain,
product(X1,X2) = difference(X2,bigC(X2,X2,X1)),
inference(cp,[status(thm)],[t23,t81]) ).
cnf(t119,plain,
difference(X1,bigC(X1,X1,X2)) = product(X2,X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t101,plain,
bigC(X1,difference(X1,X2),X1) = product(X2,X1),
inference(cp,[status(thm)],[t98,t9]) ).
cnf(t121,plain,
bigC(X1,difference(X1,X2),X1) = product(X2,X1),
inference(orient,[status(thm)],[t101]) ).
cnf(t130,plain,
bigC(X1,difference(X1,X2),X1) = product(X2,X1),
inference(rw,[status(thm)],[t121]) ).
cnf(t5989,plain,
bigC(X1,X1,difference(X1,X2)) = product(X2,X1),
inference(step,[status(thm)],[t130,t127]) ).
cnf(t153,plain,
bigC(X1,X1,difference(X1,X2)) = product(X2,X1),
inference(orient,[status(thm)],[t5989]) ).
cnf(t158,plain,
product(difference(X1,X2),X1) = difference(X1,product(X2,X1)),
inference(cp,[status(thm)],[t119,t153]) ).
cnf(t159,plain,
difference(X1,product(X2,X1)) = product(difference(X1,X2),X1),
inference(orient,[status(thm)],[t158]) ).
cnf(t22,plain,
product(product(X1,X2),X2) = quotient(X2,product(X2,product(X2,X1))),
inference(cp,[status(thm)],[t19,t11]) ).
cnf(t340,plain,
quotient(X1,product(X1,product(X1,X2))) = product(product(X2,X1),X1),
inference(orient,[status(thm)],[t22]) ).
cnf(t346,plain,
product(product(difference(X1,X2),X1),X1) = quotient(X1,product(X1,X2)),
inference(cp,[status(thm)],[t340,t9]) ).
cnf(t480,plain,
product(product(difference(X1,X2),X1),X1) = quotient(X1,product(X1,X2)),
inference(orient,[status(thm)],[t346]) ).
cnf(t499,plain,
product(difference(X1,product(difference(X1,X2),X1)),X1) = difference(X1,quotient(X1,product(X1,X2))),
inference(cp,[status(thm)],[t159,t480]) ).
cnf(t5991,plain,
product(product(difference(X1,difference(X1,X2)),X1),X1) = difference(X1,quotient(X1,product(X1,X2))),
inference(step,[status(thm)],[t499,t159]) ).
cnf(t5992,plain,
quotient(X1,product(X1,difference(X1,X2))) = difference(X1,quotient(X1,product(X1,X2))),
inference(step,[status(thm)],[t5991,t480]) ).
cnf(t5993,plain,
quotient(X1,X2) = difference(X1,quotient(X1,product(X1,X2))),
inference(step,[status(thm)],[t5992,t9]) ).
cnf(t512,plain,
difference(X1,quotient(X1,product(X1,X2))) = quotient(X1,X2),
inference(orient,[status(thm)],[t5993]) ).
cnf(t517,plain,
quotient(X1,difference(X1,X2)) = difference(X1,quotient(X1,X2)),
inference(cp,[status(thm)],[t512,t9]) ).
cnf(t534,plain,
difference(X1,quotient(X1,X2)) = quotient(X1,difference(X1,X2)),
inference(orient,[status(thm)],[t517]) ).
cnf(t542,plain,
quotient(X1,X2) = product(X1,quotient(X1,difference(X1,X2))),
inference(cp,[status(thm)],[t9,t534]) ).
cnf(t632,plain,
product(X1,quotient(X1,difference(X1,X2))) = quotient(X1,X2),
inference(orient,[status(thm)],[t542]) ).
cnf(t637,plain,
quotient(X1,product(X1,X2)) = product(X1,quotient(X1,X2)),
inference(cp,[status(thm)],[t632,t23]) ).
cnf(t665,plain,
product(X1,quotient(X1,X2)) = quotient(X1,product(X1,X2)),
inference(orient,[status(thm)],[t637]) ).
cnf(t6052,plain,
product(difference(a,c),c) = quotient(c,product(c,b)),
inference(step,[status(thm)],[t6051,t665]) ).
cnf(t2661,plain,
product(difference(a,c),c) = quotient(c,product(c,b)),
inference(orient,[status(thm)],[t6052]) ).
cnf(t453,plain,
product(product(X1,quotient(X2,X3)),X3) = product(product(X1,X3),X2),
inference(cp,[status(thm)],[t427,t16]) ).
cnf(t1152,plain,
product(product(X1,quotient(X2,X3)),X3) = product(product(X1,X3),X2),
inference(orient,[status(thm)],[t453]) ).
cnf(t1156,plain,
product(product(X1,X2),X1) = product(quotient(X1,product(X1,X2)),X2),
inference(cp,[status(thm)],[t1152,t665]) ).
cnf(t6008,plain,
bigC(X1,X2,X1) = product(quotient(X1,product(X1,X2)),X2),
inference(step,[status(thm)],[t1156,t98]) ).
cnf(t1204,plain,
product(quotient(X1,product(X1,X2)),X2) = bigC(X1,X2,X1),
inference(orient,[status(thm)],[t6008]) ).
cnf(t1214,plain,
bigC(X1,difference(X1,X2),X1) = product(quotient(X1,X2),difference(X1,X2)),
inference(cp,[status(thm)],[t1204,t9]) ).
cnf(t48,plain,
bigC(X1,difference(X1,X2),X3) = product(X2,product(X3,X1)),
inference(cp,[status(thm)],[t43,t9]) ).
cnf(t170,plain,
bigC(X1,difference(X1,X2),X3) = product(X2,product(X3,X1)),
inference(orient,[status(thm)],[t48]) ).
cnf(t6009,plain,
product(X2,product(X1,X1)) = product(quotient(X1,X2),difference(X1,X2)),
inference(step,[status(thm)],[t1214,t170]) ).
cnf(t6010,plain,
product(X2,X1) = product(quotient(X1,X2),difference(X1,X2)),
inference(step,[status(thm)],[t6009,t10]) ).
cnf(t1289,plain,
product(quotient(X1,X2),difference(X1,X2)) = product(X2,X1),
inference(orient,[status(thm)],[t6010]) ).
cnf(t2019,plain,
product(product(b,c),c) = product(product(c,a),difference(c,product(b,c))),
inference(cp,[status(thm)],[t1289,t2017]) ).
cnf(t6034,plain,
product(product(b,c),c) = product(product(c,a),product(difference(c,b),c)),
inference(step,[status(thm)],[t2019,t159]) ).
cnf(t6035,plain,
product(product(b,c),c) = bigC(c,a,difference(c,b)),
inference(step,[status(thm)],[t6034,t43]) ).
cnf(t171,plain,
product(X1,product(X2,X3)) = bigC(X3,X2,difference(X3,X1)),
inference(cp,[status(thm)],[t170,t127]) ).
cnf(t181,plain,
bigC(X1,X2,difference(X1,X3)) = product(X3,product(X2,X1)),
inference(orient,[status(thm)],[t171]) ).
cnf(t6036,plain,
product(product(b,c),c) = product(b,product(a,c)),
inference(step,[status(thm)],[t6035,t181]) ).
cnf(t2317,plain,
product(product(b,c),c) = product(b,product(a,c)),
inference(orient,[status(thm)],[t6036]) ).
cnf(t2342,plain,
product(c,difference(b,c)) = difference(b,product(b,product(a,c))),
inference(cp,[status(thm)],[t1676,t2317]) ).
cnf(t6038,plain,
product(c,difference(b,c)) = product(a,c),
inference(step,[status(thm)],[t2342,t23]) ).
cnf(t2391,plain,
product(c,difference(b,c)) = product(a,c),
inference(orient,[status(thm)],[t6038]) ).
cnf(t2409,plain,
difference(b,c) = difference(c,product(a,c)),
inference(cp,[status(thm)],[t23,t2391]) ).
cnf(t6039,plain,
difference(b,c) = product(difference(c,a),c),
inference(step,[status(thm)],[t2409,t159]) ).
cnf(t2443,plain,
product(difference(c,a),c) = difference(b,c),
inference(orient,[status(thm)],[t6039]) ).
cnf(t2446,plain,
product(difference(difference(c,a),c),c) = difference(difference(b,c),c),
inference(cp,[status(thm)],[t835,t2443]) ).
cnf(t535,plain,
quotient(X1,difference(X1,difference(X2,X1))) = difference(X1,X2),
inference(cp,[status(thm)],[t534,t79]) ).
cnf(t547,plain,
quotient(X1,difference(X1,difference(X2,X1))) = difference(X1,X2),
inference(orient,[status(thm)],[t535]) ).
cnf(t562,plain,
difference(X1,difference(X2,X1)) = difference(difference(X1,X2),X1),
inference(cp,[status(thm)],[t80,t547]) ).
cnf(t564,plain,
difference(difference(X1,X2),X1) = difference(X1,difference(X2,X1)),
inference(orient,[status(thm)],[t562]) ).
cnf(t6042,plain,
product(difference(c,difference(a,c)),c) = difference(difference(b,c),c),
inference(step,[status(thm)],[t2446,t564]) ).
cnf(t764,plain,
difference(product(difference(X1,X2),X1),X1) = quotient(product(X1,X2),X1),
inference(cp,[status(thm)],[t757,t9]) ).
cnf(t6019,plain,
product(difference(difference(X1,X2),X1),X1) = quotient(product(X1,X2),X1),
inference(step,[status(thm)],[t764,t835]) ).
cnf(t6020,plain,
product(difference(X1,difference(X2,X1)),X1) = quotient(product(X1,X2),X1),
inference(step,[status(thm)],[t6019,t564]) ).
cnf(t1570,plain,
product(difference(X1,difference(X2,X1)),X1) = quotient(product(X1,X2),X1),
inference(orient,[status(thm)],[t6020]) ).
cnf(t6043,plain,
quotient(product(c,a),c) = difference(difference(b,c),c),
inference(step,[status(thm)],[t6042,t1570]) ).
cnf(t6044,plain,
quotient(c,b) = difference(difference(b,c),c),
inference(step,[status(thm)],[t6043,t2034]) ).
cnf(t2509,plain,
difference(difference(b,c),c) = quotient(c,b),
inference(orient,[status(thm)],[t6044]) ).
cnf(t2510,plain,
c = product(difference(b,c),quotient(c,b)),
inference(cp,[status(thm)],[t9,t2509]) ).
cnf(t3040,plain,
product(difference(b,c),quotient(c,b)) = c,
inference(orient,[status(thm)],[t2510]) ).
cnf(t3066,plain,
product(product(difference(b,c),b),c) = product(c,b),
inference(cp,[status(thm)],[t1152,t3040]) ).
cnf(t3800,plain,
product(product(difference(b,c),b),c) = product(c,b),
inference(orient,[status(thm)],[t3066]) ).
cnf(t3819,plain,
product(difference(b,c),b) = quotient(product(c,b),c),
inference(cp,[status(thm)],[t19,t3800]) ).
cnf(t144,plain,
quotient(X1,X2) = difference(X2,quotient(product(X2,X1),X2)),
inference(cp,[status(thm)],[t23,t136]) ).
cnf(t204,plain,
difference(X1,quotient(product(X1,X2),X1)) = quotient(X2,X1),
inference(orient,[status(thm)],[t144]) ).
cnf(t206,plain,
quotient(difference(X1,X2),X1) = difference(X1,quotient(X2,X1)),
inference(cp,[status(thm)],[t204,t9]) ).
cnf(t216,plain,
difference(X1,quotient(X2,X1)) = quotient(difference(X1,X2),X1),
inference(orient,[status(thm)],[t206]) ).
cnf(t482,plain,
quotient(X1,product(X1,quotient(X2,X1))) = product(product(quotient(difference(X1,X2),X1),X1),X1),
inference(cp,[status(thm)],[t480,t216]) ).
cnf(t6015,plain,
quotient(X1,quotient(product(X1,X2),X1)) = product(product(quotient(difference(X1,X2),X1),X1),X1),
inference(step,[status(thm)],[t482,t136]) ).
cnf(t6016,plain,
quotient(X1,quotient(product(X1,X2),X1)) = product(difference(X1,X2),product(X1,X1)),
inference(step,[status(thm)],[t6015,t1100]) ).
cnf(t6017,plain,
quotient(X1,quotient(product(X1,X2),X1)) = product(difference(X1,X2),X1),
inference(step,[status(thm)],[t6016,t10]) ).
cnf(t1494,plain,
quotient(X1,quotient(product(X1,X2),X1)) = product(difference(X1,X2),X1),
inference(orient,[status(thm)],[t6017]) ).
cnf(t2416,plain,
product(difference(c,difference(b,c)),c) = quotient(c,quotient(product(a,c),c)),
inference(cp,[status(thm)],[t1494,t2391]) ).
cnf(t6040,plain,
quotient(product(c,b),c) = quotient(c,quotient(product(a,c),c)),
inference(step,[status(thm)],[t2416,t1570]) ).
cnf(t6041,plain,
quotient(product(c,b),c) = quotient(c,a),
inference(step,[status(thm)],[t6040,t19]) ).
cnf(t2480,plain,
quotient(product(c,b),c) = quotient(c,a),
inference(orient,[status(thm)],[t6041]) ).
cnf(t6114,plain,
product(difference(b,c),b) = quotient(c,a),
inference(step,[status(thm)],[t3819,t2480]) ).
cnf(t3840,plain,
product(difference(b,c),b) = quotient(c,a),
inference(orient,[status(thm)],[t6114]) ).
cnf(t3855,plain,
bigC(b,b,difference(b,c)) = product(b,quotient(c,a)),
inference(cp,[status(thm)],[t81,t3840]) ).
cnf(t6115,plain,
product(c,product(b,b)) = product(b,quotient(c,a)),
inference(step,[status(thm)],[t3855,t181]) ).
cnf(t6116,plain,
product(c,b) = product(b,quotient(c,a)),
inference(step,[status(thm)],[t6115,t10]) ).
cnf(t3882,plain,
product(b,quotient(c,a)) = product(c,b),
inference(orient,[status(thm)],[t6116]) ).
cnf(t3909,plain,
product(product(b,a),c) = product(product(c,b),a),
inference(cp,[status(thm)],[t1152,t3882]) ).
cnf(t1103,plain,
product(X1,product(X1,X2)) = product(quotient(X1,product(X2,X1)),X2),
inference(cp,[status(thm)],[t1100,t927]) ).
cnf(t1886,plain,
product(quotient(X1,product(X2,X1)),X2) = product(X1,product(X1,X2)),
inference(orient,[status(thm)],[t1103]) ).
cnf(t666,plain,
quotient(X1,product(X1,difference(X2,X1))) = product(X1,X2),
inference(cp,[status(thm)],[t665,t79]) ).
cnf(t741,plain,
quotient(X1,product(X1,difference(X2,X1))) = product(X1,X2),
inference(orient,[status(thm)],[t666]) ).
cnf(t2419,plain,
product(c,b) = quotient(c,product(a,c)),
inference(cp,[status(thm)],[t741,t2391]) ).
cnf(t2496,plain,
quotient(c,product(a,c)) = product(c,b),
inference(orient,[status(thm)],[t2419]) ).
cnf(t2506,plain,
product(c,product(c,a)) = product(product(c,b),a),
inference(cp,[status(thm)],[t1886,t2496]) ).
cnf(t2821,plain,
product(product(c,b),a) = product(c,product(c,a)),
inference(orient,[status(thm)],[t2506]) ).
cnf(t6119,plain,
product(product(b,a),c) = product(c,product(c,a)),
inference(step,[status(thm)],[t3909,t2821]) ).
cnf(t3990,plain,
product(product(b,a),c) = product(c,product(c,a)),
inference(orient,[status(thm)],[t6119]) ).
cnf(t4009,plain,
product(b,a) = quotient(product(c,product(c,a)),c),
inference(cp,[status(thm)],[t19,t3990]) ).
cnf(t6120,plain,
product(b,a) = product(difference(a,c),c),
inference(step,[status(thm)],[t4009,t836]) ).
cnf(t6121,plain,
product(b,a) = quotient(c,product(c,b)),
inference(step,[status(thm)],[t6120,t2661]) ).
cnf(t4030,plain,
quotient(c,product(c,b)) = product(b,a),
inference(orient,[status(thm)],[t6121]) ).
cnf(t6122,plain,
product(difference(a,c),c) = product(b,a),
inference(step,[status(thm)],[t2661,t4030]) ).
cnf(t4031,plain,
product(difference(a,c),c) = product(b,a),
inference(orient,[status(thm)],[t6122]) ).
cnf(t5844,plain,
product(c,product(X1,c)) = product(product(a,X1),product(b,a)),
inference(cp,[status(thm)],[t5762,t4031]) ).
cnf(t6214,plain,
bigC(c,c,X1) = product(product(a,X1),product(b,a)),
inference(step,[status(thm)],[t5844,t81]) ).
cnf(t6215,plain,
bigC(c,c,X1) = bigC(a,X1,b),
inference(step,[status(thm)],[t6214,t43]) ).
cnf(t5977,plain,
bigC(a,X1,b) = bigC(c,c,X1),
inference(orient,[status(thm)],[t6215]) ).
fof(f9,conjecture,
! [X0] : bigC(a,b,X0) = bigC(c,c,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f9_neg,negated_conjecture,
~ ! [X0] : bigC(a,b,X0) = bigC(c,c,X0),
inference(negated_conjecture,[status(cth)],[f9]) ).
fof(f9_nnf,plain,
? [X0] : bigC(a,b,X0) != bigC(c,c,X0),
inference(nnf_transformation,[status(thm)],[f9_neg]) ).
fof(f9_sk,plain,
bigC(a,b,sk0) != bigC(c,c,sk0),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f9_nnf]) ).
cnf(c9,plain,
bigC(a,b,sk0) != bigC(c,c,sk0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(goal_0,negated_conjecture,
bigC(c,c,sk0) != bigC(a,b,sk0),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(g0_0,plain,
bigC(c,c,sk0) != bigC(a,sk0,b),
inference(rw,[status(thm)],[goal_0,t127]) ).
cnf(g0_1,plain,
bigC(c,c,sk0) != bigC(c,c,sk0),
inference(rw,[status(thm)],[g0_0,t5977]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:56:44 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.79/1.73 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.79/1.73 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------