%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN353+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 09:37:40 AM UTC 2026
% Result : Theorem 5.35s 1.12s
% Output : CNFRefutation 5.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 1
% Syntax : Number of formulae : 96 ( 15 unt; 0 def)
% Number of atoms : 384 ( 0 equ)
% Maximal formula atoms : 47 ( 4 avg)
% Number of connectives : 409 ( 121 ~; 204 |; 56 &)
% ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-3 aty)
% Number of variables : 219 ( 6 sgn 61 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(church_46_18_5,conjecture,
! [X] :
? [Y1,Y2,Y3] :
! [Z] :
( ( big_f(Y1,Y2,Y3)
=> ( big_f(X,X,Z)
=> ( big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1) ) ) )
=> ( ( ( big_f(Y3,Y1,Y2)
=> ( big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) ) )
<=> big_f(Y2,Y1,Z) )
=> ( ( ( big_f(Y2,Y3,Y1)
=> ( big_f(Y3,Y1,Y2)
& big_f(Y1,Y2,Y3) ) )
<=> big_f(Y1,Z,Y2) )
=> ( ( ( ( big_f(Y3,Y1,Y2)
=> ~ big_f(Y2,Y3,Y1) )
=> big_f(Y1,Y2,Y3) )
<=> big_f(Z,Y2,Y1) )
=> ( ( big_f(Y3,Y1,Y2)
& big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) )
<=> big_f(Z,Z,Z) ) ) ) ) ),
file('theBenchmark.p',church_46_18_5) ).
fof(church_46_18_5_neg,negated_conjecture,
~ ! [X] :
? [Y1,Y2,Y3] :
! [Z] :
( ( big_f(Y1,Y2,Y3)
=> ( big_f(X,X,Z)
=> ( big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1) ) ) )
=> ( ( ( big_f(Y3,Y1,Y2)
=> ( big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) ) )
<=> big_f(Y2,Y1,Z) )
=> ( ( ( big_f(Y2,Y3,Y1)
=> ( big_f(Y3,Y1,Y2)
& big_f(Y1,Y2,Y3) ) )
<=> big_f(Y1,Z,Y2) )
=> ( ( ( ( big_f(Y3,Y1,Y2)
=> ~ big_f(Y2,Y3,Y1) )
=> big_f(Y1,Y2,Y3) )
<=> big_f(Z,Y2,Y1) )
=> ( ( big_f(Y3,Y1,Y2)
& big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) )
<=> big_f(Z,Z,Z) ) ) ) ) ),
inference(assume_negation,[status(cth)],[church_46_18_5]) ).
fof(nnf_1,plain,
? [X] :
! [Y1,Y2,Y3] :
? [Z] :
( ( ~ big_f(Z,Z,Z)
| ~ big_f(Y3,Y1,Y2)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y1,Y2,Y3) )
& ( big_f(Z,Z,Z)
| ( big_f(Y3,Y1,Y2)
& big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) ) )
& ( ~ big_f(Z,Y2,Y1)
| big_f(Y1,Y2,Y3)
| ( big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) )
& ( big_f(Z,Y2,Y1)
| ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y1,Z,Y2)
| ( big_f(Y3,Y1,Y2)
& big_f(Y1,Y2,Y3) )
| ~ big_f(Y2,Y3,Y1) )
& ( big_f(Y1,Z,Y2)
| ( ( ~ big_f(Y3,Y1,Y2)
| ~ big_f(Y1,Y2,Y3) )
& big_f(Y2,Y3,Y1) ) )
& ( ~ big_f(Y2,Y1,Z)
| ( big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) )
| ~ big_f(Y3,Y1,Y2) )
& ( big_f(Y2,Y1,Z)
| ( ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y1,Y2,Y3) )
& big_f(Y3,Y1,Y2) ) )
& ( big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1)
| ~ big_f(X,X,Z)
| ~ big_f(Y1,Y2,Y3) ) ),
inference(fof_nnf,[status(thm)],[church_46_18_5_neg]) ).
fof(sk_church_46_18_5_neg_sk,plain,
! [Y1,Y2,Y3] :
( ( ~ big_f(sK1(Y1,Y2,Y3),sK1(Y1,Y2,Y3),sK1(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y1,Y2,Y3) )
& ( big_f(sK1(Y1,Y2,Y3),sK1(Y1,Y2,Y3),sK1(Y1,Y2,Y3))
| ( big_f(Y3,Y1,Y2)
& big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) ) )
& ( ~ big_f(sK1(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| ( big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) )
& ( big_f(sK1(Y1,Y2,Y3),Y2,Y1)
| ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y1,sK1(Y1,Y2,Y3),Y2)
| ( big_f(Y3,Y1,Y2)
& big_f(Y1,Y2,Y3) )
| ~ big_f(Y2,Y3,Y1) )
& ( big_f(Y1,sK1(Y1,Y2,Y3),Y2)
| ( ( ~ big_f(Y3,Y1,Y2)
| ~ big_f(Y1,Y2,Y3) )
& big_f(Y2,Y3,Y1) ) )
& ( ~ big_f(Y2,Y1,sK1(Y1,Y2,Y3))
| ( big_f(Y2,Y3,Y1)
& big_f(Y1,Y2,Y3) )
| ~ big_f(Y3,Y1,Y2) )
& ( big_f(Y2,Y1,sK1(Y1,Y2,Y3))
| ( ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y1,Y2,Y3) )
& big_f(Y3,Y1,Y2) ) )
& ( big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1)
| ~ big_f(sK0,sK0,sK1(Y1,Y2,Y3))
| ~ big_f(Y1,Y2,Y3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X,sK0),skolemize(Z,sK1(Y1,Y2,Y3))],[nnf_1]) ).
fof(sk_church_46_18_5_neg,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(sK1(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2))
| ~ big_f(VAR_2,VAR_0,VAR_1)
| ~ big_f(VAR_1,VAR_2,VAR_0)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(sK1(VAR_1,VAR_2,VAR_0),sK1(VAR_1,VAR_2,VAR_0),sK1(VAR_1,VAR_2,VAR_0))
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(sK1(VAR_2,VAR_0,VAR_1),sK1(VAR_2,VAR_0,VAR_1),sK1(VAR_2,VAR_0,VAR_1))
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(sK1(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2))
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(sK1(VAR_2,VAR_0,VAR_1),VAR_0,VAR_2)
| big_f(VAR_2,VAR_0,VAR_1)
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(sK1(VAR_1,VAR_2,VAR_0),VAR_2,VAR_1)
| big_f(VAR_1,VAR_2,VAR_0)
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(sK1(VAR_0,VAR_1,VAR_2),VAR_1,VAR_0)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(sK1(VAR_1,VAR_2,VAR_0),VAR_2,VAR_1)
| ~ big_f(VAR_2,VAR_0,VAR_1)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(VAR_2,sK1(VAR_2,VAR_0,VAR_1),VAR_0)
| big_f(VAR_1,VAR_2,VAR_0)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(VAR_2,sK1(VAR_2,VAR_0,VAR_1),VAR_0)
| big_f(VAR_2,VAR_0,VAR_1)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(VAR_0,sK1(VAR_0,VAR_1,VAR_2),VAR_1)
| ~ big_f(VAR_2,VAR_0,VAR_1)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(VAR_2,sK1(VAR_2,VAR_0,VAR_1),VAR_0)
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(VAR_2,VAR_1,sK1(VAR_1,VAR_2,VAR_0))
| big_f(VAR_2,VAR_0,VAR_1)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_f(VAR_2,VAR_1,sK1(VAR_1,VAR_2,VAR_0))
| big_f(VAR_1,VAR_2,VAR_0)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(VAR_1,VAR_0,sK1(VAR_0,VAR_1,VAR_2))
| ~ big_f(VAR_1,VAR_2,VAR_0)
| ~ big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(VAR_2,VAR_1,sK1(VAR_1,VAR_2,VAR_0))
| big_f(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_f(VAR_2,VAR_0,VAR_1)
| big_f(VAR_1,VAR_2,VAR_0)
| ~ big_f(sK0,sK0,sK1(VAR_0,VAR_1,VAR_2))
| ~ big_f(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_church_46_18_5_neg_sk]) ).
cnf(c_2,negated_conjecture,
( big_f(C,A,B)
| big_f(B,C,A)
| ~ big_f(sK0,sK0,sK1(A,B,C))
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_3,negated_conjecture,
( big_f(C,B,sK1(B,C,A))
| big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_4,negated_conjecture,
( big_f(B,A,sK1(A,B,C))
| ~ big_f(B,C,A)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_5,negated_conjecture,
( ~ big_f(C,B,sK1(B,C,A))
| big_f(B,C,A)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_6,negated_conjecture,
( ~ big_f(C,B,sK1(B,C,A))
| big_f(C,A,B)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_7,negated_conjecture,
( big_f(C,sK1(C,A,B),A)
| big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_8,negated_conjecture,
( big_f(A,sK1(A,B,C),B)
| ~ big_f(C,A,B)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_9,negated_conjecture,
( ~ big_f(C,sK1(C,A,B),A)
| big_f(C,A,B)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_10,negated_conjecture,
( ~ big_f(C,sK1(C,A,B),A)
| big_f(B,C,A)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_11,negated_conjecture,
( big_f(sK1(B,C,A),C,B)
| ~ big_f(C,A,B)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_12,negated_conjecture,
( big_f(sK1(A,B,C),B,A)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_13,negated_conjecture,
( ~ big_f(sK1(B,C,A),C,B)
| big_f(B,C,A)
| big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_14,negated_conjecture,
( ~ big_f(sK1(C,A,B),A,C)
| big_f(C,A,B)
| big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_18,negated_conjecture,
( ~ big_f(sK1(A,B,C),sK1(A,B,C),sK1(A,B,C))
| ~ big_f(C,A,B)
| ~ big_f(B,C,A)
| ~ big_f(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_church_46_18_5_neg]) ).
cnf(c_19,plain,
( big_f(A,A,sK1(A,A,A))
| ~ big_f(A,A,A) ),
inference(factor,[status(thm)],[c_4]) ).
cnf(c_20,plain,
( big_f(A,sK1(A,A,A),A)
| ~ big_f(A,A,A) ),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_21,plain,
( ~ big_f(sK1(A,A,A),A,A)
| big_f(A,A,A) ),
inference(factor,[status(thm)],[c_13]) ).
cnf(c_1135,negated_conjecture,
( big_f(A,sK0,sK0)
| big_f(sK0,A,sK0)
| ~ big_f(sK0,sK0,A)
| big_f(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_25,negated_conjecture,
( big_f(sK0,A,sK0)
| ~ big_f(sK0,sK0,A)
| big_f(A,sK0,sK0) ),
inference(copy,[status(thm)],[c_1135]) ).
cnf(c_41,plain,
( big_f(A,B,C)
| big_f(C,A,B)
| ~ big_f(sK0,sK0,sK1(B,C,A))
| big_f(A,sK1(A,B,C),B) ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_46,plain,
( big_f(A,C,sK1(C,A,B))
| big_f(sK1(C,A,B),A,C)
| ~ big_f(sK0,sK0,sK1(C,sK1(C,A,B),A))
| big_f(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_65,plain,
( big_f(A,C,sK1(C,A,B))
| big_f(sK1(C,A,B),A,C)
| ~ big_f(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_3]) ).
cnf(c_67,plain,
( big_f(B,sK1(B,C,A),C)
| big_f(sK1(B,C,A),C,B)
| ~ big_f(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_7]) ).
cnf(c_1136,negated_conjecture,
( big_f(A,A,sK1(A,A,A))
| big_f(A,A,sK1(A,A,A)) ),
inference(resolve,[status(thm)],[c_19,c_3]) ).
cnf(c_136,negated_conjecture,
big_f(A,A,sK1(A,A,A)),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_1137,negated_conjecture,
( big_f(A,sK1(A,A,A),A)
| big_f(A,sK1(A,A,A),A) ),
inference(resolve,[status(thm)],[c_20,c_7]) ).
cnf(c_141,negated_conjecture,
big_f(A,sK1(A,A,A),A),
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_152,plain,
( big_f(A,sK0,sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(resolve,[status(thm)],[c_25,c_3]) ).
cnf(c_153,plain,
big_f(sK1(A,A,sK1(A,A,A)),A,A),
inference(resolve,[status(thm)],[c_136,c_12]) ).
cnf(c_1138,negated_conjecture,
( big_f(sK0,sK0,A)
| big_f(A,sK0,sK0)
| big_f(A,sK0,sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(resolve,[status(thm)],[c_152,c_13]) ).
cnf(c_398,negated_conjecture,
( big_f(sK0,sK0,A)
| big_f(A,sK0,sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(copy,[status(thm)],[c_1138]) ).
cnf(c_1139,plain,
( big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(resolve,[status(thm)],[c_152,c_67]) ).
cnf(c_1140,plain,
( big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(copy,[status(thm)],[c_1139]) ).
cnf(c_411,plain,
( big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_1141,negated_conjecture,
( ~ big_f(sK0,sK0,sK1(sK0,sK0,sK1(sK0,sK0,A)))
| big_f(sK0,sK1(sK0,sK0,A),sK0)
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(resolve,[status(thm)],[c_411,c_6]) ).
cnf(c_418,negated_conjecture,
( ~ big_f(sK0,sK0,sK1(sK0,sK0,sK1(sK0,sK0,A)))
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(copy,[status(thm)],[c_1141]) ).
cnf(c_1142,negated_conjecture,
( ~ big_f(sK0,sK1(sK0,sK0,sK1(sK0,sK0,A)),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(resolve,[status(thm)],[c_411,c_10]) ).
cnf(c_425,negated_conjecture,
( ~ big_f(sK0,sK1(sK0,sK0,sK1(sK0,sK0,A)),sK0)
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(copy,[status(thm)],[c_1142]) ).
cnf(c_1143,negated_conjecture,
( big_f(A,sK0,sK0)
| ~ big_f(sK0,A,sK0)
| big_f(sK0,sK0,A)
| big_f(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_398,c_10]) ).
cnf(c_435,negated_conjecture,
( ~ big_f(sK0,A,sK0)
| big_f(sK0,sK0,A)
| big_f(A,sK0,sK0) ),
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_1144,plain,
( big_f(sK1(sK0,sK0,A),sK0,sK0)
| big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(resolve,[status(thm)],[c_435,c_411]) ).
cnf(c_477,plain,
( big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK1(sK0,sK0,A),sK0,sK0) ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_479,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,A,sK0)
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(resolve,[status(thm)],[c_477,c_14]) ).
cnf(c_1145,negated_conjecture,
( big_f(sK0,A,sK0)
| ~ big_f(A,sK0,sK0)
| big_f(sK0,sK0,A)
| big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_479,c_6]) ).
cnf(c_521,negated_conjecture,
( ~ big_f(A,sK0,sK0)
| big_f(sK0,sK0,A)
| big_f(sK0,A,sK0) ),
inference(copy,[status(thm)],[c_1145]) ).
cnf(c_1146,plain,
( big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(resolve,[status(thm)],[c_521,c_477]) ).
cnf(c_558,plain,
( big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK0,sK1(sK0,sK0,A),sK0) ),
inference(copy,[status(thm)],[c_1146]) ).
cnf(c_564,plain,
( big_f(sK0,sK0,A)
| ~ big_f(sK0,A,sK0)
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(resolve,[status(thm)],[c_558,c_9]) ).
cnf(c_1147,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK0,sK0,A)
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(resolve,[status(thm)],[c_564,c_479]) ).
cnf(c_1148,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,sK0,A)
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_599,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(copy,[status(thm)],[c_1148]) ).
cnf(c_1149,negated_conjecture,
( big_f(sK0,sK0,A)
| ~ big_f(A,sK0,sK0)
| big_f(sK0,sK0,A) ),
inference(resolve,[status(thm)],[c_599,c_5]) ).
cnf(c_622,negated_conjecture,
( ~ big_f(A,sK0,sK0)
| big_f(sK0,sK0,A) ),
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_1150,plain,
( big_f(sK0,sK0,sK1(sK0,sK0,A))
| big_f(sK0,sK0,sK1(sK0,sK0,A)) ),
inference(resolve,[status(thm)],[c_622,c_477]) ).
cnf(c_636,plain,
big_f(sK0,sK0,sK1(sK0,sK0,A)),
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_641,negated_conjecture,
big_f(sK0,sK1(sK0,sK0,A),sK0),
inference(resolve,[status(thm)],[c_636,c_418]) ).
cnf(c_646,negated_conjecture,
big_f(sK1(sK0,sK0,A),sK0,sK0),
inference(resolve,[status(thm)],[c_641,c_425]) ).
cnf(c_658,plain,
( big_f(sK0,A,sK0)
| ~ big_f(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_636,c_6]) ).
cnf(c_661,plain,
( big_f(A,sK0,sK0)
| ~ big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_641,c_10]) ).
cnf(c_662,plain,
( big_f(sK0,sK0,A)
| ~ big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_641,c_9]) ).
cnf(c_679,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_646,c_14]) ).
cnf(c_1151,plain,
( big_f(sK0,sK0,A)
| big_f(sK0,sK0,A) ),
inference(resolve,[status(thm)],[c_679,c_662]) ).
cnf(c_685,plain,
big_f(sK0,sK0,A),
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_1152,plain,
( big_f(sK0,A,sK0)
| big_f(A,sK0,sK0)
| big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_679,c_25]) ).
cnf(c_691,plain,
( big_f(A,sK0,sK0)
| big_f(sK0,A,sK0) ),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_698,plain,
( big_f(A,C,sK1(C,A,B))
| big_f(sK1(C,A,B),A,C)
| big_f(A,B,C) ),
inference(resolve,[status(thm)],[c_685,c_46]) ).
cnf(c_699,plain,
( big_f(A,B,C)
| big_f(C,A,B)
| big_f(A,sK1(A,B,C),B) ),
inference(resolve,[status(thm)],[c_685,c_41]) ).
cnf(c_702,negated_conjecture,
( big_f(C,A,B)
| big_f(B,C,A)
| ~ big_f(A,B,C) ),
inference(resolve,[status(thm)],[c_685,c_2]) ).
cnf(c_1153,plain,
( big_f(A,sK0,sK0)
| big_f(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_691,c_661]) ).
cnf(c_714,plain,
big_f(A,sK0,sK0),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_1154,plain,
( big_f(sK0,A,sK0)
| big_f(sK0,A,sK0) ),
inference(resolve,[status(thm)],[c_691,c_658]) ).
cnf(c_715,plain,
big_f(sK0,A,sK0),
inference(copy,[status(thm)],[c_1154]) ).
cnf(c_1155,negated_conjecture,
( ~ big_f(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0))
| ~ big_f(sK0,sK0,A)
| ~ big_f(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_18,c_715]) ).
cnf(c_1156,negated_conjecture,
( ~ big_f(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0))
| ~ big_f(sK0,sK0,A) ),
inference(resolve,[status(thm)],[c_1155,c_714]) ).
cnf(c_742,negated_conjecture,
~ big_f(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0)),
inference(resolve,[status(thm)],[c_1156,c_685]) ).
cnf(c_790,plain,
~ big_f(sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0)),sK1(sK0,A,sK0),sK1(sK0,A,sK0)),
inference(resolve,[status(thm)],[c_21,c_742]) ).
cnf(c_1157,negated_conjecture,
( ~ big_f(A,sK1(A,A,sK1(A,A,A)),A)
| big_f(sK1(A,A,A),A,A) ),
inference(resolve,[status(thm)],[c_10,c_141]) ).
cnf(c_915,negated_conjecture,
~ big_f(sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0))),sK1(sK0,A,sK0)),
inference(resolve,[status(thm)],[c_1157,c_790]) ).
cnf(c_1158,plain,
( big_f(B,A,sK1(A,B,C))
| big_f(sK1(A,B,C),B,A)
| big_f(B,A,sK1(A,B,C))
| big_f(sK1(A,B,C),B,A) ),
inference(resolve,[status(thm)],[c_698,c_65]) ).
cnf(c_1159,plain,
( big_f(B,A,sK1(A,B,C))
| big_f(B,A,sK1(A,B,C))
| big_f(sK1(A,B,C),B,A) ),
inference(copy,[status(thm)],[c_1158]) ).
cnf(c_1024,plain,
( big_f(B,A,sK1(A,B,C))
| big_f(sK1(A,B,C),B,A) ),
inference(copy,[status(thm)],[c_1159]) ).
cnf(c_1160,negated_conjecture,
( big_f(B,sK1(B,A,C),A)
| big_f(A,B,sK1(B,A,C))
| big_f(A,B,sK1(B,A,C)) ),
inference(resolve,[status(thm)],[c_1024,c_702]) ).
cnf(c_1040,negated_conjecture,
( big_f(B,sK1(B,A,C),A)
| big_f(A,B,sK1(B,A,C)) ),
inference(copy,[status(thm)],[c_1160]) ).
cnf(c_1066,plain,
( big_f(A,B,C)
| ~ big_f(C,A,B)
| big_f(A,sK1(A,B,C),B) ),
inference(resolve,[status(thm)],[c_1040,c_5]) ).
cnf(c_1161,negated_conjecture,
( ~ big_f(A,sK1(A,sK1(A,A,sK1(A,A,A)),A),sK1(A,A,sK1(A,A,A)))
| big_f(A,sK1(A,A,sK1(A,A,A)),A) ),
inference(resolve,[status(thm)],[c_9,c_153]) ).
cnf(c_1108,negated_conjecture,
~ big_f(sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0))),sK1(sK0,A,sK0)),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0)))),
inference(resolve,[status(thm)],[c_1161,c_915]) ).
cnf(c_1162,plain,
( big_f(A,B,C)
| big_f(A,sK1(A,B,C),B)
| big_f(A,B,C)
| big_f(A,sK1(A,B,C),B) ),
inference(resolve,[status(thm)],[c_1066,c_699]) ).
cnf(c_1163,plain,
( big_f(A,B,C)
| big_f(A,B,C)
| big_f(A,sK1(A,B,C),B) ),
inference(copy,[status(thm)],[c_1162]) ).
cnf(c_1119,plain,
( big_f(A,B,C)
| big_f(A,sK1(A,B,C),B) ),
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_1164,plain,
big_f(sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0))),sK1(sK0,A,sK0)),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK1(sK0,A,sK0),sK1(sK0,A,sK0),sK1(sK0,A,sK0)))),
inference(resolve,[status(thm)],[c_1119,c_915]) ).
cnf(c_1134,plain,
$false,
inference(resolve,[status(thm)],[c_1108,c_1164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN353+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.42 % Computer : n001.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Sat Sep 26 17:43:13 UTC 2026
% 0.18/0.42 % CPUTime :
% 0.18/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.43 % Process 2345778 was started by sandbox2 on n001,
% 0.18/0.43 % Sat Sep 26 17:43:13 2026
% 0.18/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.43
% 0.18/0.43 % From the command line: assign(max_seconds, 300).
% 5.35/1.12
% 5.35/1.12 % SZS status Theorem for theBenchmark
% 5.35/1.12
% 5.35/1.12 % Proof 1 at 0.54 (+ 0.13) seconds.
% 5.35/1.12 % Length of proof is 62.
% 5.35/1.12 % Level of proof is 23.
% 5.35/1.12 % Maximum clause weight is 83.000.
% 5.35/1.12 % Given clauses 147.
% 5.35/1.12
% 5.35/1.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------