%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SYN353+1 : TPTP v8.1.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n010.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 : 600s
% DateTime : Thu Jul 21 09:01:41 EDT 2022
% Result : Theorem 122.51s 122.64s
% Output : CNFRefutation 122.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 1
% Syntax : Number of formulae : 169 ( 9 unt; 0 def)
% Number of atoms : 634 ( 0 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 676 ( 211 ~; 338 |; 65 &)
% ( 32 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 380 ( 7 sgn 84 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(church_46_18_5,conjecture,
! [X] :
? [Y1,Y2,Y3] :
! [Z] :
( ( big_f(Y1,Y2,Y3)
=> ( big_f(X,X,Z)
=> ( big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,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(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(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) )
<=> big_f(Z,Z,Z) ) ) ) ) ) ).
fof(subgoal_0,plain,
! [X] :
? [Y1,Y2,Y3] :
! [Z] :
( ( big_f(Y1,Y2,Y3)
=> ( big_f(X,X,Z)
=> ( big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,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(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(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) )
<=> big_f(Z,Z,Z) ) ) ) ) ),
inference(strip,[],[church_46_18_5]) ).
fof(negate_0_0,plain,
~ ! [X] :
? [Y1,Y2,Y3] :
! [Z] :
( ( big_f(Y1,Y2,Y3)
=> ( big_f(X,X,Z)
=> ( big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,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(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(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) )
<=> big_f(Z,Z,Z) ) ) ) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [X] :
! [Y1,Y2,Y3] :
? [Z] :
( ( ~ big_f(X,X,Z)
| ~ big_f(Y1,Y2,Y3)
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) )
& ( ~ big_f(Y1,Z,Y2)
<=> ( big_f(Y2,Y3,Y1)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y2,Y1,Z)
<=> ( big_f(Y3,Y1,Y2)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1) ) ) )
& ( ~ big_f(Z,Y2,Y1)
<=> ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Z,Z,Z)
<=> ( big_f(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [Y1,Y2,Y3] :
? [Z] :
( ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Z)
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) )
& ( ~ big_f(Y1,Z,Y2)
<=> ( big_f(Y2,Y3,Y1)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y2,Y1,Z)
<=> ( big_f(Y3,Y1,Y2)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1) ) ) )
& ( ~ big_f(Z,Y2,Y1)
<=> ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Z,Z,Z)
<=> ( big_f(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) ) ),
inference(skolemize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [Y1,Y2,Y3] :
? [Z] :
( ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Z)
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) )
& ( ~ big_f(Y1,Z,Y2)
<=> ( big_f(Y2,Y3,Y1)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y2,Y1,Z)
<=> ( big_f(Y3,Y1,Y2)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1) ) ) )
& ( ~ big_f(Z,Y2,Y1)
<=> ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Z,Z,Z)
<=> ( big_f(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) ) ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [Y1,Y2,Y3] :
( ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) )
& ( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
<=> ( big_f(Y2,Y3,Y1)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
<=> ( big_f(Y3,Y1,Y2)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1) ) ) )
& ( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
<=> ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) )
& ( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3))
<=> ( big_f(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) ) ),
inference(skolemize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [Y1,Y2,Y3] :
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3))
<=> ( big_f(Y1,Y2,Y3)
& big_f(Y2,Y3,Y1)
& big_f(Y3,Y1,Y2) ) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [Y1,Y2,Y3] :
( ( big_f(Y1,Y2,Y3)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) )
& ( big_f(Y2,Y3,Y1)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) )
& ( big_f(Y3,Y1,Y2)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) )
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) ) ),
inference(clausify,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) ),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [Y1,Y2,Y3] :
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
<=> ( ~ big_f(Y1,Y2,Y3)
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ) ) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_8,plain,
! [Y1,Y2,Y3] :
( ( ~ big_f(Y1,Y2,Y3)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) )
& ( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) )
& ( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y2,Y3,Y1) )
& ( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y3,Y1,Y2) ) ),
inference(clausify,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [Y1,Y2,Y3] :
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y3,Y1,Y2) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
<=> ( big_f(Y2,Y3,Y1)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2) ) ) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_11,plain,
! [Y1,Y2,Y3] :
( ( big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| big_f(Y2,Y3,Y1) )
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2) )
& ( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y1,Y2,Y3) )
& ( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ) ),
inference(clausify,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [Y1,Y2,Y3] :
( big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| big_f(Y2,Y3,Y1) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_14,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
<=> ( big_f(Y3,Y1,Y2)
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1) ) ) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_15,plain,
! [Y1,Y2,Y3] :
( ( big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y3,Y1,Y2) )
& ( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3)) )
& ( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,Y2,Y3) )
& ( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1) ) ),
inference(clausify,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [Y1,Y2,Y3] :
( big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y3,Y1,Y2) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,Y2,Y3)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_18,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_19,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3)) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_20,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_21,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y1,Y2,Y3) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_22,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,Y2,Y3) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_23,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_24,plain,
! [Y1,Y2,Y3] :
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y2,Y3,Y1) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_25,plain,
! [Y1,Y2,Y3] :
( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) ),
inference(conjunct,[],[normalize_0_8]) ).
cnf(refute_0_0,plain,
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_1,plain,
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y3,Y1,Y2) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_2,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_17648,X_17647,X_17646),X_17647,X_17648)
| big_f(X_17646,X_17648,X_17647)
| big_f(X_17648,X_17647,X_17646) ),
inference(subst,[],[refute_0_1:[bind(Y1,$fot(X_17648)),bind(Y2,$fot(X_17647)),bind(Y3,$fot(X_17646))]]) ).
cnf(refute_0_3,plain,
( big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| big_f(Y2,Y3,Y1) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_4,plain,
( big_f(X_17644,X_17643,X_17645)
| big_f(X_17645,skolemFOFtoCNF_Z(X_17645,X_17644,X_17643),X_17644) ),
inference(subst,[],[refute_0_3:[bind(Y1,$fot(X_17645)),bind(Y2,$fot(X_17644)),bind(Y3,$fot(X_17643))]]) ).
cnf(refute_0_5,plain,
( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_6,plain,
( ~ big_f(X_17629,skolemFOFtoCNF_Z(X_17629,X_17630,skolemFOFtoCNF_Z(X_17630,X_17629,X_17628)),X_17630)
| ~ big_f(X_17630,skolemFOFtoCNF_Z(X_17630,X_17629,X_17628),X_17629)
| big_f(skolemFOFtoCNF_Z(X_17630,X_17629,X_17628),X_17629,X_17630) ),
inference(subst,[],[refute_0_5:[bind(Y1,$fot(X_17629)),bind(Y2,$fot(X_17630)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_17630,X_17629,X_17628)))]]) ).
cnf(refute_0_7,plain,
( big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y3,Y1,Y2) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_8,plain,
( big_f(Y3,X_9,X_8)
| big_f(X_8,X_9,skolemFOFtoCNF_Z(X_9,X_8,Y3)) ),
inference(subst,[],[refute_0_7:[bind(Y1,$fot(X_9)),bind(Y2,$fot(X_8))]]) ).
cnf(refute_0_9,plain,
( ~ big_f(Y1,Y2,Y3)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) ),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_10,plain,
( ~ big_f(X_8,X_9,skolemFOFtoCNF_Z(X_9,X_8,Y3))
| big_f(skolemFOFtoCNF_Z(X_8,X_9,skolemFOFtoCNF_Z(X_9,X_8,Y3)),X_9,X_8) ),
inference(subst,[],[refute_0_9:[bind(Y1,$fot(X_8)),bind(Y2,$fot(X_9)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_9,X_8,Y3)))]]) ).
cnf(refute_0_11,plain,
( big_f(Y3,X_9,X_8)
| big_f(skolemFOFtoCNF_Z(X_8,X_9,skolemFOFtoCNF_Z(X_9,X_8,Y3)),X_9,X_8) ),
inference(resolve,[$cnf( big_f(X_8,X_9,skolemFOFtoCNF_Z(X_9,X_8,Y3)) )],[refute_0_8,refute_0_10]) ).
cnf(refute_0_12,plain,
( big_f(X_17625,X_17627,X_17626)
| big_f(skolemFOFtoCNF_Z(X_17626,X_17627,skolemFOFtoCNF_Z(X_17627,X_17626,X_17625)),X_17627,X_17626) ),
inference(subst,[],[refute_0_11:[bind(Y3,$fot(X_17625)),bind(X_8,$fot(X_17626)),bind(X_9,$fot(X_17627))]]) ).
cnf(refute_0_13,plain,
( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y2,Y3,Y1) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_14,plain,
( ~ big_f(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592))))
| ~ big_f(skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)),X_17594,X_17593)
| big_f(X_17593,skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)),X_17594) ),
inference(subst,[],[refute_0_13:[bind(Y1,$fot(X_17594)),bind(Y2,$fot(X_17593)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592))))]]) ).
cnf(refute_0_15,plain,
( big_f(X_117,X_116,X_118)
| big_f(X_118,skolemFOFtoCNF_Z(X_118,X_117,X_116),X_117) ),
inference(subst,[],[refute_0_3:[bind(Y1,$fot(X_118)),bind(Y2,$fot(X_117)),bind(Y3,$fot(X_116))]]) ).
cnf(refute_0_16,plain,
( big_f(Y3,X_36,X_35)
| big_f(X_35,X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3)) ),
inference(subst,[],[refute_0_7:[bind(Y1,$fot(X_36)),bind(Y2,$fot(X_35))]]) ).
cnf(refute_0_17,plain,
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3)) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_18,plain,
( ~ big_f(X_35,X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3))
| ~ big_f(X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3),X_35)
| big_f(X_36,X_35,skolemFOFtoCNF_Z(X_35,X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3))) ),
inference(subst,[],[refute_0_17:[bind(Y1,$fot(X_35)),bind(Y2,$fot(X_36)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_36,X_35,Y3)))]]) ).
cnf(refute_0_19,plain,
( ~ big_f(X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3),X_35)
| big_f(Y3,X_36,X_35)
| big_f(X_36,X_35,skolemFOFtoCNF_Z(X_35,X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3))) ),
inference(resolve,[$cnf( big_f(X_35,X_36,skolemFOFtoCNF_Z(X_36,X_35,Y3)) )],[refute_0_16,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ big_f(X_118,skolemFOFtoCNF_Z(X_118,X_117,X_116),X_117)
| big_f(X_116,X_118,X_117)
| big_f(X_118,X_117,skolemFOFtoCNF_Z(X_117,X_118,skolemFOFtoCNF_Z(X_118,X_117,X_116))) ),
inference(subst,[],[refute_0_19:[bind(Y3,$fot(X_116)),bind(X_35,$fot(X_117)),bind(X_36,$fot(X_118))]]) ).
cnf(refute_0_21,plain,
( big_f(X_116,X_118,X_117)
| big_f(X_117,X_116,X_118)
| big_f(X_118,X_117,skolemFOFtoCNF_Z(X_117,X_118,skolemFOFtoCNF_Z(X_118,X_117,X_116))) ),
inference(resolve,[$cnf( big_f(X_118,skolemFOFtoCNF_Z(X_118,X_117,X_116),X_117) )],[refute_0_15,refute_0_20]) ).
cnf(refute_0_22,plain,
( big_f(X_164,X_165,X_166)
| big_f(X_165,X_166,skolemFOFtoCNF_Z(X_166,X_165,skolemFOFtoCNF_Z(X_165,X_166,X_164)))
| big_f(X_166,X_164,X_165) ),
inference(subst,[],[refute_0_21:[bind(X_116,$fot(X_164)),bind(X_117,$fot(X_166)),bind(X_118,$fot(X_165))]]) ).
cnf(refute_0_23,plain,
( big_f(Y3,X_26,X_27)
| big_f(skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3)),X_26,X_27) ),
inference(subst,[],[refute_0_11:[bind(X_8,$fot(X_27)),bind(X_9,$fot(X_26))]]) ).
cnf(refute_0_24,plain,
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_25,plain,
( ~ big_f(X_26,X_27,skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3)))
| ~ big_f(skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3)),X_26,X_27)
| big_f(X_26,skolemFOFtoCNF_Z(X_26,X_27,skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3))),X_27) ),
inference(subst,[],[refute_0_24:[bind(Y1,$fot(X_26)),bind(Y2,$fot(X_27)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3))))]]) ).
cnf(refute_0_26,plain,
( ~ big_f(X_26,X_27,skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3)))
| big_f(Y3,X_26,X_27)
| big_f(X_26,skolemFOFtoCNF_Z(X_26,X_27,skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3))),X_27) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_27,X_26,skolemFOFtoCNF_Z(X_26,X_27,Y3)),X_26,X_27) )],[refute_0_23,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ big_f(X_165,X_166,skolemFOFtoCNF_Z(X_166,X_165,skolemFOFtoCNF_Z(X_165,X_166,X_164)))
| big_f(X_164,X_165,X_166)
| big_f(X_165,skolemFOFtoCNF_Z(X_165,X_166,skolemFOFtoCNF_Z(X_166,X_165,skolemFOFtoCNF_Z(X_165,X_166,X_164))),X_166) ),
inference(subst,[],[refute_0_26:[bind(Y3,$fot(X_164)),bind(X_26,$fot(X_165)),bind(X_27,$fot(X_166))]]) ).
cnf(refute_0_28,plain,
( big_f(X_164,X_165,X_166)
| big_f(X_165,skolemFOFtoCNF_Z(X_165,X_166,skolemFOFtoCNF_Z(X_166,X_165,skolemFOFtoCNF_Z(X_165,X_166,X_164))),X_166)
| big_f(X_166,X_164,X_165) ),
inference(resolve,[$cnf( big_f(X_165,X_166,skolemFOFtoCNF_Z(X_166,X_165,skolemFOFtoCNF_Z(X_165,X_166,X_164))) )],[refute_0_22,refute_0_27]) ).
cnf(refute_0_29,plain,
( big_f(X_17589,X_17591,X_17590)
| big_f(X_17590,X_17589,X_17591)
| big_f(X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,skolemFOFtoCNF_Z(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,X_17589))),X_17590) ),
inference(subst,[],[refute_0_28:[bind(X_164,$fot(X_17589)),bind(X_165,$fot(X_17591)),bind(X_166,$fot(X_17590))]]) ).
cnf(refute_0_30,plain,
( ~ big_f(Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2)
| ~ big_f(Y2,Y3,Y1)
| big_f(Y1,Y2,Y3) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_31,plain,
( ~ big_f(X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))),X_17588)
| ~ big_f(X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586))),X_17587)
| big_f(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))) ),
inference(subst,[],[refute_0_30:[bind(Y1,$fot(X_17587)),bind(Y2,$fot(X_17588)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))))]]) ).
cnf(refute_0_32,plain,
( ~ big_f(X_121,X_120,skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119)))
| big_f(skolemFOFtoCNF_Z(X_121,X_120,skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119))),X_120,X_121) ),
inference(subst,[],[refute_0_9:[bind(Y1,$fot(X_121)),bind(Y2,$fot(X_120)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119))))]]) ).
cnf(refute_0_33,plain,
( big_f(X_119,X_121,X_120)
| big_f(X_120,X_119,X_121)
| big_f(X_121,X_120,skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119))) ),
inference(subst,[],[refute_0_21:[bind(X_116,$fot(X_119)),bind(X_117,$fot(X_120)),bind(X_118,$fot(X_121))]]) ).
cnf(refute_0_34,plain,
( big_f(X_119,X_121,X_120)
| big_f(X_120,X_119,X_121)
| big_f(skolemFOFtoCNF_Z(X_121,X_120,skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119))),X_120,X_121) ),
inference(resolve,[$cnf( big_f(X_121,X_120,skolemFOFtoCNF_Z(X_120,X_121,skolemFOFtoCNF_Z(X_121,X_120,X_119))) )],[refute_0_33,refute_0_32]) ).
cnf(refute_0_35,plain,
( big_f(X_17583,X_17585,X_17584)
| big_f(X_17584,X_17583,X_17585)
| big_f(skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583))),X_17584,X_17585) ),
inference(subst,[],[refute_0_34:[bind(X_119,$fot(X_17583)),bind(X_120,$fot(X_17584)),bind(X_121,$fot(X_17585))]]) ).
cnf(refute_0_36,plain,
( ~ big_f(Y2,Y1,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| ~ big_f(Y3,Y1,Y2)
| big_f(Y1,Y2,Y3) ),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_37,plain,
( ~ big_f(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041)))))
| ~ big_f(skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041))),X_7042,X_7043)
| big_f(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041)))) ),
inference(subst,[],[refute_0_36:[bind(Y1,$fot(X_7042)),bind(Y2,$fot(X_7043)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041)))))]]) ).
cnf(refute_0_38,plain,
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(Y1,Y2,Y3))
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_39,plain,
( ~ big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3) ),
inference(subst,[],[refute_0_30:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X))]]) ).
cnf(refute_0_40,plain,
( ~ big_f(X_289,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_289))
| big_f(skolemFOFtoCNF_X,X_289,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_13:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_289))]]) ).
cnf(refute_0_41,plain,
( big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_3:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X))]]) ).
cnf(refute_0_42,plain,
( ~ big_f(skolemFOFtoCNF_X,X_91,skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_91),skolemFOFtoCNF_X)
| big_f(X_91,skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_5:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_91))]]) ).
cnf(refute_0_43,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(X_90,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90) ),
inference(subst,[],[refute_0_1:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_90))]]) ).
cnf(refute_0_44,plain,
( big_f(Y3,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)) ),
inference(subst,[],[refute_0_7:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X))]]) ).
cnf(refute_0_45,plain,
( big_f(X_88,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_88)) ),
inference(subst,[],[refute_0_7:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_88))]]) ).
cnf(refute_0_46,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_88)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_88))
| big_f(X_88,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_88,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_38:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_88))]]) ).
cnf(refute_0_47,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_88)
| big_f(X_88,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_88,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_88)) )],[refute_0_45,refute_0_46]) ).
cnf(refute_0_48,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_47:[bind(X_88,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)))]]) ).
cnf(refute_0_49,plain,
( big_f(Y3,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)) )],[refute_0_44,refute_0_48]) ).
cnf(refute_0_50,plain,
( big_f(X_90,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_49:[bind(Y3,$fot(X_90))]]) ).
cnf(refute_0_51,plain,
( big_f(X_90,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90),skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_90),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_50,refute_0_43]) ).
cnf(refute_0_52,plain,
( big_f(X_91,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_91)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_91),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_51:[bind(X_90,$fot(X_91))]]) ).
cnf(refute_0_53,plain,
( ~ big_f(skolemFOFtoCNF_X,X_91,skolemFOFtoCNF_X)
| big_f(X_91,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_91) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_91),skolemFOFtoCNF_X) )],[refute_0_52,refute_0_42]) ).
cnf(refute_0_54,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_53:[bind(X_91,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)))]]) ).
cnf(refute_0_55,plain,
( big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) )],[refute_0_41,refute_0_54]) ).
cnf(refute_0_56,plain,
( big_f(skolemFOFtoCNF_X,X_288,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_55:[bind(Y3,$fot(X_288))]]) ).
cnf(refute_0_57,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287)))
| ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287)) ),
inference(subst,[],[refute_0_36:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287)))]]) ).
cnf(refute_0_58,plain,
( big_f(skolemFOFtoCNF_X,X_286,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_3:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_286))]]) ).
cnf(refute_0_59,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256),skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)) ),
inference(subst,[],[refute_0_30:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)))]]) ).
cnf(refute_0_60,plain,
( ~ big_f(X_95,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_95))
| big_f(skolemFOFtoCNF_X,X_95,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_13:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_95))]]) ).
cnf(refute_0_61,plain,
( ~ big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1)
| big_f(Y1,Y2,Y3)
| big_f(Y2,Y3,Y1) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_62,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_93,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93) ),
inference(subst,[],[refute_0_61:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_93))]]) ).
cnf(refute_0_63,plain,
( big_f(skolemFOFtoCNF_X,X_93,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_55:[bind(Y3,$fot(X_93))]]) ).
cnf(refute_0_64,plain,
( big_f(skolemFOFtoCNF_X,X_93,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93)) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_63,refute_0_62]) ).
cnf(refute_0_65,plain,
( big_f(skolemFOFtoCNF_X,X_95,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_95)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_95)) ),
inference(subst,[],[refute_0_64:[bind(X_93,$fot(X_95))]]) ).
cnf(refute_0_66,plain,
( ~ big_f(X_95,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_95,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_95) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_95)) )],[refute_0_65,refute_0_60]) ).
cnf(refute_0_67,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_66:[bind(X_95,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157))))]]) ).
cnf(refute_0_68,plain,
( big_f(skolemFOFtoCNF_X,X_156,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_3:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_156))]]) ).
cnf(refute_0_69,plain,
( ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2)
| big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),Y2,Y1) ),
inference(canonicalize,[],[normalize_0_25]) ).
cnf(refute_0_70,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_69:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93)))]]) ).
cnf(refute_0_71,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_93,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_93),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_63,refute_0_70]) ).
cnf(refute_0_72,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_156,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_71:[bind(X_93,$fot(X_156))]]) ).
cnf(refute_0_73,plain,
( big_f(skolemFOFtoCNF_X,X_156,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_156),skolemFOFtoCNF_X) )],[refute_0_68,refute_0_72]) ).
cnf(refute_0_74,plain,
( big_f(skolemFOFtoCNF_X,X_157,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157))
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_73:[bind(X_156,$fot(X_157))]]) ).
cnf(refute_0_75,plain,
( big_f(skolemFOFtoCNF_X,X_157,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)),skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_157)),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_74,refute_0_67]) ).
cnf(refute_0_76,plain,
( big_f(skolemFOFtoCNF_X,X_256,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_75:[bind(X_157,$fot(X_256))]]) ).
cnf(refute_0_77,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_256,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256))) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_256)),skolemFOFtoCNF_X) )],[refute_0_76,refute_0_59]) ).
cnf(refute_0_78,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_286,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286))) ),
inference(subst,[],[refute_0_77:[bind(X_256,$fot(X_286))]]) ).
cnf(refute_0_79,plain,
( big_f(skolemFOFtoCNF_X,X_286,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286))) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_286),skolemFOFtoCNF_X) )],[refute_0_58,refute_0_78]) ).
cnf(refute_0_80,plain,
( big_f(skolemFOFtoCNF_X,X_287,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287))
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287))) ),
inference(subst,[],[refute_0_79:[bind(X_286,$fot(X_287))]]) ).
cnf(refute_0_81,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_287,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287)) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_287))) )],[refute_0_80,refute_0_57]) ).
cnf(refute_0_82,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_288,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288)) ),
inference(subst,[],[refute_0_81:[bind(X_287,$fot(X_288))]]) ).
cnf(refute_0_83,plain,
( big_f(skolemFOFtoCNF_X,X_288,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288)) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_288),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_56,refute_0_82]) ).
cnf(refute_0_84,plain,
( big_f(skolemFOFtoCNF_X,X_289,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_289)) ),
inference(subst,[],[refute_0_83:[bind(X_288,$fot(X_289))]]) ).
cnf(refute_0_85,plain,
( ~ big_f(X_289,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_289,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_289)) )],[refute_0_84,refute_0_40]) ).
cnf(refute_0_86,plain,
( ~ big_f(X_298,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_298,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_85:[bind(X_289,$fot(X_298))]]) ).
cnf(refute_0_87,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_296)
| big_f(X_296,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_296,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_47:[bind(X_88,$fot(X_296))]]) ).
cnf(refute_0_88,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_295),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_295,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_295) ),
inference(subst,[],[refute_0_61:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_295))]]) ).
cnf(refute_0_89,plain,
( ~ big_f(skolemFOFtoCNF_X,X_291,skolemFOFtoCNF_X)
| ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_291),skolemFOFtoCNF_X)
| big_f(X_291,skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_5:[bind(Y1,$fot(skolemFOFtoCNF_X)),bind(Y2,$fot(skolemFOFtoCNF_X)),bind(Y3,$fot(X_291))]]) ).
cnf(refute_0_90,plain,
( ~ big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_85:[bind(X_289,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)))]]) ).
cnf(refute_0_91,plain,
( big_f(Y3,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_49,refute_0_90]) ).
cnf(refute_0_92,plain,
( big_f(X_291,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_291),skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_91:[bind(Y3,$fot(X_291))]]) ).
cnf(refute_0_93,plain,
( ~ big_f(skolemFOFtoCNF_X,X_291,skolemFOFtoCNF_X)
| big_f(X_291,skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_291),skolemFOFtoCNF_X) )],[refute_0_92,refute_0_89]) ).
cnf(refute_0_94,plain,
( ~ big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_93:[bind(X_291,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)))]]) ).
cnf(refute_0_95,plain,
( big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) )],[refute_0_41,refute_0_94]) ).
cnf(refute_0_96,plain,
( big_f(skolemFOFtoCNF_X,X_295,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_295),skolemFOFtoCNF_X,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_95:[bind(Y3,$fot(X_295))]]) ).
cnf(refute_0_97,plain,
( big_f(skolemFOFtoCNF_X,X_295,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_295) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_295),skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_96,refute_0_88]) ).
cnf(refute_0_98,plain,
( big_f(skolemFOFtoCNF_X,X_296,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_296) ),
inference(subst,[],[refute_0_97:[bind(X_295,$fot(X_296))]]) ).
cnf(refute_0_99,plain,
( big_f(X_296,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_296,skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,X_296) )],[refute_0_98,refute_0_87]) ).
cnf(refute_0_100,plain,
( big_f(X_298,skolemFOFtoCNF_X,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,X_298,skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_99:[bind(X_296,$fot(X_298))]]) ).
cnf(refute_0_101,plain,
big_f(skolemFOFtoCNF_X,X_298,skolemFOFtoCNF_X),
inference(resolve,[$cnf( big_f(X_298,skolemFOFtoCNF_X,skolemFOFtoCNF_X) )],[refute_0_100,refute_0_86]) ).
cnf(refute_0_102,plain,
big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X),
inference(subst,[],[refute_0_101:[bind(X_298,$fot(skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3)))]]) ).
cnf(refute_0_103,plain,
( ~ big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X)
| big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_Z(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),skolemFOFtoCNF_X) )],[refute_0_102,refute_0_39]) ).
cnf(refute_0_104,plain,
big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X),
inference(subst,[],[refute_0_101:[bind(X_298,$fot(Y3))]]) ).
cnf(refute_0_105,plain,
big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,Y3),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,Y3,skolemFOFtoCNF_X) )],[refute_0_104,refute_0_103]) ).
cnf(refute_0_106,plain,
big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(Y1,Y2,Y3)),
inference(subst,[],[refute_0_105:[bind(Y3,$fot(skolemFOFtoCNF_Z(Y1,Y2,Y3)))]]) ).
cnf(refute_0_107,plain,
( ~ big_f(Y1,Y2,Y3)
| big_f(Y2,Y3,Y1)
| big_f(Y3,Y1,Y2) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_X,skolemFOFtoCNF_X,skolemFOFtoCNF_Z(Y1,Y2,Y3)) )],[refute_0_106,refute_0_38]) ).
cnf(refute_0_108,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))),X_2255,X_2254)
| big_f(X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))),X_2255)
| big_f(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253))))) ),
inference(subst,[],[refute_0_107:[bind(Y1,$fot(skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))))),bind(Y2,$fot(X_2255)),bind(Y3,$fot(X_2254))]]) ).
cnf(refute_0_109,plain,
( big_f(X_2250,X_2252,X_2251)
| big_f(X_2251,X_2250,X_2252)
| big_f(X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,X_2250))),X_2251) ),
inference(subst,[],[refute_0_28:[bind(X_164,$fot(X_2250)),bind(X_165,$fot(X_2252)),bind(X_166,$fot(X_2251))]]) ).
cnf(refute_0_110,plain,
( ~ big_f(X_181,skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179))),X_180)
| ~ big_f(skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179))),X_180,X_181)
| big_f(skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179)))),X_181,X_180) ),
inference(subst,[],[refute_0_69:[bind(Y1,$fot(X_180)),bind(Y2,$fot(X_181)),bind(Y3,$fot(skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179)))))]]) ).
cnf(refute_0_111,plain,
( big_f(X_179,X_181,X_180)
| big_f(X_180,X_179,X_181)
| big_f(skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179))),X_180,X_181) ),
inference(subst,[],[refute_0_34:[bind(X_119,$fot(X_179)),bind(X_120,$fot(X_180)),bind(X_121,$fot(X_181))]]) ).
cnf(refute_0_112,plain,
( ~ big_f(X_181,skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179))),X_180)
| big_f(X_179,X_181,X_180)
| big_f(X_180,X_179,X_181)
| big_f(skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179)))),X_181,X_180) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_181,X_180,skolemFOFtoCNF_Z(X_180,X_181,skolemFOFtoCNF_Z(X_181,X_180,X_179))),X_180,X_181) )],[refute_0_111,refute_0_110]) ).
cnf(refute_0_113,plain,
( ~ big_f(X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,X_2250))),X_2251)
| big_f(X_2250,X_2252,X_2251)
| big_f(X_2251,X_2250,X_2252)
| big_f(skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,X_2250)))),X_2252,X_2251) ),
inference(subst,[],[refute_0_112:[bind(X_179,$fot(X_2250)),bind(X_180,$fot(X_2251)),bind(X_181,$fot(X_2252))]]) ).
cnf(refute_0_114,plain,
( big_f(X_2250,X_2252,X_2251)
| big_f(X_2251,X_2250,X_2252)
| big_f(skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,X_2250)))),X_2252,X_2251) ),
inference(resolve,[$cnf( big_f(X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,skolemFOFtoCNF_Z(X_2251,X_2252,skolemFOFtoCNF_Z(X_2252,X_2251,X_2250))),X_2251) )],[refute_0_109,refute_0_113]) ).
cnf(refute_0_115,plain,
( big_f(X_2253,X_2255,X_2254)
| big_f(X_2254,X_2253,X_2255)
| big_f(skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))),X_2255,X_2254) ),
inference(subst,[],[refute_0_114:[bind(X_2250,$fot(X_2253)),bind(X_2251,$fot(X_2254)),bind(X_2252,$fot(X_2255))]]) ).
cnf(refute_0_116,plain,
( big_f(X_2253,X_2255,X_2254)
| big_f(X_2254,X_2253,X_2255)
| big_f(X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))),X_2255)
| big_f(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253))))) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,skolemFOFtoCNF_Z(X_2254,X_2255,skolemFOFtoCNF_Z(X_2255,X_2254,X_2253)))),X_2255,X_2254) )],[refute_0_115,refute_0_108]) ).
cnf(refute_0_117,plain,
( big_f(X_7041,X_7043,X_7042)
| big_f(X_7042,X_7041,X_7043)
| big_f(X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041)))),X_7043)
| big_f(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041))))) ),
inference(subst,[],[refute_0_116:[bind(X_2253,$fot(X_7041)),bind(X_2254,$fot(X_7042)),bind(X_2255,$fot(X_7043))]]) ).
cnf(refute_0_118,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041))),X_7042,X_7043)
| big_f(X_7041,X_7043,X_7042)
| big_f(X_7042,X_7041,X_7043)
| big_f(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041))))
| big_f(X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041)))),X_7043) ),
inference(resolve,[$cnf( big_f(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,skolemFOFtoCNF_Z(X_7042,X_7043,skolemFOFtoCNF_Z(X_7043,X_7042,X_7041))))) )],[refute_0_117,refute_0_37]) ).
cnf(refute_0_119,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583))),X_17584,X_17585)
| big_f(X_17583,X_17585,X_17584)
| big_f(X_17584,X_17583,X_17585)
| big_f(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583))))
| big_f(X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583)))),X_17585) ),
inference(subst,[],[refute_0_118:[bind(X_7041,$fot(X_17583)),bind(X_7042,$fot(X_17584)),bind(X_7043,$fot(X_17585))]]) ).
cnf(refute_0_120,plain,
( big_f(X_17583,X_17585,X_17584)
| big_f(X_17584,X_17583,X_17585)
| big_f(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583))))
| big_f(X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583)))),X_17585) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_17585,X_17584,skolemFOFtoCNF_Z(X_17584,X_17585,skolemFOFtoCNF_Z(X_17585,X_17584,X_17583))),X_17584,X_17585) )],[refute_0_35,refute_0_119]) ).
cnf(refute_0_121,plain,
( big_f(X_17586,X_17588,X_17587)
| big_f(X_17587,X_17586,X_17588)
| big_f(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586))))
| big_f(X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))),X_17588) ),
inference(subst,[],[refute_0_120:[bind(X_17583,$fot(X_17586)),bind(X_17584,$fot(X_17587)),bind(X_17585,$fot(X_17588))]]) ).
cnf(refute_0_122,plain,
( ~ big_f(X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586))),X_17587)
| big_f(X_17586,X_17588,X_17587)
| big_f(X_17587,X_17586,X_17588)
| big_f(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))) ),
inference(resolve,[$cnf( big_f(X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,skolemFOFtoCNF_Z(X_17587,X_17588,skolemFOFtoCNF_Z(X_17588,X_17587,X_17586)))),X_17588) )],[refute_0_121,refute_0_31]) ).
cnf(refute_0_123,plain,
( ~ big_f(X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,skolemFOFtoCNF_Z(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,X_17589))),X_17590)
| big_f(X_17589,X_17591,X_17590)
| big_f(X_17590,X_17589,X_17591)
| big_f(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,skolemFOFtoCNF_Z(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,X_17589)))) ),
inference(subst,[],[refute_0_122:[bind(X_17586,$fot(X_17589)),bind(X_17587,$fot(X_17590)),bind(X_17588,$fot(X_17591))]]) ).
cnf(refute_0_124,plain,
( big_f(X_17589,X_17591,X_17590)
| big_f(X_17590,X_17589,X_17591)
| big_f(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,skolemFOFtoCNF_Z(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,X_17589)))) ),
inference(resolve,[$cnf( big_f(X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,skolemFOFtoCNF_Z(X_17590,X_17591,skolemFOFtoCNF_Z(X_17591,X_17590,X_17589))),X_17590) )],[refute_0_29,refute_0_123]) ).
cnf(refute_0_125,plain,
( big_f(X_17592,X_17594,X_17593)
| big_f(X_17593,X_17592,X_17594)
| big_f(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)))) ),
inference(subst,[],[refute_0_124:[bind(X_17589,$fot(X_17592)),bind(X_17590,$fot(X_17593)),bind(X_17591,$fot(X_17594))]]) ).
cnf(refute_0_126,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)),X_17594,X_17593)
| big_f(X_17592,X_17594,X_17593)
| big_f(X_17593,X_17592,X_17594)
| big_f(X_17593,skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)),X_17594) ),
inference(resolve,[$cnf( big_f(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,skolemFOFtoCNF_Z(X_17593,X_17594,skolemFOFtoCNF_Z(X_17594,X_17593,X_17592)))) )],[refute_0_125,refute_0_14]) ).
cnf(refute_0_127,plain,
( ~ big_f(skolemFOFtoCNF_Z(X_17626,X_17627,skolemFOFtoCNF_Z(X_17627,X_17626,X_17625)),X_17627,X_17626)
| big_f(X_17625,X_17627,X_17626)
| big_f(X_17626,X_17625,X_17627)
| big_f(X_17626,skolemFOFtoCNF_Z(X_17626,X_17627,skolemFOFtoCNF_Z(X_17627,X_17626,X_17625)),X_17627) ),
inference(subst,[],[refute_0_126:[bind(X_17592,$fot(X_17625)),bind(X_17593,$fot(X_17626)),bind(X_17594,$fot(X_17627))]]) ).
cnf(refute_0_128,plain,
( big_f(X_17625,X_17627,X_17626)
| big_f(X_17626,X_17625,X_17627)
| big_f(X_17626,skolemFOFtoCNF_Z(X_17626,X_17627,skolemFOFtoCNF_Z(X_17627,X_17626,X_17625)),X_17627) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_17626,X_17627,skolemFOFtoCNF_Z(X_17627,X_17626,X_17625)),X_17627,X_17626) )],[refute_0_12,refute_0_127]) ).
cnf(refute_0_129,plain,
( big_f(X_17628,X_17630,X_17629)
| big_f(X_17629,X_17628,X_17630)
| big_f(X_17629,skolemFOFtoCNF_Z(X_17629,X_17630,skolemFOFtoCNF_Z(X_17630,X_17629,X_17628)),X_17630) ),
inference(subst,[],[refute_0_128:[bind(X_17625,$fot(X_17628)),bind(X_17626,$fot(X_17629)),bind(X_17627,$fot(X_17630))]]) ).
cnf(refute_0_130,plain,
( ~ big_f(X_17630,skolemFOFtoCNF_Z(X_17630,X_17629,X_17628),X_17629)
| big_f(X_17628,X_17630,X_17629)
| big_f(X_17629,X_17628,X_17630)
| big_f(skolemFOFtoCNF_Z(X_17630,X_17629,X_17628),X_17629,X_17630) ),
inference(resolve,[$cnf( big_f(X_17629,skolemFOFtoCNF_Z(X_17629,X_17630,skolemFOFtoCNF_Z(X_17630,X_17629,X_17628)),X_17630) )],[refute_0_129,refute_0_6]) ).
cnf(refute_0_131,plain,
( ~ big_f(X_17645,skolemFOFtoCNF_Z(X_17645,X_17644,X_17643),X_17644)
| big_f(X_17643,X_17645,X_17644)
| big_f(X_17644,X_17643,X_17645)
| big_f(skolemFOFtoCNF_Z(X_17645,X_17644,X_17643),X_17644,X_17645) ),
inference(subst,[],[refute_0_130:[bind(X_17628,$fot(X_17643)),bind(X_17629,$fot(X_17644)),bind(X_17630,$fot(X_17645))]]) ).
cnf(refute_0_132,plain,
( big_f(X_17643,X_17645,X_17644)
| big_f(X_17644,X_17643,X_17645)
| big_f(skolemFOFtoCNF_Z(X_17645,X_17644,X_17643),X_17644,X_17645) ),
inference(resolve,[$cnf( big_f(X_17645,skolemFOFtoCNF_Z(X_17645,X_17644,X_17643),X_17644) )],[refute_0_4,refute_0_131]) ).
cnf(refute_0_133,plain,
( big_f(X_17646,X_17648,X_17647)
| big_f(X_17647,X_17646,X_17648)
| big_f(skolemFOFtoCNF_Z(X_17648,X_17647,X_17646),X_17647,X_17648) ),
inference(subst,[],[refute_0_132:[bind(X_17643,$fot(X_17646)),bind(X_17644,$fot(X_17647)),bind(X_17645,$fot(X_17648))]]) ).
cnf(refute_0_134,plain,
( big_f(X_17646,X_17648,X_17647)
| big_f(X_17647,X_17646,X_17648)
| big_f(X_17648,X_17647,X_17646) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(X_17648,X_17647,X_17646),X_17647,X_17648) )],[refute_0_133,refute_0_2]) ).
cnf(refute_0_135,plain,
big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)),
inference(subst,[],[refute_0_134:[bind(X_17646,$fot(skolemFOFtoCNF_Z(Y1,Y2,Y3))),bind(X_17647,$fot(skolemFOFtoCNF_Z(Y1,Y2,Y3))),bind(X_17648,$fot(skolemFOFtoCNF_Z(Y1,Y2,Y3)))]]) ).
cnf(refute_0_136,plain,
( ~ big_f(Y1,Y2,Y3)
| ~ big_f(Y2,Y3,Y1)
| ~ big_f(Y3,Y1,Y2) ),
inference(resolve,[$cnf( big_f(skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3),skolemFOFtoCNF_Z(Y1,Y2,Y3)) )],[refute_0_135,refute_0_0]) ).
cnf(refute_0_137,plain,
~ big_f(Y1,Y1,Y1),
inference(subst,[],[refute_0_136:[bind(Y2,$fot(Y1)),bind(Y3,$fot(Y1))]]) ).
cnf(refute_0_138,plain,
big_f(Y1,Y1,Y1),
inference(subst,[],[refute_0_134:[bind(X_17646,$fot(Y1)),bind(X_17647,$fot(Y1)),bind(X_17648,$fot(Y1))]]) ).
cnf(refute_0_139,plain,
$false,
inference(resolve,[$cnf( big_f(Y1,Y1,Y1) )],[refute_0_138,refute_0_137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN353+1 : TPTP v8.1.0. Released v2.0.0.
% 0.03/0.12 % Command : metis --show proof --show saturation %s
% 0.13/0.33 % Computer : n010.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Mon Jul 11 14:01:00 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 122.51/122.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.51/122.64
% 122.51/122.64 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 122.51/122.66
%------------------------------------------------------------------------------