%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 07:24:38 AM UTC 2026
% Result : Theorem 125.49s 26.44s
% Output : CNFRefutation 125.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 10
% Syntax : Number of formulae : 147 ( 147 unt; 0 def)
% Number of atoms : 147 ( 146 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 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 : 226 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos01,axiom,
! [X0,X1] : difference(X1,product(X1,X0)) = X0 ).
fof(sos02,axiom,
! [X0,X1] : product(X1,difference(X1,X0)) = X0 ).
fof(sos03,axiom,
! [X0,X1] : quotient(product(X1,X0),X0) = X1 ).
fof(sos04,axiom,
! [X0,X1] : product(quotient(X1,X0),X0) = X1 ).
fof(sos05,axiom,
! [X0,X1,X2,X3] : product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)) ).
fof(sos06,axiom,
! [X0] : product(X0,X0) = X0 ).
fof(sos07,axiom,
! [X0,X1] : product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0 ).
fof(sos08,axiom,
! [X0,X1,X2] : bigC(X2,X1,X0) = product(product(X2,X1),product(X0,X2)) ).
fof(sos09,axiom,
product(product(a,c),product(c,b)) = product(a,b) ).
fof(goals,conjecture,
! [X0] : bigC(a,b,X0) = bigC(c,c,X0) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] : bigC(a,b,X0) = bigC(c,c,X0),
inference(negate_conjecture,[status(cth)],[goals]) ).
cnf(c0,plain,
difference(X0,product(X0,X1)) = X1,
inference(clausification,[status(esa)],[sos01]) ).
cnf(c1,plain,
product(X0,difference(X0,X1)) = X1,
inference(clausification,[status(esa)],[sos02]) ).
cnf(c2,plain,
quotient(product(X0,X1),X1) = X0,
inference(clausification,[status(esa)],[sos03]) ).
cnf(c3,plain,
product(quotient(X0,X1),X1) = X0,
inference(clausification,[status(esa)],[sos04]) ).
cnf(c4,plain,
product(product(X0,X1),product(X2,X3)) = product(product(X0,X2),product(X1,X3)),
inference(clausification,[status(esa)],[sos05]) ).
cnf(c5,plain,
product(X0,X0) = X0,
inference(clausification,[status(esa)],[sos06]) ).
cnf(c6,plain,
product(product(product(X0,X1),X1),product(X1,product(X1,X0))) = X1,
inference(clausification,[status(esa)],[sos07]) ).
cnf(c7,plain,
bigC(X0,X1,X2) = product(product(X0,X1),product(X2,X0)),
inference(clausification,[status(esa)],[sos08]) ).
cnf(c8,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(clausification,[status(esa)],[sos09]) ).
cnf(c9,plain,
bigC(a,b,sK18) != bigC(c,c,sK18),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
product(product(X0,X2),product(X1,X0)) = bigC(X0,X1,X2),
inference(superposition,[status(thm)],[c7,c4]) ).
cnf(d1,plain,
bigC(X0,X1,X2) = bigC(X0,X2,X1),
inference(superposition,[status(thm)],[d0,c7]) ).
cnf(d2,plain,
product(product(X0,X0),product(X1,X1)) = product(X0,X1),
inference(superposition,[status(thm)],[c4,c5]) ).
cnf(d3,plain,
product(X0,product(X1,X1)) = product(X0,X1),
inference(demodulation,[status(thm)],[d2,c5]) ).
cnf(d4,plain,
product(X1,X0) = product(X1,X0),
inference(demodulation,[status(thm)],[d3,c5]) ).
cnf(d5,plain,
X0 = product(X0,X0),
inference(superposition,[status(thm)],[c5,d4]) ).
cnf(d6,plain,
bigC(X0,X1,X0) = product(product(X0,X1),X0),
inference(superposition,[status(thm)],[d5,c7]) ).
cnf(d7,plain,
product(product(X2,quotient(X0,X1)),product(X3,X1)) = product(product(X2,X3),X0),
inference(superposition,[status(thm)],[c3,c4]) ).
cnf(d8,plain,
quotient(bigC(X0,X1,X0),X0) = product(X0,X1),
inference(superposition,[status(thm)],[d6,c2]) ).
cnf(d9,plain,
quotient(bigC(X0,X0,X1),X0) = product(X0,X1),
inference(superposition,[status(thm)],[d1,d8]) ).
cnf(d10,plain,
bigC(X0,X0,X1) = product(X0,product(X1,X0)),
inference(superposition,[status(thm)],[d5,c7]) ).
cnf(d11,plain,
product(X0,product(X1,X0)) = bigC(X0,X0,X1),
inference(superposition,[status(thm)],[d10,d4]) ).
cnf(d12,plain,
X0 = product(quotient(X0,X1),X1),
inference(superposition,[status(thm)],[c3,d4]) ).
cnf(d13,plain,
product(X1,X0) = bigC(X1,X1,quotient(X0,X1)),
inference(superposition,[status(thm)],[d12,d11]) ).
cnf(d14,plain,
quotient(product(X0,X1),X0) = product(X0,quotient(X1,X0)),
inference(superposition,[status(thm)],[d13,d9]) ).
cnf(d15,plain,
difference(X0,bigC(X0,X0,X1)) = product(X1,X0),
inference(superposition,[status(thm)],[d10,c0]) ).
cnf(d16,plain,
bigC(X0,difference(X0,X1),X0) = product(X1,X0),
inference(superposition,[status(thm)],[c1,d6]) ).
cnf(d17,plain,
bigC(X0,X0,difference(X0,X1)) = product(X1,X0),
inference(demodulation,[status(thm)],[d16,d1]) ).
cnf(d18,plain,
difference(X0,product(X1,X0)) = product(difference(X0,X1),X0),
inference(superposition,[status(thm)],[d17,d15]) ).
cnf(d19,plain,
difference(X1,X0) = product(difference(X1,quotient(X0,X1)),X1),
inference(superposition,[status(thm)],[d12,d18]) ).
cnf(d20,plain,
quotient(difference(X0,X1),X0) = difference(X0,quotient(X1,X0)),
inference(superposition,[status(thm)],[d19,c2]) ).
cnf(d21,plain,
quotient(X1,difference(X0,X1)) = X0,
inference(superposition,[status(thm)],[c1,c2]) ).
cnf(d22,plain,
difference(product(X0,X1),bigC(X0,X1,X0)) = X0,
inference(superposition,[status(thm)],[d6,c0]) ).
cnf(d23,plain,
difference(product(X0,X1),bigC(X0,X0,X1)) = X0,
inference(superposition,[status(thm)],[d1,d22]) ).
cnf(d24,plain,
difference(product(X0,quotient(X1,X0)),product(X0,X1)) = X0,
inference(superposition,[status(thm)],[d13,d23]) ).
cnf(d25,plain,
difference(product(X0,quotient(difference(X0,X1),X0)),X1) = X0,
inference(superposition,[status(thm)],[c1,d24]) ).
cnf(d26,plain,
quotient(X1,X0) = product(X0,quotient(difference(X0,X1),X0)),
inference(superposition,[status(thm)],[d25,d21]) ).
cnf(d27,plain,
quotient(X1,X0) = product(X0,difference(X0,quotient(X1,X0))),
inference(demodulation,[status(thm)],[d26,d20]) ).
cnf(d28,plain,
quotient(X1,X0) = quotient(X1,X0),
inference(demodulation,[status(thm)],[d27,c1]) ).
cnf(d29,plain,
X0 = quotient(product(X0,X1),X1),
inference(superposition,[status(thm)],[c2,d28]) ).
cnf(d30,plain,
quotient(product(product(X0,X2),product(X1,X3)),product(X2,X3)) = product(X0,X1),
inference(superposition,[status(thm)],[c4,c2]) ).
cnf(d31,plain,
quotient(product(X0,product(X2,X3)),product(X1,X3)) = product(quotient(X0,X1),X2),
inference(superposition,[status(thm)],[d12,d30]) ).
cnf(d32,plain,
product(X0,product(X1,X2)) = product(product(X0,X1),product(X0,X2)),
inference(superposition,[status(thm)],[c5,c4]) ).
cnf(d33,plain,
product(X0,product(X2,difference(X0,X1))) = product(product(X0,X2),X1),
inference(superposition,[status(thm)],[c1,d32]) ).
cnf(d34,plain,
difference(product(X0,X1),product(product(X0,X2),product(X1,X3))) = product(X2,X3),
inference(superposition,[status(thm)],[c4,c0]) ).
cnf(d35,plain,
difference(product(X0,X1),product(X0,product(X1,X2))) = product(X0,X2),
inference(superposition,[status(thm)],[d5,d34]) ).
cnf(d36,plain,
difference(product(X2,X0),product(X2,X1)) = product(X2,difference(X0,X1)),
inference(superposition,[status(thm)],[c1,d35]) ).
cnf(d37,plain,
difference(product(a,c),product(a,b)) = product(c,b),
inference(superposition,[status(thm)],[c8,c0]) ).
cnf(d38,plain,
product(a,difference(c,b)) = product(c,b),
inference(demodulation,[status(thm)],[d37,d36]) ).
cnf(d39,plain,
product(c,product(c,b)) = product(product(c,a),b),
inference(superposition,[status(thm)],[d38,d33]) ).
cnf(d40,plain,
product(product(X0,X2),product(product(X1,X0),X3)) = product(bigC(X0,X0,X1),product(X2,X3)),
inference(superposition,[status(thm)],[d10,c4]) ).
cnf(d41,plain,
product(product(X0,X2),product(X1,product(X0,X1))) = bigC(product(X0,X1),product(X0,X1),X2),
inference(superposition,[status(thm)],[d10,c4]) ).
cnf(d42,plain,
product(product(X1,X2),bigC(X0,X0,X1)) = bigC(product(X1,X0),product(X1,X0),X2),
inference(demodulation,[status(thm)],[d41,d10]) ).
cnf(d43,plain,
bigC(product(X2,X3),product(X2,X3),product(X0,X1)) = product(product(X2,X3),product(product(X0,X2),product(X1,X3))),
inference(superposition,[status(thm)],[c4,d10]) ).
cnf(d44,plain,
product(product(X0,product(X2,X3)),bigC(X1,X1,X0)) = product(product(X0,X1),product(product(X2,X0),product(X3,X1))),
inference(demodulation,[status(thm)],[d43,d42]) ).
cnf(d45,plain,
product(product(X0,product(X2,X3)),bigC(X1,X1,X0)) = product(bigC(X0,X0,X2),product(X1,product(X3,X1))),
inference(demodulation,[status(thm)],[d44,d40]) ).
cnf(d46,plain,
product(product(X2,product(X3,X1)),bigC(X0,X0,X2)) = product(bigC(X2,X2,X3),bigC(X0,X0,X1)),
inference(demodulation,[status(thm)],[d45,d10]) ).
cnf(d47,plain,
bigC(product(c,b),product(c,b),product(a,c)) = product(product(c,b),product(a,b)),
inference(superposition,[status(thm)],[c8,d10]) ).
cnf(d48,plain,
product(product(c,product(a,c)),bigC(b,b,c)) = product(product(c,b),product(a,b)),
inference(demodulation,[status(thm)],[d47,d42]) ).
cnf(d49,plain,
product(bigC(c,c,a),bigC(b,b,c)) = product(product(c,b),product(a,b)),
inference(demodulation,[status(thm)],[d48,d46]) ).
cnf(d50,plain,
product(bigC(c,c,a),bigC(b,c,b)) = product(product(c,b),product(a,b)),
inference(demodulation,[status(thm)],[d49,d1]) ).
cnf(d51,plain,
product(bigC(c,c,a),bigC(b,c,b)) = product(product(c,a),product(b,b)),
inference(demodulation,[status(thm)],[d50,c4]) ).
cnf(d52,plain,
product(bigC(c,c,a),bigC(b,c,b)) = product(product(c,a),b),
inference(demodulation,[status(thm)],[d51,c5]) ).
cnf(d53,plain,
product(bigC(c,c,a),bigC(b,c,b)) = product(c,product(c,b)),
inference(demodulation,[status(thm)],[d52,d39]) ).
cnf(d54,plain,
quotient(bigC(X0,X0,X1),product(X1,X0)) = X0,
inference(superposition,[status(thm)],[d10,c2]) ).
cnf(d55,plain,
quotient(bigC(product(c,b),product(c,b),product(a,c)),product(a,b)) = product(c,b),
inference(superposition,[status(thm)],[c8,d54]) ).
cnf(d56,plain,
quotient(product(product(c,product(a,c)),bigC(b,b,c)),product(a,b)) = product(c,b),
inference(demodulation,[status(thm)],[d55,d42]) ).
cnf(d57,plain,
quotient(product(bigC(c,c,a),bigC(b,b,c)),product(a,b)) = product(c,b),
inference(demodulation,[status(thm)],[d56,d46]) ).
cnf(d58,plain,
quotient(product(bigC(c,c,a),bigC(b,c,b)),product(a,b)) = product(c,b),
inference(demodulation,[status(thm)],[d57,d1]) ).
cnf(d59,plain,
quotient(product(c,product(c,b)),product(a,b)) = product(c,b),
inference(demodulation,[status(thm)],[d58,d53]) ).
cnf(d60,plain,
product(quotient(c,a),c) = product(c,b),
inference(demodulation,[status(thm)],[d59,d31]) ).
cnf(d61,plain,
quotient(c,a) = quotient(product(c,b),c),
inference(superposition,[status(thm)],[d60,d29]) ).
cnf(d62,plain,
quotient(c,a) = product(c,quotient(b,c)),
inference(demodulation,[status(thm)],[d61,d14]) ).
cnf(d63,plain,
product(product(X2,X3),X0) = product(product(X2,quotient(X0,X1)),product(X3,X1)),
inference(superposition,[status(thm)],[c3,c4]) ).
cnf(d64,plain,
product(product(X1,X0),X2) = product(product(X1,quotient(X2,X0)),X0),
inference(superposition,[status(thm)],[d5,d63]) ).
cnf(d65,plain,
product(X0,product(difference(X0,X1),X2)) = product(X1,product(X0,X2)),
inference(superposition,[status(thm)],[c1,d32]) ).
cnf(d66,plain,
quotient(product(X0,product(X1,X2)),product(X0,X2)) = product(X0,X1),
inference(superposition,[status(thm)],[d5,d30]) ).
cnf(d67,plain,
quotient(product(X2,X1),product(X2,difference(X0,X1))) = product(X2,X0),
inference(superposition,[status(thm)],[c1,d66]) ).
cnf(d68,plain,
quotient(X0,product(X0,difference(X1,X0))) = product(X0,X1),
inference(superposition,[status(thm)],[d5,d67]) ).
cnf(d69,plain,
difference(quotient(X0,X1),X0) = X1,
inference(superposition,[status(thm)],[c3,c0]) ).
cnf(d70,plain,
quotient(X0,product(X0,X1)) = product(X0,quotient(X0,X1)),
inference(superposition,[status(thm)],[d69,d68]) ).
cnf(d71,plain,
quotient(X0,X1) = product(X0,quotient(X0,difference(X0,X1))),
inference(superposition,[status(thm)],[c1,d70]) ).
cnf(d72,plain,
difference(X0,quotient(X0,X1)) = quotient(X0,difference(X0,X1)),
inference(superposition,[status(thm)],[d71,c0]) ).
cnf(d73,plain,
quotient(product(product(X1,X2),X0),product(X2,X0)) = product(X1,X0),
inference(superposition,[status(thm)],[d5,d30]) ).
cnf(d74,plain,
quotient(product(X1,X2),product(difference(X0,X1),X2)) = product(X0,X2),
inference(superposition,[status(thm)],[c1,d73]) ).
cnf(d75,plain,
quotient(X0,product(difference(X1,X0),X0)) = product(X1,X0),
inference(superposition,[status(thm)],[d5,d74]) ).
cnf(d76,plain,
quotient(X0,product(X1,X0)) = product(quotient(X0,X1),X0),
inference(superposition,[status(thm)],[d69,d75]) ).
cnf(d77,plain,
product(X0,product(X2,X3)) = product(product(quotient(X0,X1),X2),product(X1,X3)),
inference(superposition,[status(thm)],[c3,c4]) ).
cnf(d78,plain,
product(X1,product(X2,X0)) = product(product(quotient(X1,X0),X2),X0),
inference(superposition,[status(thm)],[d5,d77]) ).
cnf(d79,plain,
quotient(product(X0,X2),product(X1,X2)) = product(quotient(X0,X1),X2),
inference(superposition,[status(thm)],[d12,d73]) ).
cnf(d80,plain,
quotient(product(a,b),product(c,b)) = product(a,c),
inference(superposition,[status(thm)],[c8,c2]) ).
cnf(d81,plain,
product(quotient(a,c),b) = product(a,c),
inference(demodulation,[status(thm)],[d80,d79]) ).
cnf(d82,plain,
product(a,product(b,c)) = product(product(a,c),c),
inference(superposition,[status(thm)],[d81,d78]) ).
cnf(d83,plain,
difference(product(a,c),product(a,product(b,c))) = c,
inference(superposition,[status(thm)],[d82,c0]) ).
cnf(d84,plain,
product(a,difference(c,product(b,c))) = c,
inference(demodulation,[status(thm)],[d83,d36]) ).
cnf(d85,plain,
product(a,product(difference(c,b),c)) = c,
inference(demodulation,[status(thm)],[d84,d18]) ).
cnf(d86,plain,
a = quotient(c,product(difference(c,b),c)),
inference(superposition,[status(thm)],[d85,d29]) ).
cnf(d87,plain,
a = product(quotient(c,difference(c,b)),c),
inference(demodulation,[status(thm)],[d86,d76]) ).
cnf(d88,plain,
a = product(difference(c,quotient(c,b)),c),
inference(demodulation,[status(thm)],[d87,d72]) ).
cnf(d89,plain,
difference(c,quotient(c,b)) = quotient(a,c),
inference(superposition,[status(thm)],[d88,d29]) ).
cnf(d90,plain,
product(c,quotient(a,c)) = quotient(c,b),
inference(superposition,[status(thm)],[d89,c1]) ).
cnf(d91,plain,
product(product(X1,X2),X0) = product(product(X1,X0),product(X2,X0)),
inference(superposition,[status(thm)],[c5,c4]) ).
cnf(d92,plain,
product(product(X2,quotient(X0,X1)),X1) = product(product(X2,X1),X0),
inference(superposition,[status(thm)],[d12,d91]) ).
cnf(d93,plain,
difference(product(X0,quotient(X1,X2)),product(product(X0,X2),X1)) = X2,
inference(superposition,[status(thm)],[d92,c0]) ).
cnf(d94,plain,
X1 = product(X0,difference(X0,X1)),
inference(superposition,[status(thm)],[c1,d4]) ).
cnf(d95,plain,
product(product(product(difference(X0,X1),X0),X0),product(X0,X1)) = X0,
inference(superposition,[status(thm)],[c1,c6]) ).
cnf(d96,plain,
product(product(difference(X0,X1),X0),product(X0,quotient(X1,X0))) = X0,
inference(superposition,[status(thm)],[d19,d95]) ).
cnf(d97,plain,
difference(a,c) = product(difference(c,b),c),
inference(superposition,[status(thm)],[d85,c0]) ).
cnf(d98,plain,
product(difference(a,c),product(c,quotient(b,c))) = c,
inference(superposition,[status(thm)],[d97,d96]) ).
cnf(d99,plain,
difference(difference(a,c),c) = product(c,quotient(b,c)),
inference(superposition,[status(thm)],[d98,c0]) ).
cnf(d100,plain,
c = product(difference(a,c),product(c,quotient(b,c))),
inference(superposition,[status(thm)],[d99,d94]) ).
cnf(d101,plain,
c = product(difference(a,c),quotient(c,a)),
inference(demodulation,[status(thm)],[d100,d62]) ).
cnf(d102,plain,
difference(c,product(product(difference(a,c),a),c)) = a,
inference(superposition,[status(thm)],[d101,d93]) ).
cnf(d103,plain,
product(difference(c,product(difference(a,c),a)),c) = a,
inference(demodulation,[status(thm)],[d102,d18]) ).
cnf(d104,plain,
difference(c,product(difference(a,c),a)) = quotient(a,c),
inference(superposition,[status(thm)],[d103,d29]) ).
cnf(d105,plain,
product(c,quotient(a,c)) = product(difference(a,c),a),
inference(superposition,[status(thm)],[d104,c1]) ).
cnf(d106,plain,
quotient(c,b) = product(difference(a,c),a),
inference(demodulation,[status(thm)],[d105,d90]) ).
cnf(d107,plain,
product(a,quotient(c,b)) = product(c,product(a,a)),
inference(superposition,[status(thm)],[d106,d65]) ).
cnf(d108,plain,
product(a,quotient(c,b)) = product(c,a),
inference(demodulation,[status(thm)],[d107,c5]) ).
cnf(d109,plain,
product(product(a,b),c) = product(product(c,a),b),
inference(superposition,[status(thm)],[d108,d64]) ).
cnf(d110,plain,
product(product(a,b),c) = product(c,product(c,b)),
inference(demodulation,[status(thm)],[d109,d39]) ).
cnf(d111,plain,
product(a,b) = quotient(product(c,product(c,b)),c),
inference(superposition,[status(thm)],[d110,d29]) ).
cnf(d112,plain,
product(a,b) = product(c,quotient(product(c,b),c)),
inference(demodulation,[status(thm)],[d111,d14]) ).
cnf(d113,plain,
product(a,b) = product(c,product(c,quotient(b,c))),
inference(demodulation,[status(thm)],[d112,d14]) ).
cnf(d114,plain,
product(a,b) = product(c,quotient(c,a)),
inference(demodulation,[status(thm)],[d113,d62]) ).
cnf(d115,plain,
product(product(a,b),product(X0,a)) = product(product(c,X0),c),
inference(superposition,[status(thm)],[d114,d7]) ).
cnf(d116,plain,
bigC(a,b,X0) = product(product(c,X0),c),
inference(demodulation,[status(thm)],[d115,c7]) ).
cnf(d117,plain,
bigC(a,b,X0) = bigC(c,X0,c),
inference(demodulation,[status(thm)],[d116,d6]) ).
cnf(d118,plain,
bigC(c,sK18,c) != bigC(c,c,sK18),
inference(demodulation,[status(thm)],[c9,d117]) ).
cnf(d119,plain,
bigC(c,c,sK18) != bigC(c,c,sK18),
inference(demodulation,[status(thm)],[d118,d1]) ).
cnf(d120,plain,
X1 = quotient(X0,difference(X1,X0)),
inference(superposition,[status(thm)],[d21,d28]) ).
cnf(d121,plain,
quotient(X1,X0) = product(X0,quotient(difference(X0,X1),X0)),
inference(superposition,[status(thm)],[c1,d14]) ).
cnf(d122,plain,
quotient(quotient(X1,X0),quotient(difference(X0,X1),X0)) = X0,
inference(superposition,[status(thm)],[d121,c2]) ).
cnf(d123,plain,
quotient(quotient(X1,X0),difference(X0,quotient(X1,X0))) = X0,
inference(demodulation,[status(thm)],[d122,d20]) ).
cnf(d124,plain,
X1 = X1,
inference(demodulation,[status(thm)],[d123,d120]) ).
cnf(d125,plain,
$false,
inference(resolution,[status(thm)],[d124,d119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n005.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Fri Sep 25 15:46:32 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 125.49/26.44 % SZS status Theorem for theBenchmark.p
% 125.49/26.44 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------