%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n022.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 : Sun Jul 17 03:18:38 EDT 2022
% Result : Unsatisfiable 40.45s 40.63s
% Output : CNFRefutation 40.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 18
% Syntax : Number of formulae : 171 ( 28 unt; 0 def)
% Number of atoms : 1168 ( 389 equ)
% Maximal formula atoms : 420 ( 6 avg)
% Number of connectives : 1666 ( 669 ~; 880 |; 109 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 76 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-1 aty)
% Number of variables : 155 ( 0 sgn 81 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_2,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( rr(X,Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp5(Y) )
& ? [Y] :
( rr(X,Y)
& cp(Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp1(Y) )
& ! [Y8,Y9,Y10,Y11,Y12] :
( ( rr(X,Y8)
& rr(X,Y9)
& rr(X,Y10)
& rr(X,Y11)
& rr(X,Y12) )
=> ( Y8 = Y9
| Y8 = Y10
| Y8 = Y11
| Y8 = Y12
| Y9 = Y10
| Y9 = Y11
| Y9 = Y12
| Y10 = Y11
| Y10 = Y12
| Y11 = Y12 ) )
& ? [Y] :
( rr(X,Y)
& cp1(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y) ) ) ) ).
fof(axiom_3,axiom,
! [X] :
( cp1(X)
=> ~ ( cp2(X)
| cp4(X)
| cp5(X)
| cp3(X) ) ) ).
fof(axiom_4,axiom,
! [X] :
( cp2(X)
=> ~ ( cp4(X)
| cp5(X)
| cp3(X) ) ) ).
fof(axiom_5,axiom,
! [X] :
( cp3(X)
=> ~ ( cp4(X)
| cp5(X) ) ) ).
fof(axiom_6,axiom,
! [X] :
( cp4(X)
=> ~ cp5(X) ) ).
fof(axiom_7,axiom,
cUnsatisfiable(i2003_11_14_17_19_24236) ).
fof(normalize_0_0,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(canonicalize,[],[axiom_7]) ).
fof(normalize_0_1,plain,
! [X] :
( ~ cUnsatisfiable(X)
<=> ( ? [Y8,Y9,Y10,Y11,Y12] :
( Y8 != Y9
& Y8 != Y10
& Y8 != Y11
& Y8 != Y12
& Y9 != Y10
& Y9 != Y11
& Y9 != Y12
& Y10 != Y11
& Y10 != Y12
& Y11 != Y12
& rr(X,Y8)
& rr(X,Y9)
& rr(X,Y10)
& rr(X,Y11)
& rr(X,Y12) )
| ! [Y] :
( ~ cp1(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp2(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp3(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp4(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp5(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp1(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp2(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp3(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp4(Y)
| ~ rr(X,Y) ) ) ),
inference(canonicalize,[],[axiom_2]) ).
fof(normalize_0_2,plain,
! [X] :
( ~ cUnsatisfiable(X)
<=> ( ? [Y8,Y9,Y10,Y11,Y12] :
( Y8 != Y9
& Y8 != Y10
& Y8 != Y11
& Y8 != Y12
& Y9 != Y10
& Y9 != Y11
& Y9 != Y12
& Y10 != Y11
& Y10 != Y12
& Y11 != Y12
& rr(X,Y8)
& rr(X,Y9)
& rr(X,Y10)
& rr(X,Y11)
& rr(X,Y12) )
| ! [Y] :
( ~ cp1(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp2(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp3(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp4(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp5(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp1(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp2(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp3(Y)
| ~ rr(X,Y) )
| ! [Y] :
( ~ cp(Y)
| ~ cp4(Y)
| ~ rr(X,Y) ) ) ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [X,Y,Y0,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,Y10,Y11,Y12] :
( ( ~ cUnsatisfiable(X)
| cp(skolemFOFtoCNF_Y(X)) )
& ( ~ cUnsatisfiable(X)
| cp(skolemFOFtoCNF_Y_1(X)) )
& ( ~ cUnsatisfiable(X)
| cp(skolemFOFtoCNF_Y_2(X)) )
& ( ~ cUnsatisfiable(X)
| cp(skolemFOFtoCNF_Y_3(X)) )
& ( ~ cUnsatisfiable(X)
| cp1(skolemFOFtoCNF_Y_3(X)) )
& ( ~ cUnsatisfiable(X)
| cp1(skolemFOFtoCNF_Y_8(X)) )
& ( ~ cUnsatisfiable(X)
| cp2(skolemFOFtoCNF_Y_2(X)) )
& ( ~ cUnsatisfiable(X)
| cp2(skolemFOFtoCNF_Y_7(X)) )
& ( ~ cUnsatisfiable(X)
| cp3(skolemFOFtoCNF_Y_1(X)) )
& ( ~ cUnsatisfiable(X)
| cp3(skolemFOFtoCNF_Y_6(X)) )
& ( ~ cUnsatisfiable(X)
| cp4(skolemFOFtoCNF_Y(X)) )
& ( ~ cUnsatisfiable(X)
| cp4(skolemFOFtoCNF_Y_5(X)) )
& ( ~ cUnsatisfiable(X)
| cp5(skolemFOFtoCNF_Y_4(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_1(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_2(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_3(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_4(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_5(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_6(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_7(X)) )
& ( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_8(X)) )
& ( ~ cUnsatisfiable(X)
| ~ rr(X,Y8)
| ~ rr(X,Y9)
| ~ rr(X,Y10)
| ~ rr(X,Y11)
| ~ rr(X,Y12)
| Y8 = Y9
| Y8 = Y10
| Y8 = Y11
| Y8 = Y12
| Y9 = Y10
| Y9 = Y11
| Y9 = Y12
| Y10 = Y11
| Y10 = Y12
| Y11 = Y12 )
& ( skolemFOFtoCNF_Y0(X) != skolemFOFtoCNF_Y1(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y0(X) != skolemFOFtoCNF_Y2(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y0(X) != skolemFOFtoCNF_Y3(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y0(X) != skolemFOFtoCNF_Y4(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y1(X) != skolemFOFtoCNF_Y2(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y1(X) != skolemFOFtoCNF_Y3(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y1(X) != skolemFOFtoCNF_Y4(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y2(X) != skolemFOFtoCNF_Y3(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y2(X) != skolemFOFtoCNF_Y4(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( skolemFOFtoCNF_Y3(X) != skolemFOFtoCNF_Y4(X)
| ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X) )
& ( ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y0(X)) )
& ( ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y1(X)) )
& ( ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y2(X)) )
& ( ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y3(X)) )
& ( ~ cp(Y4)
| ~ cp(Y5)
| ~ cp(Y6)
| ~ cp(Y7)
| ~ cp1(Y)
| ~ cp1(Y4)
| ~ cp2(Y0)
| ~ cp2(Y5)
| ~ cp3(Y1)
| ~ cp3(Y6)
| ~ cp4(Y2)
| ~ cp4(Y7)
| ~ cp5(Y3)
| ~ rr(X,Y)
| ~ rr(X,Y0)
| ~ rr(X,Y1)
| ~ rr(X,Y2)
| ~ rr(X,Y3)
| ~ rr(X,Y4)
| ~ rr(X,Y5)
| ~ rr(X,Y6)
| ~ rr(X,Y7)
| cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y4(X)) ) ),
inference(clausify,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [X] :
( ~ cUnsatisfiable(X)
| cp3(skolemFOFtoCNF_Y_1(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [X] :
( ~ cUnsatisfiable(X)
| cp2(skolemFOFtoCNF_Y_2(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_6,plain,
! [X] :
( ~ cUnsatisfiable(X)
| cp1(skolemFOFtoCNF_Y_3(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_7,plain,
! [X] :
( ~ cp1(X)
| ( ~ cp2(X)
& ~ cp3(X)
& ~ cp4(X)
& ~ cp5(X) ) ),
inference(canonicalize,[],[axiom_3]) ).
fof(normalize_0_8,plain,
! [X] :
( ~ cp1(X)
| ( ~ cp2(X)
& ~ cp3(X)
& ~ cp4(X)
& ~ cp5(X) ) ),
inference(specialize,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [X] :
( ( ~ cp1(X)
| ~ cp2(X) )
& ( ~ cp1(X)
| ~ cp3(X) )
& ( ~ cp1(X)
| ~ cp4(X) )
& ( ~ cp1(X)
| ~ cp5(X) ) ),
inference(clausify,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [X] :
( ~ cp1(X)
| ~ cp5(X) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [X] :
( ~ cUnsatisfiable(X)
| cp5(skolemFOFtoCNF_Y_4(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_12,plain,
! [X] :
( ~ cp3(X)
| ( ~ cp4(X)
& ~ cp5(X) ) ),
inference(canonicalize,[],[axiom_5]) ).
fof(normalize_0_13,plain,
! [X] :
( ~ cp3(X)
| ( ~ cp4(X)
& ~ cp5(X) ) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [X] :
( ( ~ cp3(X)
| ~ cp4(X) )
& ( ~ cp3(X)
| ~ cp5(X) ) ),
inference(clausify,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [X] :
( ~ cp3(X)
| ~ cp5(X) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [X] :
( ~ cp4(X)
| ~ cp5(X) ),
inference(canonicalize,[],[axiom_6]) ).
fof(normalize_0_17,plain,
! [X] :
( ~ cp4(X)
| ~ cp5(X) ),
inference(specialize,[],[normalize_0_16]) ).
fof(normalize_0_18,plain,
! [X] :
( ~ cp2(X)
| ( ~ cp3(X)
& ~ cp4(X)
& ~ cp5(X) ) ),
inference(canonicalize,[],[axiom_4]) ).
fof(normalize_0_19,plain,
! [X] :
( ~ cp2(X)
| ( ~ cp3(X)
& ~ cp4(X)
& ~ cp5(X) ) ),
inference(specialize,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
! [X] :
( ( ~ cp2(X)
| ~ cp3(X) )
& ( ~ cp2(X)
| ~ cp4(X) )
& ( ~ cp2(X)
| ~ cp5(X) ) ),
inference(clausify,[],[normalize_0_19]) ).
fof(normalize_0_21,plain,
! [X] :
( ~ cp2(X)
| ~ cp5(X) ),
inference(conjunct,[],[normalize_0_20]) ).
fof(normalize_0_22,plain,
! [X] :
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_4(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_23,plain,
! [X] :
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_1(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_24,plain,
! [X] :
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_2(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_25,plain,
! [X] :
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_3(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_26,plain,
! [X] :
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_27,plain,
! [X,Y8,Y9,Y10,Y11,Y12] :
( ~ cUnsatisfiable(X)
| ~ rr(X,Y8)
| ~ rr(X,Y9)
| ~ rr(X,Y10)
| ~ rr(X,Y11)
| ~ rr(X,Y12)
| Y8 = Y9
| Y8 = Y10
| Y8 = Y11
| Y8 = Y12
| Y9 = Y10
| Y9 = Y11
| Y9 = Y12
| Y10 = Y11
| Y10 = Y12
| Y11 = Y12 ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_28,plain,
! [X] :
( ~ cUnsatisfiable(X)
| cp4(skolemFOFtoCNF_Y(X)) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_29,plain,
! [X] :
( ~ cp1(X)
| ~ cp4(X) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_30,plain,
! [X] :
( ~ cp1(X)
| ~ cp3(X) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_31,plain,
! [X] :
( ~ cp1(X)
| ~ cp2(X) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_32,plain,
! [X] :
( ~ cp2(X)
| ~ cp4(X) ),
inference(conjunct,[],[normalize_0_20]) ).
fof(normalize_0_33,plain,
! [X] :
( ~ cp2(X)
| ~ cp3(X) ),
inference(conjunct,[],[normalize_0_20]) ).
fof(normalize_0_34,plain,
! [X] :
( ~ cp3(X)
| ~ cp4(X) ),
inference(conjunct,[],[normalize_0_14]) ).
cnf(refute_0_0,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( ~ cUnsatisfiable(X)
| cp3(skolemFOFtoCNF_Y_1(X)) ),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_2,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_3,plain,
cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ cUnsatisfiable(X)
| cp2(skolemFOFtoCNF_Y_2(X)) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_6,plain,
cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_5]) ).
cnf(refute_0_7,plain,
( ~ cUnsatisfiable(X)
| cp1(skolemFOFtoCNF_Y_3(X)) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_8,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_7:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_9,plain,
cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_8]) ).
cnf(refute_0_10,plain,
( ~ cp1(X)
| ~ cp5(X) ),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_11,plain,
( ~ cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236))
| ~ cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_10:[bind(X,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_12,plain,
( ~ cUnsatisfiable(X)
| cp5(skolemFOFtoCNF_Y_4(X)) ),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_13,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_12:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_14,plain,
cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_13]) ).
cnf(refute_0_15,plain,
~ cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_14,refute_0_11]) ).
cnf(refute_0_16,plain,
( ~ cp3(X)
| ~ cp5(X) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_17,plain,
( ~ cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236))
| ~ cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_16:[bind(X,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_18,plain,
~ cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_14,refute_0_17]) ).
cnf(refute_0_19,plain,
( ~ cp4(X)
| ~ cp5(X) ),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_20,plain,
( ~ cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236))
| ~ cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_19:[bind(X,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_21,plain,
~ cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_14,refute_0_20]) ).
cnf(refute_0_22,plain,
( ~ cp2(X)
| ~ cp5(X) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_23,plain,
( ~ cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236))
| ~ cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_22:[bind(X,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_24,plain,
~ cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp5(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_14,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_4(X)) ),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_26,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_25:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_27,plain,
rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_26]) ).
cnf(refute_0_28,plain,
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_1(X)) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_29,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_28:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_30,plain,
rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_29]) ).
cnf(refute_0_31,plain,
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_2(X)) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_32,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_31:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_33,plain,
rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_32]) ).
cnf(refute_0_34,plain,
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y_3(X)) ),
inference(canonicalize,[],[normalize_0_25]) ).
cnf(refute_0_35,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_34:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_36,plain,
rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_35]) ).
cnf(refute_0_37,plain,
( ~ cUnsatisfiable(X)
| rr(X,skolemFOFtoCNF_Y(X)) ),
inference(canonicalize,[],[normalize_0_26]) ).
cnf(refute_0_38,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_37:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_39,plain,
rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_38]) ).
cnf(refute_0_40,plain,
( ~ cUnsatisfiable(X)
| ~ rr(X,Y8)
| ~ rr(X,Y9)
| ~ rr(X,Y10)
| ~ rr(X,Y11)
| ~ rr(X,Y12)
| Y8 = Y9
| Y8 = Y10
| Y8 = Y11
| Y8 = Y12
| Y9 = Y10
| Y9 = Y11
| Y9 = Y12
| Y10 = Y11
| Y10 = Y12
| Y11 = Y12 ),
inference(canonicalize,[],[normalize_0_27]) ).
cnf(refute_0_41,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| ~ rr(i2003_11_14_17_19_24236,X_128)
| ~ rr(i2003_11_14_17_19_24236,X_129)
| ~ rr(i2003_11_14_17_19_24236,X_130)
| ~ rr(i2003_11_14_17_19_24236,X_131)
| ~ rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| X_128 = X_129
| X_128 = X_130
| X_128 = X_131
| X_129 = X_130
| X_129 = X_131
| X_130 = X_131
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_128
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_129
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_130
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_131 ),
inference(subst,[],[refute_0_40:[bind(X,$fot(i2003_11_14_17_19_24236)),bind(Y8,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))),bind(Y9,$fot(X_128)),bind(Y10,$fot(X_129)),bind(Y11,$fot(X_130)),bind(Y12,$fot(X_131))]]) ).
cnf(refute_0_42,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| ~ rr(i2003_11_14_17_19_24236,X_128)
| ~ rr(i2003_11_14_17_19_24236,X_129)
| ~ rr(i2003_11_14_17_19_24236,X_130)
| ~ rr(i2003_11_14_17_19_24236,X_131)
| X_128 = X_129
| X_128 = X_130
| X_128 = X_131
| X_129 = X_130
| X_129 = X_131
| X_130 = X_131
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_128
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_129
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_130
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_131 ),
inference(resolve,[$cnf( rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_39,refute_0_41]) ).
cnf(refute_0_43,plain,
( ~ rr(i2003_11_14_17_19_24236,X_128)
| ~ rr(i2003_11_14_17_19_24236,X_129)
| ~ rr(i2003_11_14_17_19_24236,X_130)
| ~ rr(i2003_11_14_17_19_24236,X_131)
| X_128 = X_129
| X_128 = X_130
| X_128 = X_131
| X_129 = X_130
| X_129 = X_131
| X_130 = X_131
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_128
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_129
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_130
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_131 ),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_42]) ).
cnf(refute_0_44,plain,
( ~ rr(i2003_11_14_17_19_24236,X_133)
| ~ rr(i2003_11_14_17_19_24236,X_134)
| ~ rr(i2003_11_14_17_19_24236,X_135)
| ~ rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| X_133 = X_134
| X_133 = X_135
| X_134 = X_135
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_133
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_134
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_135
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_133
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_134
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_135 ),
inference(subst,[],[refute_0_43:[bind(X_128,$fot(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))),bind(X_129,$fot(X_133)),bind(X_130,$fot(X_134)),bind(X_131,$fot(X_135))]]) ).
cnf(refute_0_45,plain,
( ~ rr(i2003_11_14_17_19_24236,X_133)
| ~ rr(i2003_11_14_17_19_24236,X_134)
| ~ rr(i2003_11_14_17_19_24236,X_135)
| X_133 = X_134
| X_133 = X_135
| X_134 = X_135
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_133
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_134
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_135
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_133
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_134
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_135 ),
inference(resolve,[$cnf( rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_36,refute_0_44]) ).
cnf(refute_0_46,plain,
( ~ rr(i2003_11_14_17_19_24236,X_169)
| ~ rr(i2003_11_14_17_19_24236,X_170)
| ~ rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| X_169 = X_170
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_45:[bind(X_133,$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))),bind(X_134,$fot(X_169)),bind(X_135,$fot(X_170))]]) ).
cnf(refute_0_47,plain,
( ~ rr(i2003_11_14_17_19_24236,X_169)
| ~ rr(i2003_11_14_17_19_24236,X_170)
| X_169 = X_170
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_169
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_170
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_33,refute_0_46]) ).
cnf(refute_0_48,plain,
( ~ rr(i2003_11_14_17_19_24236,X_172)
| ~ rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_47:[bind(X_169,$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))),bind(X_170,$fot(X_172))]]) ).
cnf(refute_0_49,plain,
( ~ rr(i2003_11_14_17_19_24236,X_172)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = X_172
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_30,refute_0_48]) ).
cnf(refute_0_50,plain,
( ~ rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_49:[bind(X_172,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_51,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( rr(i2003_11_14_17_19_24236,skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_27,refute_0_50]) ).
cnf(refute_0_52,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_53,plain,
( X0 != X0
| X0 != Y13
| Y13 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y13)]]) ).
cnf(refute_0_54,plain,
( X0 != Y13
| Y13 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
( skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_56,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_51,refute_0_55]) ).
cnf(refute_0_57,plain,
( skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( ~ cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_58,plain,
( ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
( ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_58,refute_0_24]) ).
cnf(refute_0_60,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_6,refute_0_59]) ).
cnf(refute_0_61,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_62,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_60,refute_0_61]) ).
cnf(refute_0_63,plain,
( skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( ~ cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_64,plain,
( ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_62,refute_0_63]) ).
cnf(refute_0_65,plain,
( ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp4(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_64,refute_0_21]) ).
cnf(refute_0_66,plain,
( ~ cUnsatisfiable(X)
| cp4(skolemFOFtoCNF_Y(X)) ),
inference(canonicalize,[],[normalize_0_28]) ).
cnf(refute_0_67,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_66:[bind(X,$fot(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_68,plain,
cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_19_24236) )],[refute_0_0,refute_0_67]) ).
cnf(refute_0_69,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_68,refute_0_65]) ).
cnf(refute_0_70,plain,
( skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_71,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_69,refute_0_70]) ).
cnf(refute_0_72,plain,
( skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( ~ cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_73,plain,
( ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_71,refute_0_72]) ).
cnf(refute_0_74,plain,
( ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_73,refute_0_18]) ).
cnf(refute_0_75,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_3,refute_0_74]) ).
cnf(refute_0_76,plain,
( skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_77,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_75,refute_0_76]) ).
cnf(refute_0_78,plain,
( skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( ~ cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_79,plain,
( ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
( ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_4(i2003_11_14_17_19_24236)) )],[refute_0_79,refute_0_15]) ).
cnf(refute_0_81,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_9,refute_0_80]) ).
cnf(refute_0_82,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_83,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
( skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_85,plain,
( ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_83,refute_0_84]) ).
cnf(refute_0_86,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_9,refute_0_85]) ).
cnf(refute_0_87,plain,
( ~ cp1(X)
| ~ cp4(X) ),
inference(canonicalize,[],[normalize_0_29]) ).
cnf(refute_0_88,plain,
( ~ cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_87:[bind(X,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_89,plain,
~ cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_68,refute_0_88]) ).
cnf(refute_0_90,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_86,refute_0_89]) ).
cnf(refute_0_91,plain,
( skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_92,plain,
( ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_90,refute_0_91]) ).
cnf(refute_0_93,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_9,refute_0_92]) ).
cnf(refute_0_94,plain,
( ~ cp1(X)
| ~ cp3(X) ),
inference(canonicalize,[],[normalize_0_30]) ).
cnf(refute_0_95,plain,
( ~ cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_94:[bind(X,$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_96,plain,
~ cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_3,refute_0_95]) ).
cnf(refute_0_97,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_93,refute_0_96]) ).
cnf(refute_0_98,plain,
( skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_99,plain,
( ~ cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_97,refute_0_98]) ).
cnf(refute_0_100,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_3(i2003_11_14_17_19_24236)) )],[refute_0_9,refute_0_99]) ).
cnf(refute_0_101,plain,
( ~ cp1(X)
| ~ cp2(X) ),
inference(canonicalize,[],[normalize_0_31]) ).
cnf(refute_0_102,plain,
( ~ cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_101:[bind(X,$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_103,plain,
~ cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_6,refute_0_102]) ).
cnf(refute_0_104,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp1(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_100,refute_0_103]) ).
cnf(refute_0_105,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_106,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_104,refute_0_105]) ).
cnf(refute_0_107,plain,
( skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_108,plain,
( ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_106,refute_0_107]) ).
cnf(refute_0_109,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_6,refute_0_108]) ).
cnf(refute_0_110,plain,
( ~ cp2(X)
| ~ cp4(X) ),
inference(canonicalize,[],[normalize_0_32]) ).
cnf(refute_0_111,plain,
( ~ cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_110:[bind(X,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_112,plain,
~ cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_68,refute_0_111]) ).
cnf(refute_0_113,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) ),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_109,refute_0_112]) ).
cnf(refute_0_114,plain,
( skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_115,plain,
( ~ cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236))
| skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_113,refute_0_114]) ).
cnf(refute_0_116,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_2(i2003_11_14_17_19_24236)) )],[refute_0_6,refute_0_115]) ).
cnf(refute_0_117,plain,
( ~ cp2(X)
| ~ cp3(X) ),
inference(canonicalize,[],[normalize_0_33]) ).
cnf(refute_0_118,plain,
( ~ cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_117:[bind(X,$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_119,plain,
~ cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_3,refute_0_118]) ).
cnf(refute_0_120,plain,
skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236),
inference(resolve,[$cnf( cp2(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_116,refute_0_119]) ).
cnf(refute_0_121,plain,
( skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)
| skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236) ),
inference(subst,[],[refute_0_54:[bind(X0,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))),bind(Y13,$fot(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_122,plain,
skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) = skolemFOFtoCNF_Y(i2003_11_14_17_19_24236),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_120,refute_0_121]) ).
cnf(refute_0_123,plain,
( skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236) != skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)
| ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
introduced(tautology,[equality,[$cnf( cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) ),[0],$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))]]) ).
cnf(refute_0_124,plain,
( ~ cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236))
| cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236),skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_122,refute_0_123]) ).
cnf(refute_0_125,plain,
cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y_1(i2003_11_14_17_19_24236)) )],[refute_0_3,refute_0_124]) ).
cnf(refute_0_126,plain,
( ~ cp3(X)
| ~ cp4(X) ),
inference(canonicalize,[],[normalize_0_34]) ).
cnf(refute_0_127,plain,
( ~ cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236))
| ~ cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) ),
inference(subst,[],[refute_0_126:[bind(X,$fot(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)))]]) ).
cnf(refute_0_128,plain,
~ cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)),
inference(resolve,[$cnf( cp4(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_68,refute_0_127]) ).
cnf(refute_0_129,plain,
$false,
inference(resolve,[$cnf( cp3(skolemFOFtoCNF_Y(i2003_11_14_17_19_24236)) )],[refute_0_125,refute_0_128]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jun 7 11:46:35 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 40.45/40.63 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.45/40.63
% 40.45/40.63 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 40.45/40.65
%------------------------------------------------------------------------------