%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN348+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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 : Thu May 9 17:47:59 EDT 2024
% Result : CounterSatisfiable 1.09s 1.30s
% Output : Saturation 1.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(church_46_17_4,conjecture,
? [X1] :
! [X2] :
? [X3] :
! [X4] :
( ( ( ( big_f(X1,X4)
<=> big_f(X4,X3) )
<=> big_f(X3,X4) )
<=> big_f(X4,X1) )
& ( ( ( big_f(X2,X4)
<=> big_f(X4,X3) )
<=> big_f(X3,X4) )
<=> big_f(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',church_46_17_4) ).
fof(c0,negated_conjecture,
~ ? [X1] :
! [X2] :
? [X3] :
! [X4] :
( ( ( ( big_f(X1,X4)
<=> big_f(X4,X3) )
<=> big_f(X3,X4) )
<=> big_f(X4,X1) )
& ( ( ( big_f(X2,X4)
<=> big_f(X4,X3) )
<=> big_f(X3,X4) )
<=> big_f(X4,X2) ) ),
inference(assume_negation,[status(cth)],[church_46_17_4]) ).
fof(c1,negated_conjecture,
! [X1] :
? [X2] :
! [X3] :
? [X4] :
( ( ( ( ( ( ( ~ big_f(X1,X4)
| ~ big_f(X4,X3) )
& ( big_f(X1,X4)
| big_f(X4,X3) ) )
| ~ big_f(X3,X4) )
& ( ( ( ~ big_f(X1,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X1,X4) ) )
| big_f(X3,X4) ) )
| ~ big_f(X4,X1) )
& ( ( ( ( ( ~ big_f(X1,X4)
| ~ big_f(X4,X3) )
& ( big_f(X1,X4)
| big_f(X4,X3) ) )
| big_f(X3,X4) )
& ( ~ big_f(X3,X4)
| ( ( ~ big_f(X1,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X1,X4) ) ) ) )
| big_f(X4,X1) ) )
| ( ( ( ( ( ( ~ big_f(X2,X4)
| ~ big_f(X4,X3) )
& ( big_f(X2,X4)
| big_f(X4,X3) ) )
| ~ big_f(X3,X4) )
& ( ( ( ~ big_f(X2,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X2,X4) ) )
| big_f(X3,X4) ) )
| ~ big_f(X4,X2) )
& ( ( ( ( ( ~ big_f(X2,X4)
| ~ big_f(X4,X3) )
& ( big_f(X2,X4)
| big_f(X4,X3) ) )
| big_f(X3,X4) )
& ( ~ big_f(X3,X4)
| ( ( ~ big_f(X2,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X2,X4) ) ) ) )
| big_f(X4,X2) ) ) ),
inference(fof_nnf,[status(thm)],[c0]) ).
fof(c2,negated_conjecture,
! [X1] :
? [X2] :
! [X3] :
( ? [X4] :
( ( ( ( ( ( ~ big_f(X1,X4)
| ~ big_f(X4,X3) )
& ( big_f(X1,X4)
| big_f(X4,X3) ) )
| ~ big_f(X3,X4) )
& ( ( ( ~ big_f(X1,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X1,X4) ) )
| big_f(X3,X4) ) )
| ~ big_f(X4,X1) )
& ( ( ( ( ( ~ big_f(X1,X4)
| ~ big_f(X4,X3) )
& ( big_f(X1,X4)
| big_f(X4,X3) ) )
| big_f(X3,X4) )
& ( ~ big_f(X3,X4)
| ( ( ~ big_f(X1,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X1,X4) ) ) ) )
| big_f(X4,X1) ) )
| ? [X4] :
( ( ( ( ( ( ~ big_f(X2,X4)
| ~ big_f(X4,X3) )
& ( big_f(X2,X4)
| big_f(X4,X3) ) )
| ~ big_f(X3,X4) )
& ( ( ( ~ big_f(X2,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X2,X4) ) )
| big_f(X3,X4) ) )
| ~ big_f(X4,X2) )
& ( ( ( ( ( ~ big_f(X2,X4)
| ~ big_f(X4,X3) )
& ( big_f(X2,X4)
| big_f(X4,X3) ) )
| big_f(X3,X4) )
& ( ~ big_f(X3,X4)
| ( ( ~ big_f(X2,X4)
| big_f(X4,X3) )
& ( ~ big_f(X4,X3)
| big_f(X2,X4) ) ) ) )
| big_f(X4,X2) ) ) ),
inference(shift_quantors,[status(thm)],[c1]) ).
fof(c3,negated_conjecture,
! [X2] :
? [X3] :
! [X4] :
( ? [X5] :
( ( ( ( ( ( ~ big_f(X2,X5)
| ~ big_f(X5,X4) )
& ( big_f(X2,X5)
| big_f(X5,X4) ) )
| ~ big_f(X4,X5) )
& ( ( ( ~ big_f(X2,X5)
| big_f(X5,X4) )
& ( ~ big_f(X5,X4)
| big_f(X2,X5) ) )
| big_f(X4,X5) ) )
| ~ big_f(X5,X2) )
& ( ( ( ( ( ~ big_f(X2,X5)
| ~ big_f(X5,X4) )
& ( big_f(X2,X5)
| big_f(X5,X4) ) )
| big_f(X4,X5) )
& ( ~ big_f(X4,X5)
| ( ( ~ big_f(X2,X5)
| big_f(X5,X4) )
& ( ~ big_f(X5,X4)
| big_f(X2,X5) ) ) ) )
| big_f(X5,X2) ) )
| ? [X6] :
( ( ( ( ( ( ~ big_f(X3,X6)
| ~ big_f(X6,X4) )
& ( big_f(X3,X6)
| big_f(X6,X4) ) )
| ~ big_f(X4,X6) )
& ( ( ( ~ big_f(X3,X6)
| big_f(X6,X4) )
& ( ~ big_f(X6,X4)
| big_f(X3,X6) ) )
| big_f(X4,X6) ) )
| ~ big_f(X6,X3) )
& ( ( ( ( ( ~ big_f(X3,X6)
| ~ big_f(X6,X4) )
& ( big_f(X3,X6)
| big_f(X6,X4) ) )
| big_f(X4,X6) )
& ( ~ big_f(X4,X6)
| ( ( ~ big_f(X3,X6)
| big_f(X6,X4) )
& ( ~ big_f(X6,X4)
| big_f(X3,X6) ) ) ) )
| big_f(X6,X3) ) ) ),
inference(variable_rename,[status(thm)],[c2]) ).
fof(c4,negated_conjecture,
! [X2,X4] :
( ( ( ( ( ( ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4) ) )
| ~ big_f(X4,skolem0002(X2,X4)) )
& ( ( ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4)) ) )
| big_f(X4,skolem0002(X2,X4)) ) )
| ~ big_f(skolem0002(X2,X4),X2) )
& ( ( ( ( ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4) ) )
| big_f(X4,skolem0002(X2,X4)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ( ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4)) ) ) ) )
| big_f(skolem0002(X2,X4),X2) ) )
| ( ( ( ( ( ( ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4) )
& ( big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4) ) )
| ~ big_f(X4,skolem0003(X2,X4)) )
& ( ( ( ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4) )
& ( ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4)) ) )
| big_f(X4,skolem0003(X2,X4)) ) )
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ( ( ( ( ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4) )
& ( big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4) ) )
| big_f(X4,skolem0003(X2,X4)) )
& ( ~ big_f(X4,skolem0003(X2,X4))
| ( ( ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4) )
& ( ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4)) ) ) ) )
| big_f(skolem0003(X2,X4),skolem0001(X2)) ) ) ),
inference(skolemize,[status(esa)],[c3]) ).
fof(c5,negated_conjecture,
! [X2,X4] :
( ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X2,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(X4,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X4)
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(X4,skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),X4)
| big_f(skolem0003(X2,X4),skolem0001(X2)) )
& ( ~ big_f(X4,skolem0002(X2,X4))
| ~ big_f(skolem0002(X2,X4),X4)
| big_f(X2,skolem0002(X2,X4))
| big_f(skolem0002(X2,X4),X2)
| ~ big_f(X4,skolem0003(X2,X4))
| ~ big_f(skolem0003(X2,X4),X4)
| big_f(skolem0001(X2),skolem0003(X2,X4))
| big_f(skolem0003(X2,X4),skolem0001(X2)) ) ),
inference(distribute,[status(thm)],[c4]) ).
cnf(c68,negated_conjecture,
( ~ big_f(X219,skolem0002(X218,X219))
| ~ big_f(skolem0002(X218,X219),X219)
| big_f(X218,skolem0002(X218,X219))
| big_f(skolem0002(X218,X219),X218)
| ~ big_f(X219,skolem0003(X218,X219))
| ~ big_f(skolem0001(X218),skolem0003(X218,X219))
| big_f(skolem0003(X218,X219),X219)
| big_f(skolem0003(X218,X219),skolem0001(X218)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c434,plain,
( ~ big_f(skolem0001(X417),skolem0002(X417,skolem0001(X417)))
| ~ big_f(skolem0002(X417,skolem0001(X417)),skolem0001(X417))
| big_f(X417,skolem0002(X417,skolem0001(X417)))
| big_f(skolem0002(X417,skolem0001(X417)),X417)
| ~ big_f(skolem0001(X417),skolem0003(X417,skolem0001(X417)))
| big_f(skolem0003(X417,skolem0001(X417)),skolem0001(X417)) ),
inference(factor,[status(thm)],[c68]) ).
cnf(c65,negated_conjecture,
( ~ big_f(X198,skolem0002(X197,X198))
| ~ big_f(skolem0002(X197,X198),X198)
| big_f(X197,skolem0002(X197,X198))
| big_f(skolem0002(X197,X198),X197)
| ~ big_f(skolem0003(X197,X198),X198)
| big_f(skolem0001(X197),skolem0003(X197,X198))
| big_f(X198,skolem0003(X197,X198))
| ~ big_f(skolem0003(X197,X198),skolem0001(X197)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c425,plain,
( ~ big_f(skolem0001(X416),skolem0002(X416,skolem0001(X416)))
| ~ big_f(skolem0002(X416,skolem0001(X416)),skolem0001(X416))
| big_f(X416,skolem0002(X416,skolem0001(X416)))
| big_f(skolem0002(X416,skolem0001(X416)),X416)
| ~ big_f(skolem0003(X416,skolem0001(X416)),skolem0001(X416))
| big_f(skolem0001(X416),skolem0003(X416,skolem0001(X416))) ),
inference(factor,[status(thm)],[c65]) ).
cnf(c62,negated_conjecture,
( ~ big_f(X177,skolem0002(X176,X177))
| ~ big_f(skolem0002(X176,X177),X177)
| big_f(X176,skolem0002(X176,X177))
| big_f(skolem0002(X176,X177),X176)
| ~ big_f(skolem0001(X176),skolem0003(X176,X177))
| ~ big_f(skolem0003(X176,X177),X177)
| ~ big_f(X177,skolem0003(X176,X177))
| ~ big_f(skolem0003(X176,X177),skolem0001(X176)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c415,plain,
( ~ big_f(skolem0001(X413),skolem0002(X413,skolem0001(X413)))
| ~ big_f(skolem0002(X413,skolem0001(X413)),skolem0001(X413))
| big_f(X413,skolem0002(X413,skolem0001(X413)))
| big_f(skolem0002(X413,skolem0001(X413)),X413)
| ~ big_f(skolem0001(X413),skolem0003(X413,skolem0001(X413)))
| ~ big_f(skolem0003(X413,skolem0001(X413)),skolem0001(X413)) ),
inference(factor,[status(thm)],[c62]) ).
cnf(c60,negated_conjecture,
( ~ big_f(X163,skolem0002(X162,X163))
| ~ big_f(X162,skolem0002(X162,X163))
| big_f(skolem0002(X162,X163),X163)
| big_f(skolem0002(X162,X163),X162)
| ~ big_f(X163,skolem0003(X162,X163))
| ~ big_f(skolem0001(X162),skolem0003(X162,X163))
| big_f(skolem0003(X162,X163),X163)
| big_f(skolem0003(X162,X163),skolem0001(X162)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c408,plain,
( ~ big_f(skolem0001(X412),skolem0002(X412,skolem0001(X412)))
| ~ big_f(X412,skolem0002(X412,skolem0001(X412)))
| big_f(skolem0002(X412,skolem0001(X412)),skolem0001(X412))
| big_f(skolem0002(X412,skolem0001(X412)),X412)
| ~ big_f(skolem0001(X412),skolem0003(X412,skolem0001(X412)))
| big_f(skolem0003(X412,skolem0001(X412)),skolem0001(X412)) ),
inference(factor,[status(thm)],[c60]) ).
cnf(c57,negated_conjecture,
( ~ big_f(X142,skolem0002(X141,X142))
| ~ big_f(X141,skolem0002(X141,X142))
| big_f(skolem0002(X141,X142),X142)
| big_f(skolem0002(X141,X142),X141)
| ~ big_f(skolem0003(X141,X142),X142)
| big_f(skolem0001(X141),skolem0003(X141,X142))
| big_f(X142,skolem0003(X141,X142))
| ~ big_f(skolem0003(X141,X142),skolem0001(X141)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c291,plain,
( ~ big_f(skolem0001(X411),skolem0002(X411,skolem0001(X411)))
| ~ big_f(X411,skolem0002(X411,skolem0001(X411)))
| big_f(skolem0002(X411,skolem0001(X411)),skolem0001(X411))
| big_f(skolem0002(X411,skolem0001(X411)),X411)
| ~ big_f(skolem0003(X411,skolem0001(X411)),skolem0001(X411))
| big_f(skolem0001(X411),skolem0003(X411,skolem0001(X411))) ),
inference(factor,[status(thm)],[c57]) ).
cnf(c54,negated_conjecture,
( ~ big_f(X121,skolem0002(X120,X121))
| ~ big_f(X120,skolem0002(X120,X121))
| big_f(skolem0002(X120,X121),X121)
| big_f(skolem0002(X120,X121),X120)
| ~ big_f(skolem0001(X120),skolem0003(X120,X121))
| ~ big_f(skolem0003(X120,X121),X121)
| ~ big_f(X121,skolem0003(X120,X121))
| ~ big_f(skolem0003(X120,X121),skolem0001(X120)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c281,plain,
( ~ big_f(skolem0001(X410),skolem0002(X410,skolem0001(X410)))
| ~ big_f(X410,skolem0002(X410,skolem0001(X410)))
| big_f(skolem0002(X410,skolem0001(X410)),skolem0001(X410))
| big_f(skolem0002(X410,skolem0001(X410)),X410)
| ~ big_f(skolem0001(X410),skolem0003(X410,skolem0001(X410)))
| ~ big_f(skolem0003(X410,skolem0001(X410)),skolem0001(X410)) ),
inference(factor,[status(thm)],[c54]) ).
cnf(c49,negated_conjecture,
( big_f(X95,skolem0002(X95,X96))
| big_f(skolem0002(X95,X96),X96)
| big_f(X96,skolem0002(X95,X96))
| big_f(skolem0002(X95,X96),X95)
| ~ big_f(skolem0003(X95,X96),X96)
| big_f(skolem0001(X95),skolem0003(X95,X96))
| big_f(X96,skolem0003(X95,X96))
| ~ big_f(skolem0003(X95,X96),skolem0001(X95)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c88,plain,
( big_f(X335,skolem0002(X335,skolem0001(X335)))
| big_f(skolem0002(X335,skolem0001(X335)),skolem0001(X335))
| big_f(skolem0001(X335),skolem0002(X335,skolem0001(X335)))
| big_f(skolem0002(X335,skolem0001(X335)),X335)
| ~ big_f(skolem0003(X335,skolem0001(X335)),skolem0001(X335))
| big_f(skolem0001(X335),skolem0003(X335,skolem0001(X335))) ),
inference(factor,[status(thm)],[c49]) ).
cnf(c51,negated_conjecture,
( big_f(X99,skolem0002(X99,X100))
| big_f(skolem0002(X99,X100),X100)
| big_f(X100,skolem0002(X99,X100))
| big_f(skolem0002(X99,X100),X99)
| big_f(skolem0001(X99),skolem0003(X99,X100))
| big_f(skolem0003(X99,X100),X100)
| big_f(X100,skolem0003(X99,X100))
| big_f(skolem0003(X99,X100),skolem0001(X99)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c91,plain,
( big_f(X343,skolem0002(X343,skolem0001(X343)))
| big_f(skolem0002(X343,skolem0001(X343)),skolem0001(X343))
| big_f(skolem0001(X343),skolem0002(X343,skolem0001(X343)))
| big_f(skolem0002(X343,skolem0001(X343)),X343)
| big_f(skolem0001(X343),skolem0003(X343,skolem0001(X343)))
| big_f(skolem0003(X343,skolem0001(X343)),skolem0001(X343)) ),
inference(factor,[status(thm)],[c51]) ).
cnf(c552,plain,
( big_f(X344,skolem0002(X344,skolem0001(X344)))
| big_f(skolem0002(X344,skolem0001(X344)),skolem0001(X344))
| big_f(skolem0001(X344),skolem0002(X344,skolem0001(X344)))
| big_f(skolem0002(X344,skolem0001(X344)),X344)
| big_f(skolem0001(X344),skolem0003(X344,skolem0001(X344))) ),
inference(resolution,[status(thm)],[c91,c88]) ).
cnf(c46,negated_conjecture,
( big_f(X89,skolem0002(X89,X90))
| big_f(skolem0002(X89,X90),X90)
| big_f(X90,skolem0002(X89,X90))
| big_f(skolem0002(X89,X90),X89)
| ~ big_f(skolem0001(X89),skolem0003(X89,X90))
| ~ big_f(skolem0003(X89,X90),X90)
| ~ big_f(X90,skolem0003(X89,X90))
| ~ big_f(skolem0003(X89,X90),skolem0001(X89)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c87,plain,
( big_f(X326,skolem0002(X326,skolem0001(X326)))
| big_f(skolem0002(X326,skolem0001(X326)),skolem0001(X326))
| big_f(skolem0001(X326),skolem0002(X326,skolem0001(X326)))
| big_f(skolem0002(X326,skolem0001(X326)),X326)
| ~ big_f(skolem0001(X326),skolem0003(X326,skolem0001(X326)))
| ~ big_f(skolem0003(X326,skolem0001(X326)),skolem0001(X326)) ),
inference(factor,[status(thm)],[c46]) ).
cnf(c52,negated_conjecture,
( big_f(X106,skolem0002(X106,X107))
| big_f(skolem0002(X106,X107),X107)
| big_f(X107,skolem0002(X106,X107))
| big_f(skolem0002(X106,X107),X106)
| ~ big_f(X107,skolem0003(X106,X107))
| ~ big_f(skolem0001(X106),skolem0003(X106,X107))
| big_f(skolem0003(X106,X107),X107)
| big_f(skolem0003(X106,X107),skolem0001(X106)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c274,plain,
( big_f(X402,skolem0002(X402,skolem0001(X402)))
| big_f(skolem0002(X402,skolem0001(X402)),skolem0001(X402))
| big_f(skolem0001(X402),skolem0002(X402,skolem0001(X402)))
| big_f(skolem0002(X402,skolem0001(X402)),X402)
| ~ big_f(skolem0001(X402),skolem0003(X402,skolem0001(X402)))
| big_f(skolem0003(X402,skolem0001(X402)),skolem0001(X402)) ),
inference(factor,[status(thm)],[c52]) ).
cnf(c584,plain,
( big_f(X403,skolem0002(X403,skolem0001(X403)))
| big_f(skolem0002(X403,skolem0001(X403)),skolem0001(X403))
| big_f(skolem0001(X403),skolem0002(X403,skolem0001(X403)))
| big_f(skolem0002(X403,skolem0001(X403)),X403)
| big_f(skolem0003(X403,skolem0001(X403)),skolem0001(X403)) ),
inference(resolution,[status(thm)],[c274,c552]) ).
cnf(c609,plain,
( big_f(X404,skolem0002(X404,skolem0001(X404)))
| big_f(skolem0002(X404,skolem0001(X404)),skolem0001(X404))
| big_f(skolem0001(X404),skolem0002(X404,skolem0001(X404)))
| big_f(skolem0002(X404,skolem0001(X404)),X404)
| ~ big_f(skolem0001(X404),skolem0003(X404,skolem0001(X404))) ),
inference(resolution,[status(thm)],[c584,c87]) ).
cnf(c645,plain,
( big_f(X405,skolem0002(X405,skolem0001(X405)))
| big_f(skolem0002(X405,skolem0001(X405)),skolem0001(X405))
| big_f(skolem0001(X405),skolem0002(X405,skolem0001(X405)))
| big_f(skolem0002(X405,skolem0001(X405)),X405) ),
inference(resolution,[status(thm)],[c609,c552]) ).
cnf(c44,negated_conjecture,
( ~ big_f(X85,skolem0002(X85,X86))
| ~ big_f(skolem0002(X85,X86),X86)
| big_f(X86,skolem0002(X85,X86))
| big_f(skolem0002(X85,X86),X85)
| ~ big_f(X86,skolem0003(X85,X86))
| ~ big_f(skolem0001(X85),skolem0003(X85,X86))
| big_f(skolem0003(X85,X86),X86)
| big_f(skolem0003(X85,X86),skolem0001(X85)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c86,plain,
( ~ big_f(X320,skolem0002(X320,skolem0001(X320)))
| ~ big_f(skolem0002(X320,skolem0001(X320)),skolem0001(X320))
| big_f(skolem0001(X320),skolem0002(X320,skolem0001(X320)))
| big_f(skolem0002(X320,skolem0001(X320)),X320)
| ~ big_f(skolem0001(X320),skolem0003(X320,skolem0001(X320)))
| big_f(skolem0003(X320,skolem0001(X320)),skolem0001(X320)) ),
inference(factor,[status(thm)],[c44]) ).
cnf(c41,negated_conjecture,
( ~ big_f(X79,skolem0002(X79,X80))
| ~ big_f(skolem0002(X79,X80),X80)
| big_f(X80,skolem0002(X79,X80))
| big_f(skolem0002(X79,X80),X79)
| ~ big_f(skolem0003(X79,X80),X80)
| big_f(skolem0001(X79),skolem0003(X79,X80))
| big_f(X80,skolem0003(X79,X80))
| ~ big_f(skolem0003(X79,X80),skolem0001(X79)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c85,plain,
( ~ big_f(X314,skolem0002(X314,skolem0001(X314)))
| ~ big_f(skolem0002(X314,skolem0001(X314)),skolem0001(X314))
| big_f(skolem0001(X314),skolem0002(X314,skolem0001(X314)))
| big_f(skolem0002(X314,skolem0001(X314)),X314)
| ~ big_f(skolem0003(X314,skolem0001(X314)),skolem0001(X314))
| big_f(skolem0001(X314),skolem0003(X314,skolem0001(X314))) ),
inference(factor,[status(thm)],[c41]) ).
cnf(c38,negated_conjecture,
( ~ big_f(X73,skolem0002(X73,X74))
| ~ big_f(skolem0002(X73,X74),X74)
| big_f(X74,skolem0002(X73,X74))
| big_f(skolem0002(X73,X74),X73)
| ~ big_f(skolem0001(X73),skolem0003(X73,X74))
| ~ big_f(skolem0003(X73,X74),X74)
| ~ big_f(X74,skolem0003(X73,X74))
| ~ big_f(skolem0003(X73,X74),skolem0001(X73)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c84,plain,
( ~ big_f(X308,skolem0002(X308,skolem0001(X308)))
| ~ big_f(skolem0002(X308,skolem0001(X308)),skolem0001(X308))
| big_f(skolem0001(X308),skolem0002(X308,skolem0001(X308)))
| big_f(skolem0002(X308,skolem0001(X308)),X308)
| ~ big_f(skolem0001(X308),skolem0003(X308,skolem0001(X308)))
| ~ big_f(skolem0003(X308,skolem0001(X308)),skolem0001(X308)) ),
inference(factor,[status(thm)],[c38]) ).
cnf(c36,negated_conjecture,
( ~ big_f(skolem0002(X69,X70),X70)
| big_f(X69,skolem0002(X69,X70))
| big_f(X70,skolem0002(X69,X70))
| ~ big_f(skolem0002(X69,X70),X69)
| ~ big_f(X70,skolem0003(X69,X70))
| ~ big_f(skolem0001(X69),skolem0003(X69,X70))
| big_f(skolem0003(X69,X70),X70)
| big_f(skolem0003(X69,X70),skolem0001(X69)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c83,plain,
( ~ big_f(skolem0002(X302,skolem0001(X302)),skolem0001(X302))
| big_f(X302,skolem0002(X302,skolem0001(X302)))
| big_f(skolem0001(X302),skolem0002(X302,skolem0001(X302)))
| ~ big_f(skolem0002(X302,skolem0001(X302)),X302)
| ~ big_f(skolem0001(X302),skolem0003(X302,skolem0001(X302)))
| big_f(skolem0003(X302,skolem0001(X302)),skolem0001(X302)) ),
inference(factor,[status(thm)],[c36]) ).
cnf(c33,negated_conjecture,
( ~ big_f(skolem0002(X62,X63),X63)
| big_f(X62,skolem0002(X62,X63))
| big_f(X63,skolem0002(X62,X63))
| ~ big_f(skolem0002(X62,X63),X62)
| ~ big_f(skolem0003(X62,X63),X63)
| big_f(skolem0001(X62),skolem0003(X62,X63))
| big_f(X63,skolem0003(X62,X63))
| ~ big_f(skolem0003(X62,X63),skolem0001(X62)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c81,plain,
( ~ big_f(skolem0002(X296,skolem0001(X296)),skolem0001(X296))
| big_f(X296,skolem0002(X296,skolem0001(X296)))
| big_f(skolem0001(X296),skolem0002(X296,skolem0001(X296)))
| ~ big_f(skolem0002(X296,skolem0001(X296)),X296)
| ~ big_f(skolem0003(X296,skolem0001(X296)),skolem0001(X296))
| big_f(skolem0001(X296),skolem0003(X296,skolem0001(X296))) ),
inference(factor,[status(thm)],[c33]) ).
cnf(c30,negated_conjecture,
( ~ big_f(skolem0002(X56,X57),X57)
| big_f(X56,skolem0002(X56,X57))
| big_f(X57,skolem0002(X56,X57))
| ~ big_f(skolem0002(X56,X57),X56)
| ~ big_f(skolem0001(X56),skolem0003(X56,X57))
| ~ big_f(skolem0003(X56,X57),X57)
| ~ big_f(X57,skolem0003(X56,X57))
| ~ big_f(skolem0003(X56,X57),skolem0001(X56)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c80,plain,
( ~ big_f(skolem0002(X289,skolem0001(X289)),skolem0001(X289))
| big_f(X289,skolem0002(X289,skolem0001(X289)))
| big_f(skolem0001(X289),skolem0002(X289,skolem0001(X289)))
| ~ big_f(skolem0002(X289,skolem0001(X289)),X289)
| ~ big_f(skolem0001(X289),skolem0003(X289,skolem0001(X289)))
| ~ big_f(skolem0003(X289,skolem0001(X289)),skolem0001(X289)) ),
inference(factor,[status(thm)],[c30]) ).
cnf(c28,negated_conjecture,
( ~ big_f(X52,skolem0002(X52,X53))
| big_f(skolem0002(X52,X53),X53)
| big_f(X53,skolem0002(X52,X53))
| ~ big_f(skolem0002(X52,X53),X52)
| ~ big_f(X53,skolem0003(X52,X53))
| ~ big_f(skolem0001(X52),skolem0003(X52,X53))
| big_f(skolem0003(X52,X53),X53)
| big_f(skolem0003(X52,X53),skolem0001(X52)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c79,plain,
( ~ big_f(X283,skolem0002(X283,skolem0001(X283)))
| big_f(skolem0002(X283,skolem0001(X283)),skolem0001(X283))
| big_f(skolem0001(X283),skolem0002(X283,skolem0001(X283)))
| ~ big_f(skolem0002(X283,skolem0001(X283)),X283)
| ~ big_f(skolem0001(X283),skolem0003(X283,skolem0001(X283)))
| big_f(skolem0003(X283,skolem0001(X283)),skolem0001(X283)) ),
inference(factor,[status(thm)],[c28]) ).
cnf(c25,negated_conjecture,
( ~ big_f(X46,skolem0002(X46,X47))
| big_f(skolem0002(X46,X47),X47)
| big_f(X47,skolem0002(X46,X47))
| ~ big_f(skolem0002(X46,X47),X46)
| ~ big_f(skolem0003(X46,X47),X47)
| big_f(skolem0001(X46),skolem0003(X46,X47))
| big_f(X47,skolem0003(X46,X47))
| ~ big_f(skolem0003(X46,X47),skolem0001(X46)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c78,plain,
( ~ big_f(X277,skolem0002(X277,skolem0001(X277)))
| big_f(skolem0002(X277,skolem0001(X277)),skolem0001(X277))
| big_f(skolem0001(X277),skolem0002(X277,skolem0001(X277)))
| ~ big_f(skolem0002(X277,skolem0001(X277)),X277)
| ~ big_f(skolem0003(X277,skolem0001(X277)),skolem0001(X277))
| big_f(skolem0001(X277),skolem0003(X277,skolem0001(X277))) ),
inference(factor,[status(thm)],[c25]) ).
cnf(c22,negated_conjecture,
( ~ big_f(X40,skolem0002(X40,X41))
| big_f(skolem0002(X40,X41),X41)
| big_f(X41,skolem0002(X40,X41))
| ~ big_f(skolem0002(X40,X41),X40)
| ~ big_f(skolem0001(X40),skolem0003(X40,X41))
| ~ big_f(skolem0003(X40,X41),X41)
| ~ big_f(X41,skolem0003(X40,X41))
| ~ big_f(skolem0003(X40,X41),skolem0001(X40)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c77,plain,
( ~ big_f(X271,skolem0002(X271,skolem0001(X271)))
| big_f(skolem0002(X271,skolem0001(X271)),skolem0001(X271))
| big_f(skolem0001(X271),skolem0002(X271,skolem0001(X271)))
| ~ big_f(skolem0002(X271,skolem0001(X271)),X271)
| ~ big_f(skolem0001(X271),skolem0003(X271,skolem0001(X271)))
| ~ big_f(skolem0003(X271,skolem0001(X271)),skolem0001(X271)) ),
inference(factor,[status(thm)],[c22]) ).
cnf(c20,negated_conjecture,
( big_f(X36,skolem0002(X36,X37))
| big_f(skolem0002(X36,X37),X37)
| ~ big_f(X37,skolem0002(X36,X37))
| ~ big_f(skolem0002(X36,X37),X36)
| ~ big_f(X37,skolem0003(X36,X37))
| ~ big_f(skolem0001(X36),skolem0003(X36,X37))
| big_f(skolem0003(X36,X37),X37)
| big_f(skolem0003(X36,X37),skolem0001(X36)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c76,plain,
( big_f(X265,skolem0002(X265,skolem0001(X265)))
| big_f(skolem0002(X265,skolem0001(X265)),skolem0001(X265))
| ~ big_f(skolem0001(X265),skolem0002(X265,skolem0001(X265)))
| ~ big_f(skolem0002(X265,skolem0001(X265)),X265)
| ~ big_f(skolem0001(X265),skolem0003(X265,skolem0001(X265)))
| big_f(skolem0003(X265,skolem0001(X265)),skolem0001(X265)) ),
inference(factor,[status(thm)],[c20]) ).
cnf(c17,negated_conjecture,
( big_f(X30,skolem0002(X30,X31))
| big_f(skolem0002(X30,X31),X31)
| ~ big_f(X31,skolem0002(X30,X31))
| ~ big_f(skolem0002(X30,X31),X30)
| ~ big_f(skolem0003(X30,X31),X31)
| big_f(skolem0001(X30),skolem0003(X30,X31))
| big_f(X31,skolem0003(X30,X31))
| ~ big_f(skolem0003(X30,X31),skolem0001(X30)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c75,plain,
( big_f(X259,skolem0002(X259,skolem0001(X259)))
| big_f(skolem0002(X259,skolem0001(X259)),skolem0001(X259))
| ~ big_f(skolem0001(X259),skolem0002(X259,skolem0001(X259)))
| ~ big_f(skolem0002(X259,skolem0001(X259)),X259)
| ~ big_f(skolem0003(X259,skolem0001(X259)),skolem0001(X259))
| big_f(skolem0001(X259),skolem0003(X259,skolem0001(X259))) ),
inference(factor,[status(thm)],[c17]) ).
cnf(c14,negated_conjecture,
( big_f(X24,skolem0002(X24,X25))
| big_f(skolem0002(X24,X25),X25)
| ~ big_f(X25,skolem0002(X24,X25))
| ~ big_f(skolem0002(X24,X25),X24)
| ~ big_f(skolem0001(X24),skolem0003(X24,X25))
| ~ big_f(skolem0003(X24,X25),X25)
| ~ big_f(X25,skolem0003(X24,X25))
| ~ big_f(skolem0003(X24,X25),skolem0001(X24)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c74,plain,
( big_f(X250,skolem0002(X250,skolem0001(X250)))
| big_f(skolem0002(X250,skolem0001(X250)),skolem0001(X250))
| ~ big_f(skolem0001(X250),skolem0002(X250,skolem0001(X250)))
| ~ big_f(skolem0002(X250,skolem0001(X250)),X250)
| ~ big_f(skolem0001(X250),skolem0003(X250,skolem0001(X250)))
| ~ big_f(skolem0003(X250,skolem0001(X250)),skolem0001(X250)) ),
inference(factor,[status(thm)],[c14]) ).
cnf(c12,negated_conjecture,
( ~ big_f(X20,skolem0002(X20,X21))
| ~ big_f(skolem0002(X20,X21),X21)
| ~ big_f(X21,skolem0002(X20,X21))
| ~ big_f(skolem0002(X20,X21),X20)
| ~ big_f(X21,skolem0003(X20,X21))
| ~ big_f(skolem0001(X20),skolem0003(X20,X21))
| big_f(skolem0003(X20,X21),X21)
| big_f(skolem0003(X20,X21),skolem0001(X20)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c73,plain,
( ~ big_f(X244,skolem0002(X244,skolem0001(X244)))
| ~ big_f(skolem0002(X244,skolem0001(X244)),skolem0001(X244))
| ~ big_f(skolem0001(X244),skolem0002(X244,skolem0001(X244)))
| ~ big_f(skolem0002(X244,skolem0001(X244)),X244)
| ~ big_f(skolem0001(X244),skolem0003(X244,skolem0001(X244)))
| big_f(skolem0003(X244,skolem0001(X244)),skolem0001(X244)) ),
inference(factor,[status(thm)],[c12]) ).
cnf(c9,negated_conjecture,
( ~ big_f(X13,skolem0002(X13,X14))
| ~ big_f(skolem0002(X13,X14),X14)
| ~ big_f(X14,skolem0002(X13,X14))
| ~ big_f(skolem0002(X13,X14),X13)
| ~ big_f(skolem0003(X13,X14),X14)
| big_f(skolem0001(X13),skolem0003(X13,X14))
| big_f(X14,skolem0003(X13,X14))
| ~ big_f(skolem0003(X13,X14),skolem0001(X13)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c71,plain,
( ~ big_f(X238,skolem0002(X238,skolem0001(X238)))
| ~ big_f(skolem0002(X238,skolem0001(X238)),skolem0001(X238))
| ~ big_f(skolem0001(X238),skolem0002(X238,skolem0001(X238)))
| ~ big_f(skolem0002(X238,skolem0001(X238)),X238)
| ~ big_f(skolem0003(X238,skolem0001(X238)),skolem0001(X238))
| big_f(skolem0001(X238),skolem0003(X238,skolem0001(X238))) ),
inference(factor,[status(thm)],[c9]) ).
cnf(c6,negated_conjecture,
( ~ big_f(X7,skolem0002(X7,X8))
| ~ big_f(skolem0002(X7,X8),X8)
| ~ big_f(X8,skolem0002(X7,X8))
| ~ big_f(skolem0002(X7,X8),X7)
| ~ big_f(skolem0001(X7),skolem0003(X7,X8))
| ~ big_f(skolem0003(X7,X8),X8)
| ~ big_f(X8,skolem0003(X7,X8))
| ~ big_f(skolem0003(X7,X8),skolem0001(X7)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c70,plain,
( ~ big_f(X232,skolem0002(X232,skolem0001(X232)))
| ~ big_f(skolem0002(X232,skolem0001(X232)),skolem0001(X232))
| ~ big_f(skolem0001(X232),skolem0002(X232,skolem0001(X232)))
| ~ big_f(skolem0002(X232,skolem0001(X232)),X232)
| ~ big_f(skolem0001(X232),skolem0003(X232,skolem0001(X232)))
| ~ big_f(skolem0003(X232,skolem0001(X232)),skolem0001(X232)) ),
inference(factor,[status(thm)],[c6]) ).
cnf(c69,negated_conjecture,
( ~ big_f(X226,skolem0002(X225,X226))
| ~ big_f(skolem0002(X225,X226),X226)
| big_f(X225,skolem0002(X225,X226))
| big_f(skolem0002(X225,X226),X225)
| ~ big_f(X226,skolem0003(X225,X226))
| ~ big_f(skolem0003(X225,X226),X226)
| big_f(skolem0001(X225),skolem0003(X225,X226))
| big_f(skolem0003(X225,X226),skolem0001(X225)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c67,negated_conjecture,
( ~ big_f(X212,skolem0002(X211,X212))
| ~ big_f(skolem0002(X211,X212),X212)
| big_f(X211,skolem0002(X211,X212))
| big_f(skolem0002(X211,X212),X211)
| big_f(skolem0001(X211),skolem0003(X211,X212))
| big_f(skolem0003(X211,X212),X212)
| big_f(X212,skolem0003(X211,X212))
| big_f(skolem0003(X211,X212),skolem0001(X211)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c66,negated_conjecture,
( ~ big_f(X205,skolem0002(X204,X205))
| ~ big_f(skolem0002(X204,X205),X205)
| big_f(X204,skolem0002(X204,X205))
| big_f(skolem0002(X204,X205),X204)
| ~ big_f(skolem0001(X204),skolem0003(X204,X205))
| ~ big_f(skolem0003(X204,X205),X205)
| big_f(X205,skolem0003(X204,X205))
| big_f(skolem0003(X204,X205),skolem0001(X204)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c64,negated_conjecture,
( ~ big_f(X191,skolem0002(X190,X191))
| ~ big_f(skolem0002(X190,X191),X191)
| big_f(X190,skolem0002(X190,X191))
| big_f(skolem0002(X190,X191),X190)
| ~ big_f(skolem0001(X190),skolem0003(X190,X191))
| big_f(skolem0003(X190,X191),X191)
| big_f(X191,skolem0003(X190,X191))
| ~ big_f(skolem0003(X190,X191),skolem0001(X190)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c63,negated_conjecture,
( ~ big_f(X184,skolem0002(X183,X184))
| ~ big_f(skolem0002(X183,X184),X184)
| big_f(X183,skolem0002(X183,X184))
| big_f(skolem0002(X183,X184),X183)
| big_f(skolem0001(X183),skolem0003(X183,X184))
| big_f(skolem0003(X183,X184),X184)
| ~ big_f(X184,skolem0003(X183,X184))
| ~ big_f(skolem0003(X183,X184),skolem0001(X183)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c61,negated_conjecture,
( ~ big_f(X170,skolem0002(X169,X170))
| ~ big_f(X169,skolem0002(X169,X170))
| big_f(skolem0002(X169,X170),X170)
| big_f(skolem0002(X169,X170),X169)
| ~ big_f(X170,skolem0003(X169,X170))
| ~ big_f(skolem0003(X169,X170),X170)
| big_f(skolem0001(X169),skolem0003(X169,X170))
| big_f(skolem0003(X169,X170),skolem0001(X169)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c35,negated_conjecture,
( ~ big_f(skolem0002(X66,X67),X67)
| big_f(X66,skolem0002(X66,X67))
| big_f(X67,skolem0002(X66,X67))
| ~ big_f(skolem0002(X66,X67),X66)
| big_f(skolem0001(X66),skolem0003(X66,X67))
| big_f(skolem0003(X66,X67),X67)
| big_f(X67,skolem0003(X66,X67))
| big_f(skolem0003(X66,X67),skolem0001(X66)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c82,plain,
( ~ big_f(skolem0002(X68,X68),X68)
| big_f(X68,skolem0002(X68,X68))
| big_f(skolem0001(X68),skolem0003(X68,X68))
| big_f(skolem0003(X68,X68),X68)
| big_f(X68,skolem0003(X68,X68))
| big_f(skolem0003(X68,X68),skolem0001(X68)) ),
inference(factor,[status(thm)],[c35]) ).
cnf(c89,plain,
( big_f(X101,skolem0002(X101,X101))
| big_f(skolem0002(X101,X101),X101)
| big_f(skolem0001(X101),skolem0003(X101,X101))
| big_f(skolem0003(X101,X101),X101)
| big_f(X101,skolem0003(X101,X101))
| big_f(skolem0003(X101,X101),skolem0001(X101)) ),
inference(factor,[status(thm)],[c51]) ).
cnf(c189,plain,
( big_f(X102,skolem0002(X102,X102))
| big_f(skolem0001(X102),skolem0003(X102,X102))
| big_f(skolem0003(X102,X102),X102)
| big_f(X102,skolem0003(X102,X102))
| big_f(skolem0003(X102,X102),skolem0001(X102)) ),
inference(resolution,[status(thm)],[c89,c82]) ).
cnf(c11,negated_conjecture,
( ~ big_f(X17,skolem0002(X17,X18))
| ~ big_f(skolem0002(X17,X18),X18)
| ~ big_f(X18,skolem0002(X17,X18))
| ~ big_f(skolem0002(X17,X18),X17)
| big_f(skolem0001(X17),skolem0003(X17,X18))
| big_f(skolem0003(X17,X18),X18)
| big_f(X18,skolem0003(X17,X18))
| big_f(skolem0003(X17,X18),skolem0001(X17)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c72,plain,
( ~ big_f(X19,skolem0002(X19,X19))
| ~ big_f(skolem0002(X19,X19),X19)
| big_f(skolem0001(X19),skolem0003(X19,X19))
| big_f(skolem0003(X19,X19),X19)
| big_f(X19,skolem0003(X19,X19))
| big_f(skolem0003(X19,X19),skolem0001(X19)) ),
inference(factor,[status(thm)],[c11]) ).
cnf(c59,negated_conjecture,
( ~ big_f(X156,skolem0002(X155,X156))
| ~ big_f(X155,skolem0002(X155,X156))
| big_f(skolem0002(X155,X156),X156)
| big_f(skolem0002(X155,X156),X155)
| big_f(skolem0001(X155),skolem0003(X155,X156))
| big_f(skolem0003(X155,X156),X156)
| big_f(X156,skolem0003(X155,X156))
| big_f(skolem0003(X155,X156),skolem0001(X155)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c298,plain,
( ~ big_f(X157,skolem0002(X157,X157))
| big_f(skolem0002(X157,X157),X157)
| big_f(skolem0001(X157),skolem0003(X157,X157))
| big_f(skolem0003(X157,X157),X157)
| big_f(X157,skolem0003(X157,X157))
| big_f(skolem0003(X157,X157),skolem0001(X157)) ),
inference(factor,[status(thm)],[c59]) ).
cnf(c303,plain,
( big_f(skolem0002(X158,X158),X158)
| big_f(skolem0001(X158),skolem0003(X158,X158))
| big_f(skolem0003(X158,X158),X158)
| big_f(X158,skolem0003(X158,X158))
| big_f(skolem0003(X158,X158),skolem0001(X158)) ),
inference(resolution,[status(thm)],[c298,c189]) ).
cnf(c305,plain,
( big_f(skolem0001(X159),skolem0003(X159,X159))
| big_f(skolem0003(X159,X159),X159)
| big_f(X159,skolem0003(X159,X159))
| big_f(skolem0003(X159,X159),skolem0001(X159))
| ~ big_f(X159,skolem0002(X159,X159)) ),
inference(resolution,[status(thm)],[c303,c72]) ).
cnf(c359,plain,
( big_f(skolem0001(X160),skolem0003(X160,X160))
| big_f(skolem0003(X160,X160),X160)
| big_f(X160,skolem0003(X160,X160))
| big_f(skolem0003(X160,X160),skolem0001(X160)) ),
inference(resolution,[status(thm)],[c305,c189]) ).
cnf(c58,negated_conjecture,
( ~ big_f(X149,skolem0002(X148,X149))
| ~ big_f(X148,skolem0002(X148,X149))
| big_f(skolem0002(X148,X149),X149)
| big_f(skolem0002(X148,X149),X148)
| ~ big_f(skolem0001(X148),skolem0003(X148,X149))
| ~ big_f(skolem0003(X148,X149),X149)
| big_f(X149,skolem0003(X148,X149))
| big_f(skolem0003(X148,X149),skolem0001(X148)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c56,negated_conjecture,
( ~ big_f(X135,skolem0002(X134,X135))
| ~ big_f(X134,skolem0002(X134,X135))
| big_f(skolem0002(X134,X135),X135)
| big_f(skolem0002(X134,X135),X134)
| ~ big_f(skolem0001(X134),skolem0003(X134,X135))
| big_f(skolem0003(X134,X135),X135)
| big_f(X135,skolem0003(X134,X135))
| ~ big_f(skolem0003(X134,X135),skolem0001(X134)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c55,negated_conjecture,
( ~ big_f(X128,skolem0002(X127,X128))
| ~ big_f(X127,skolem0002(X127,X128))
| big_f(skolem0002(X127,X128),X128)
| big_f(skolem0002(X127,X128),X127)
| big_f(skolem0001(X127),skolem0003(X127,X128))
| big_f(skolem0003(X127,X128),X128)
| ~ big_f(X128,skolem0003(X127,X128))
| ~ big_f(skolem0003(X127,X128),skolem0001(X127)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c53,negated_conjecture,
( big_f(X113,skolem0002(X113,X114))
| big_f(skolem0002(X113,X114),X114)
| big_f(X114,skolem0002(X113,X114))
| big_f(skolem0002(X113,X114),X113)
| ~ big_f(X114,skolem0003(X113,X114))
| ~ big_f(skolem0003(X113,X114),X114)
| big_f(skolem0001(X113),skolem0003(X113,X114))
| big_f(skolem0003(X113,X114),skolem0001(X113)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c50,negated_conjecture,
( big_f(X97,skolem0002(X97,X98))
| big_f(skolem0002(X97,X98),X98)
| big_f(X98,skolem0002(X97,X98))
| big_f(skolem0002(X97,X98),X97)
| ~ big_f(skolem0001(X97),skolem0003(X97,X98))
| ~ big_f(skolem0003(X97,X98),X98)
| big_f(X98,skolem0003(X97,X98))
| big_f(skolem0003(X97,X98),skolem0001(X97)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c48,negated_conjecture,
( big_f(X93,skolem0002(X93,X94))
| big_f(skolem0002(X93,X94),X94)
| big_f(X94,skolem0002(X93,X94))
| big_f(skolem0002(X93,X94),X93)
| ~ big_f(skolem0001(X93),skolem0003(X93,X94))
| big_f(skolem0003(X93,X94),X94)
| big_f(X94,skolem0003(X93,X94))
| ~ big_f(skolem0003(X93,X94),skolem0001(X93)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c47,negated_conjecture,
( big_f(X91,skolem0002(X91,X92))
| big_f(skolem0002(X91,X92),X92)
| big_f(X92,skolem0002(X91,X92))
| big_f(skolem0002(X91,X92),X91)
| big_f(skolem0001(X91),skolem0003(X91,X92))
| big_f(skolem0003(X91,X92),X92)
| ~ big_f(X92,skolem0003(X91,X92))
| ~ big_f(skolem0003(X91,X92),skolem0001(X91)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c45,negated_conjecture,
( ~ big_f(X87,skolem0002(X87,X88))
| ~ big_f(skolem0002(X87,X88),X88)
| big_f(X88,skolem0002(X87,X88))
| big_f(skolem0002(X87,X88),X87)
| ~ big_f(X88,skolem0003(X87,X88))
| ~ big_f(skolem0003(X87,X88),X88)
| big_f(skolem0001(X87),skolem0003(X87,X88))
| big_f(skolem0003(X87,X88),skolem0001(X87)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c43,negated_conjecture,
( ~ big_f(X83,skolem0002(X83,X84))
| ~ big_f(skolem0002(X83,X84),X84)
| big_f(X84,skolem0002(X83,X84))
| big_f(skolem0002(X83,X84),X83)
| big_f(skolem0001(X83),skolem0003(X83,X84))
| big_f(skolem0003(X83,X84),X84)
| big_f(X84,skolem0003(X83,X84))
| big_f(skolem0003(X83,X84),skolem0001(X83)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c42,negated_conjecture,
( ~ big_f(X81,skolem0002(X81,X82))
| ~ big_f(skolem0002(X81,X82),X82)
| big_f(X82,skolem0002(X81,X82))
| big_f(skolem0002(X81,X82),X81)
| ~ big_f(skolem0001(X81),skolem0003(X81,X82))
| ~ big_f(skolem0003(X81,X82),X82)
| big_f(X82,skolem0003(X81,X82))
| big_f(skolem0003(X81,X82),skolem0001(X81)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c40,negated_conjecture,
( ~ big_f(X77,skolem0002(X77,X78))
| ~ big_f(skolem0002(X77,X78),X78)
| big_f(X78,skolem0002(X77,X78))
| big_f(skolem0002(X77,X78),X77)
| ~ big_f(skolem0001(X77),skolem0003(X77,X78))
| big_f(skolem0003(X77,X78),X78)
| big_f(X78,skolem0003(X77,X78))
| ~ big_f(skolem0003(X77,X78),skolem0001(X77)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c39,negated_conjecture,
( ~ big_f(X75,skolem0002(X75,X76))
| ~ big_f(skolem0002(X75,X76),X76)
| big_f(X76,skolem0002(X75,X76))
| big_f(skolem0002(X75,X76),X75)
| big_f(skolem0001(X75),skolem0003(X75,X76))
| big_f(skolem0003(X75,X76),X76)
| ~ big_f(X76,skolem0003(X75,X76))
| ~ big_f(skolem0003(X75,X76),skolem0001(X75)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c37,negated_conjecture,
( ~ big_f(skolem0002(X71,X72),X72)
| big_f(X71,skolem0002(X71,X72))
| big_f(X72,skolem0002(X71,X72))
| ~ big_f(skolem0002(X71,X72),X71)
| ~ big_f(X72,skolem0003(X71,X72))
| ~ big_f(skolem0003(X71,X72),X72)
| big_f(skolem0001(X71),skolem0003(X71,X72))
| big_f(skolem0003(X71,X72),skolem0001(X71)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c34,negated_conjecture,
( ~ big_f(skolem0002(X64,X65),X65)
| big_f(X64,skolem0002(X64,X65))
| big_f(X65,skolem0002(X64,X65))
| ~ big_f(skolem0002(X64,X65),X64)
| ~ big_f(skolem0001(X64),skolem0003(X64,X65))
| ~ big_f(skolem0003(X64,X65),X65)
| big_f(X65,skolem0003(X64,X65))
| big_f(skolem0003(X64,X65),skolem0001(X64)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c32,negated_conjecture,
( ~ big_f(skolem0002(X60,X61),X61)
| big_f(X60,skolem0002(X60,X61))
| big_f(X61,skolem0002(X60,X61))
| ~ big_f(skolem0002(X60,X61),X60)
| ~ big_f(skolem0001(X60),skolem0003(X60,X61))
| big_f(skolem0003(X60,X61),X61)
| big_f(X61,skolem0003(X60,X61))
| ~ big_f(skolem0003(X60,X61),skolem0001(X60)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c31,negated_conjecture,
( ~ big_f(skolem0002(X58,X59),X59)
| big_f(X58,skolem0002(X58,X59))
| big_f(X59,skolem0002(X58,X59))
| ~ big_f(skolem0002(X58,X59),X58)
| big_f(skolem0001(X58),skolem0003(X58,X59))
| big_f(skolem0003(X58,X59),X59)
| ~ big_f(X59,skolem0003(X58,X59))
| ~ big_f(skolem0003(X58,X59),skolem0001(X58)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c29,negated_conjecture,
( ~ big_f(X54,skolem0002(X54,X55))
| big_f(skolem0002(X54,X55),X55)
| big_f(X55,skolem0002(X54,X55))
| ~ big_f(skolem0002(X54,X55),X54)
| ~ big_f(X55,skolem0003(X54,X55))
| ~ big_f(skolem0003(X54,X55),X55)
| big_f(skolem0001(X54),skolem0003(X54,X55))
| big_f(skolem0003(X54,X55),skolem0001(X54)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c27,negated_conjecture,
( ~ big_f(X50,skolem0002(X50,X51))
| big_f(skolem0002(X50,X51),X51)
| big_f(X51,skolem0002(X50,X51))
| ~ big_f(skolem0002(X50,X51),X50)
| big_f(skolem0001(X50),skolem0003(X50,X51))
| big_f(skolem0003(X50,X51),X51)
| big_f(X51,skolem0003(X50,X51))
| big_f(skolem0003(X50,X51),skolem0001(X50)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c26,negated_conjecture,
( ~ big_f(X48,skolem0002(X48,X49))
| big_f(skolem0002(X48,X49),X49)
| big_f(X49,skolem0002(X48,X49))
| ~ big_f(skolem0002(X48,X49),X48)
| ~ big_f(skolem0001(X48),skolem0003(X48,X49))
| ~ big_f(skolem0003(X48,X49),X49)
| big_f(X49,skolem0003(X48,X49))
| big_f(skolem0003(X48,X49),skolem0001(X48)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c24,negated_conjecture,
( ~ big_f(X44,skolem0002(X44,X45))
| big_f(skolem0002(X44,X45),X45)
| big_f(X45,skolem0002(X44,X45))
| ~ big_f(skolem0002(X44,X45),X44)
| ~ big_f(skolem0001(X44),skolem0003(X44,X45))
| big_f(skolem0003(X44,X45),X45)
| big_f(X45,skolem0003(X44,X45))
| ~ big_f(skolem0003(X44,X45),skolem0001(X44)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c23,negated_conjecture,
( ~ big_f(X42,skolem0002(X42,X43))
| big_f(skolem0002(X42,X43),X43)
| big_f(X43,skolem0002(X42,X43))
| ~ big_f(skolem0002(X42,X43),X42)
| big_f(skolem0001(X42),skolem0003(X42,X43))
| big_f(skolem0003(X42,X43),X43)
| ~ big_f(X43,skolem0003(X42,X43))
| ~ big_f(skolem0003(X42,X43),skolem0001(X42)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c21,negated_conjecture,
( big_f(X38,skolem0002(X38,X39))
| big_f(skolem0002(X38,X39),X39)
| ~ big_f(X39,skolem0002(X38,X39))
| ~ big_f(skolem0002(X38,X39),X38)
| ~ big_f(X39,skolem0003(X38,X39))
| ~ big_f(skolem0003(X38,X39),X39)
| big_f(skolem0001(X38),skolem0003(X38,X39))
| big_f(skolem0003(X38,X39),skolem0001(X38)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c19,negated_conjecture,
( big_f(X34,skolem0002(X34,X35))
| big_f(skolem0002(X34,X35),X35)
| ~ big_f(X35,skolem0002(X34,X35))
| ~ big_f(skolem0002(X34,X35),X34)
| big_f(skolem0001(X34),skolem0003(X34,X35))
| big_f(skolem0003(X34,X35),X35)
| big_f(X35,skolem0003(X34,X35))
| big_f(skolem0003(X34,X35),skolem0001(X34)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c18,negated_conjecture,
( big_f(X32,skolem0002(X32,X33))
| big_f(skolem0002(X32,X33),X33)
| ~ big_f(X33,skolem0002(X32,X33))
| ~ big_f(skolem0002(X32,X33),X32)
| ~ big_f(skolem0001(X32),skolem0003(X32,X33))
| ~ big_f(skolem0003(X32,X33),X33)
| big_f(X33,skolem0003(X32,X33))
| big_f(skolem0003(X32,X33),skolem0001(X32)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c16,negated_conjecture,
( big_f(X28,skolem0002(X28,X29))
| big_f(skolem0002(X28,X29),X29)
| ~ big_f(X29,skolem0002(X28,X29))
| ~ big_f(skolem0002(X28,X29),X28)
| ~ big_f(skolem0001(X28),skolem0003(X28,X29))
| big_f(skolem0003(X28,X29),X29)
| big_f(X29,skolem0003(X28,X29))
| ~ big_f(skolem0003(X28,X29),skolem0001(X28)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c15,negated_conjecture,
( big_f(X26,skolem0002(X26,X27))
| big_f(skolem0002(X26,X27),X27)
| ~ big_f(X27,skolem0002(X26,X27))
| ~ big_f(skolem0002(X26,X27),X26)
| big_f(skolem0001(X26),skolem0003(X26,X27))
| big_f(skolem0003(X26,X27),X27)
| ~ big_f(X27,skolem0003(X26,X27))
| ~ big_f(skolem0003(X26,X27),skolem0001(X26)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c13,negated_conjecture,
( ~ big_f(X22,skolem0002(X22,X23))
| ~ big_f(skolem0002(X22,X23),X23)
| ~ big_f(X23,skolem0002(X22,X23))
| ~ big_f(skolem0002(X22,X23),X22)
| ~ big_f(X23,skolem0003(X22,X23))
| ~ big_f(skolem0003(X22,X23),X23)
| big_f(skolem0001(X22),skolem0003(X22,X23))
| big_f(skolem0003(X22,X23),skolem0001(X22)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c10,negated_conjecture,
( ~ big_f(X15,skolem0002(X15,X16))
| ~ big_f(skolem0002(X15,X16),X16)
| ~ big_f(X16,skolem0002(X15,X16))
| ~ big_f(skolem0002(X15,X16),X15)
| ~ big_f(skolem0001(X15),skolem0003(X15,X16))
| ~ big_f(skolem0003(X15,X16),X16)
| big_f(X16,skolem0003(X15,X16))
| big_f(skolem0003(X15,X16),skolem0001(X15)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c8,negated_conjecture,
( ~ big_f(X11,skolem0002(X11,X12))
| ~ big_f(skolem0002(X11,X12),X12)
| ~ big_f(X12,skolem0002(X11,X12))
| ~ big_f(skolem0002(X11,X12),X11)
| ~ big_f(skolem0001(X11),skolem0003(X11,X12))
| big_f(skolem0003(X11,X12),X12)
| big_f(X12,skolem0003(X11,X12))
| ~ big_f(skolem0003(X11,X12),skolem0001(X11)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c7,negated_conjecture,
( ~ big_f(X9,skolem0002(X9,X10))
| ~ big_f(skolem0002(X9,X10),X10)
| ~ big_f(X10,skolem0002(X9,X10))
| ~ big_f(skolem0002(X9,X10),X9)
| big_f(skolem0001(X9),skolem0003(X9,X10))
| big_f(skolem0003(X9,X10),X10)
| ~ big_f(X10,skolem0003(X9,X10))
| ~ big_f(skolem0003(X9,X10),skolem0001(X9)) ),
inference(split_conjunct,[status(thm)],[c5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN348+1 : TPTP v8.1.2. Released v2.0.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.32 % Computer : n006.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.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 20:35:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 1.09/1.30 % Version: 1.5
% 1.09/1.30 % SZS status CounterSatisfiable
% 1.09/1.30 % SZS output start Saturation
% See solution above
% 1.16/1.31
% 1.16/1.31 % Initial clauses : 64
% 1.16/1.31 % Processed clauses : 101
% 1.16/1.31 % Factors computed : 31
% 1.16/1.31 % Resolvents computed: 565
% 1.16/1.31 % Tautologies deleted: 536
% 1.16/1.31 % Forward subsumed : 23
% 1.16/1.31 % Backward subsumed : 14
% 1.16/1.31 % -------- CPU Time ---------
% 1.16/1.31 % User time : 0.963 s
% 1.16/1.31 % System time : 0.020 s
% 1.16/1.31 % Total time : 0.983 s
%------------------------------------------------------------------------------