%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET776+4 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 08:36:56 AM UTC 2026
% Result : Theorem 12.74s 2.16s
% Output : CNFRefutation 12.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 2
% Syntax : Number of formulae : 36 ( 14 unt; 0 def)
% Number of atoms : 166 ( 0 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 198 ( 68 ~; 63 |; 53 &)
% ( 3 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 59 ( 0 sgn 34 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(pre_order,axiom,
! [R,E] :
( pre_order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X] :
( member(X,E)
=> apply(R,X,X) ) ) ),
file('theBenchmark.p',pre_order) ).
fof(thIII12,conjecture,
! [E,P,R] :
( ( ! [A,B] :
( ( member(B,E)
& member(A,E) )
=> ( apply(R,A,B)
<=> ( apply(P,B,A)
& apply(P,A,B) ) ) )
& pre_order(P,E) )
=> ! [X1,X2,Y1,Y2] :
( ( member(Y2,E)
& member(Y1,E)
& member(X2,E)
& member(X1,E) )
=> ( ( apply(P,X1,X2)
& apply(R,X2,Y2)
& apply(R,X1,Y1) )
=> apply(P,Y1,Y2) ) ) ),
file('theBenchmark.p',thIII12) ).
fof(thIII12_neg,negated_conjecture,
~ ! [E,P,R] :
( ( ! [A,B] :
( ( member(B,E)
& member(A,E) )
=> ( apply(R,A,B)
<=> ( apply(P,B,A)
& apply(P,A,B) ) ) )
& pre_order(P,E) )
=> ! [X1,X2,Y1,Y2] :
( ( member(Y2,E)
& member(Y1,E)
& member(X2,E)
& member(X1,E) )
=> ( ( apply(P,X1,X2)
& apply(R,X2,Y2)
& apply(R,X1,Y1) )
=> apply(P,Y1,Y2) ) ) ),
inference(assume_negation,[status(cth)],[thIII12]) ).
cnf(c_100,plain,
( apply(A,C,E)
| ~ apply(A,D,E)
| ~ apply(A,C,D)
| ~ member(E,B)
| ~ member(D,B)
| ~ member(C,B)
| ~ pre_order(A,B) ),
inference(clausify,[status(thm)],[pre_order]) ).
fof(nnf_17,plain,
? [E,P,R] :
( ? [X1,X2,Y1,Y2] :
( ~ apply(P,Y1,Y2)
& apply(P,X1,X2)
& apply(R,X2,Y2)
& apply(R,X1,Y1)
& member(Y2,E)
& member(Y1,E)
& member(X2,E)
& member(X1,E) )
& ! [A,B] :
( ( ( ~ apply(P,B,A)
| ~ apply(P,A,B)
| apply(R,A,B) )
& ( ( apply(P,B,A)
& apply(P,A,B) )
| ~ apply(R,A,B) ) )
| ~ member(B,E)
| ~ member(A,E) )
& pre_order(P,E) ),
inference(fof_nnf,[status(thm)],[thIII12_neg]) ).
fof(sk_thIII12_neg_sk,plain,
( ~ apply(sK0,sK2,sK3)
& apply(sK0,sK4,sK5)
& apply(sK6,sK5,sK3)
& apply(sK6,sK4,sK2)
& member(sK3,sK1)
& member(sK2,sK1)
& member(sK5,sK1)
& member(sK4,sK1)
& ! [A,B] :
( ( ( ~ apply(sK0,B,A)
| ~ apply(sK0,A,B)
| apply(sK6,A,B) )
& ( ( apply(sK0,B,A)
& apply(sK0,A,B) )
| ~ apply(sK6,A,B) ) )
| ~ member(B,sK1)
| ~ member(A,sK1) )
& pre_order(sK0,sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK6,sK4,sK5,sK2,sK3]),skolemize(E,sK1),skolemize(P,sK0),skolemize(R,sK6),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(Y1,sK2),skolemize(Y2,sK3)],[nnf_17]) ).
fof(sk_thIII12_neg,plain,
( ~ apply(sK0,sK2,sK3)
& apply(sK0,sK4,sK5)
& apply(sK6,sK5,sK3)
& apply(sK6,sK4,sK2)
& member(sK3,sK1)
& member(sK2,sK1)
& member(sK5,sK1)
& member(sK4,sK1)
& ! [VAR_0,VAR_1] :
( ~ apply(sK0,VAR_1,VAR_0)
| ~ apply(sK0,VAR_0,VAR_1)
| apply(sK6,VAR_0,VAR_1)
| ~ member(VAR_1,sK1)
| ~ member(VAR_0,sK1) )
& ! [VAR_0,VAR_1] :
( apply(sK0,VAR_1,VAR_0)
| ~ apply(sK6,VAR_0,VAR_1)
| ~ member(VAR_1,sK1)
| ~ member(VAR_0,sK1) )
& ! [VAR_0,VAR_1] :
( apply(sK0,VAR_0,VAR_1)
| ~ apply(sK6,VAR_0,VAR_1)
| ~ member(VAR_1,sK1)
| ~ member(VAR_0,sK1) )
& pre_order(sK0,sK1) ),
inference(cnf_transformation,[status(thm)],[sk_thIII12_neg_sk]) ).
cnf(c_113,negated_conjecture,
pre_order(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_115,negated_conjecture,
( apply(sK0,A,C)
| ~ apply(sK0,B,C)
| ~ apply(sK0,A,B)
| ~ member(C,sK1)
| ~ member(B,sK1)
| ~ member(A,sK1) ),
inference(resolve,[status(thm)],[c_113,c_100]) ).
cnf(c_220,negated_conjecture,
~ apply(sK0,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_221,negated_conjecture,
apply(sK0,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_222,negated_conjecture,
apply(sK6,sK5,sK3),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_223,negated_conjecture,
apply(sK6,sK4,sK2),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_224,negated_conjecture,
member(sK3,sK1),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_225,negated_conjecture,
member(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_226,negated_conjecture,
member(sK5,sK1),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_227,negated_conjecture,
member(sK4,sK1),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_229,negated_conjecture,
( apply(sK0,B,A)
| ~ apply(sK6,A,B)
| ~ member(B,sK1)
| ~ member(A,sK1) ),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_230,negated_conjecture,
( apply(sK0,A,B)
| ~ apply(sK6,A,B)
| ~ member(B,sK1)
| ~ member(A,sK1) ),
inference(split_conjunct,[status(thm)],[sk_thIII12_neg]) ).
cnf(c_3652,negated_conjecture,
( apply(sK0,sK2,sK4)
| ~ member(sK2,sK1)
| ~ member(sK4,sK1) ),
inference(resolve,[status(thm)],[c_229,c_223]) ).
cnf(c_3653,negated_conjecture,
( apply(sK0,sK2,sK4)
| ~ member(sK2,sK1) ),
inference(resolve,[status(thm)],[c_227,c_3652]) ).
cnf(c_1454,negated_conjecture,
apply(sK0,sK2,sK4),
inference(resolve,[status(thm)],[c_225,c_3653]) ).
cnf(c_3654,negated_conjecture,
( apply(sK0,sK5,sK3)
| ~ member(sK3,sK1)
| ~ member(sK5,sK1) ),
inference(resolve,[status(thm)],[c_230,c_222]) ).
cnf(c_3655,negated_conjecture,
( apply(sK0,sK5,sK3)
| ~ member(sK3,sK1) ),
inference(resolve,[status(thm)],[c_226,c_3654]) ).
cnf(c_1457,negated_conjecture,
apply(sK0,sK5,sK3),
inference(resolve,[status(thm)],[c_224,c_3655]) ).
cnf(c_3656,negated_conjecture,
( apply(sK0,sK2,B)
| ~ apply(sK0,A,B)
| ~ apply(sK0,sK2,A)
| ~ member(B,sK1)
| ~ member(A,sK1) ),
inference(resolve,[status(thm)],[c_115,c_225]) ).
cnf(c_3657,negated_conjecture,
( apply(sK0,sK2,A)
| ~ apply(sK0,sK4,A)
| ~ apply(sK0,sK2,sK4)
| ~ member(A,sK1) ),
inference(resolve,[status(thm)],[c_3656,c_227]) ).
cnf(c_3658,negated_conjecture,
( apply(sK0,sK2,sK5)
| ~ apply(sK0,sK4,sK5)
| ~ apply(sK0,sK2,sK4) ),
inference(resolve,[status(thm)],[c_3657,c_226]) ).
cnf(c_3659,negated_conjecture,
( apply(sK0,sK2,sK5)
| ~ apply(sK0,sK4,sK5) ),
inference(resolve,[status(thm)],[c_3658,c_1454]) ).
cnf(c_2916,negated_conjecture,
apply(sK0,sK2,sK5),
inference(resolve,[status(thm)],[c_3659,c_221]) ).
cnf(c_3660,negated_conjecture,
( apply(sK0,sK2,B)
| ~ apply(sK0,A,B)
| ~ apply(sK0,sK2,A)
| ~ member(B,sK1)
| ~ member(A,sK1) ),
inference(resolve,[status(thm)],[c_115,c_225]) ).
cnf(c_3661,negated_conjecture,
( apply(sK0,sK2,A)
| ~ apply(sK0,sK5,A)
| ~ apply(sK0,sK2,sK5)
| ~ member(A,sK1) ),
inference(resolve,[status(thm)],[c_3660,c_226]) ).
cnf(c_3662,negated_conjecture,
( apply(sK0,sK2,sK3)
| ~ apply(sK0,sK5,sK3)
| ~ apply(sK0,sK2,sK5) ),
inference(resolve,[status(thm)],[c_3661,c_224]) ).
cnf(c_3663,negated_conjecture,
( apply(sK0,sK2,sK3)
| ~ apply(sK0,sK5,sK3) ),
inference(resolve,[status(thm)],[c_3662,c_2916]) ).
cnf(c_3664,negated_conjecture,
apply(sK0,sK2,sK3),
inference(resolve,[status(thm)],[c_3663,c_1457]) ).
cnf(c_3651,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_220,c_3664]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET776+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43 % Computer : n010.cluster.edu
% 0.11/0.43 % Model : x86_64 x86_64
% 0.11/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.43 % Memory : 8046.5625MB
% 0.11/0.43 % OS : Linux 6.8.0-71-generic
% 0.11/0.43 % CPULimit : 300
% 0.11/0.43 % WCLimit : 300
% 0.11/0.43 % DateTime : Sat Sep 26 08:15:00 UTC 2026
% 0.11/0.43 % CPUTime :
% 0.11/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.43 % Process 2878652 was started by sandbox on n010,
% 0.11/0.43 % Sat Sep 26 08:15:00 2026
% 0.11/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.45
% 0.11/0.45 % From the command line: assign(max_seconds, 300).
% 12.74/2.16
% 12.74/2.16 % given #500 (I,wt=37): 613 member(f6(A,B),A) | member(f7(A,B),B) | member(f8(A,B),A) | -member(C,A) | -member(A,A) | -member(A,C) | A = C. [factor(219,e,g)].
% 12.74/2.16
% 12.74/2.16 % SZS status Theorem for theBenchmark
% 12.74/2.16
% 12.74/2.16 % Proof 1 at 1.60 (+ 0.08) seconds.
% 12.74/2.16 % Length of proof is 19.
% 12.74/2.16 % Level of proof is 4.
% 12.74/2.16 % Maximum clause weight is 26.000.
% 12.74/2.16 % Given clauses 737.
% 12.74/2.16
% 12.74/2.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------