%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : KRS104+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n027.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:43 EDT 2022
% Result : Unsatisfiable 0.21s 0.39s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 20
% Syntax : Number of formulae : 205 ( 12 unt; 0 def)
% Number of atoms : 477 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 487 ( 215 ~; 190 |; 29 &)
% ( 51 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 260 ( 11 sgn 125 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_2,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ) ).
fof(axiom_3,axiom,
! [X] :
( cUnsatisfiablexcomp(X)
<=> ( ca_Cx7(X)
& ca_Cx8(X)
& ca_Cx6(X) ) ) ).
fof(axiom_4,axiom,
! [X] :
( cUnsatisfiablexcomp(X)
<=> ? [Y0] : ra_Px5(X,Y0) ) ).
fof(axiom_5,axiom,
! [X] :
( ca(X)
=> ca_Cx1(X) ) ).
fof(axiom_6,axiom,
! [X] :
( cb(X)
<=> ? [Y0] : ra_Px3(X,Y0) ) ).
fof(axiom_7,axiom,
! [X] :
( cb(X)
=> ccxcomp(X) ) ).
fof(axiom_8,axiom,
! [X] :
( cbxcomp(X)
<=> ~ ? [Y] : ra_Px3(X,Y) ) ).
fof(axiom_9,axiom,
! [X] :
( cc(X)
<=> ? [Y0] : ra_Px2(X,Y0) ) ).
fof(axiom_10,axiom,
! [X] :
( ccxcomp(X)
<=> ~ ? [Y] : ra_Px2(X,Y) ) ).
fof(axiom_11,axiom,
! [X] :
( ca_Cx1(X)
<=> ( cbxcomp(X)
& ccxcomp(X) ) ) ).
fof(axiom_14,axiom,
! [X] :
( ca_Cx6(X)
<=> ~ ? [Y] : ra_Px6(X,Y) ) ).
fof(axiom_15,axiom,
! [X] :
( ca_Cx6xcomp(X)
<=> ( ca(X)
& cb(X) ) ) ).
fof(axiom_16,axiom,
! [X] :
( ca_Cx6xcomp(X)
<=> ? [Y0] : ra_Px6(X,Y0) ) ).
fof(axiom_17,axiom,
! [X] :
( ca_Cx7(X)
<=> ? [Y0] : ra_Px7(X,Y0) ) ).
fof(axiom_18,axiom,
! [X] :
( ca_Cx7xcomp(X)
<=> ( cc(X)
& ca(X) ) ) ).
fof(axiom_19,axiom,
! [X] :
( ca_Cx7xcomp(X)
<=> ~ ? [Y] : ra_Px7(X,Y) ) ).
fof(axiom_20,axiom,
! [X] :
( ca_Cx8(X)
<=> ~ ? [Y] : ra_Px8(X,Y) ) ).
fof(axiom_21,axiom,
! [X] :
( ca_Cx8xcomp(X)
<=> ? [Y0] : ra_Px8(X,Y0) ) ).
fof(axiom_22,axiom,
! [X] :
( ca_Cx8xcomp(X)
<=> ( cc(X)
& cb(X) ) ) ).
fof(axiom_23,axiom,
cUnsatisfiable(i2003_11_14_17_20_50869) ).
fof(normalize_0_0,plain,
cUnsatisfiable(i2003_11_14_17_20_50869),
inference(canonicalize,[],[axiom_23]) ).
fof(normalize_0_1,plain,
! [X] :
( ~ cUnsatisfiable(X)
<=> ? [Y] : ra_Px5(X,Y) ),
inference(canonicalize,[],[axiom_2]) ).
fof(normalize_0_2,plain,
! [X] :
( ~ cUnsatisfiable(X)
<=> ? [Y] : ra_Px5(X,Y) ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [X,Y] :
( ( ~ cUnsatisfiable(X)
| ~ ra_Px5(X,Y) )
& ( cUnsatisfiable(X)
| ra_Px5(X,skolemFOFtoCNF_Y(X)) ) ),
inference(clausify,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [X,Y] :
( ~ cUnsatisfiable(X)
| ~ ra_Px5(X,Y) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [X] :
( ~ cUnsatisfiablexcomp(X)
<=> ! [Y0] : ~ ra_Px5(X,Y0) ),
inference(canonicalize,[],[axiom_4]) ).
fof(normalize_0_6,plain,
! [X] :
( ~ cUnsatisfiablexcomp(X)
<=> ! [Y0] : ~ ra_Px5(X,Y0) ),
inference(specialize,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [X,Y0] :
( ( ~ cUnsatisfiablexcomp(X)
| ra_Px5(X,skolemFOFtoCNF_Y0(X)) )
& ( ~ ra_Px5(X,Y0)
| cUnsatisfiablexcomp(X) ) ),
inference(clausify,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [X] :
( ~ cUnsatisfiablexcomp(X)
| ra_Px5(X,skolemFOFtoCNF_Y0(X)) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [X] :
( ~ cbxcomp(X)
<=> ? [Y] : ra_Px3(X,Y) ),
inference(canonicalize,[],[axiom_8]) ).
fof(normalize_0_10,plain,
! [X] :
( ~ cbxcomp(X)
<=> ? [Y] : ra_Px3(X,Y) ),
inference(specialize,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [X,Y] :
( ( ~ cbxcomp(X)
| ~ ra_Px3(X,Y) )
& ( cbxcomp(X)
| ra_Px3(X,skolemFOFtoCNF_Y_1(X)) ) ),
inference(clausify,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [X,Y] :
( ~ cbxcomp(X)
| ~ ra_Px3(X,Y) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [X] :
( ~ cb(X)
<=> ! [Y0] : ~ ra_Px3(X,Y0) ),
inference(canonicalize,[],[axiom_6]) ).
fof(normalize_0_14,plain,
! [X] :
( ~ cb(X)
<=> ! [Y0] : ~ ra_Px3(X,Y0) ),
inference(specialize,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [X,Y0] :
( ( ~ cb(X)
| ra_Px3(X,skolemFOFtoCNF_Y0_1(X)) )
& ( ~ ra_Px3(X,Y0)
| cb(X) ) ),
inference(clausify,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [X] :
( ~ cb(X)
| ra_Px3(X,skolemFOFtoCNF_Y0_1(X)) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
<=> ( ~ ca(X)
| ~ cb(X) ) ),
inference(canonicalize,[],[axiom_15]) ).
fof(normalize_0_18,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
<=> ( ~ ca(X)
| ~ cb(X) ) ),
inference(specialize,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [X] :
( ( ~ ca_Cx6xcomp(X)
| ca(X) )
& ( ~ ca_Cx6xcomp(X)
| cb(X) )
& ( ~ ca(X)
| ~ cb(X)
| ca_Cx6xcomp(X) ) ),
inference(clausify,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
| cb(X) ),
inference(conjunct,[],[normalize_0_19]) ).
fof(normalize_0_21,plain,
! [X] :
( ~ ca_Cx6(X)
<=> ? [Y] : ra_Px6(X,Y) ),
inference(canonicalize,[],[axiom_14]) ).
fof(normalize_0_22,plain,
! [X] :
( ~ ca_Cx6(X)
<=> ? [Y] : ra_Px6(X,Y) ),
inference(specialize,[],[normalize_0_21]) ).
fof(normalize_0_23,plain,
! [X,Y] :
( ( ~ ca_Cx6(X)
| ~ ra_Px6(X,Y) )
& ( ca_Cx6(X)
| ra_Px6(X,skolemFOFtoCNF_Y_4(X)) ) ),
inference(clausify,[],[normalize_0_22]) ).
fof(normalize_0_24,plain,
! [X] :
( ca_Cx6(X)
| ra_Px6(X,skolemFOFtoCNF_Y_4(X)) ),
inference(conjunct,[],[normalize_0_23]) ).
fof(normalize_0_25,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
<=> ! [Y0] : ~ ra_Px6(X,Y0) ),
inference(canonicalize,[],[axiom_16]) ).
fof(normalize_0_26,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
<=> ! [Y0] : ~ ra_Px6(X,Y0) ),
inference(specialize,[],[normalize_0_25]) ).
fof(normalize_0_27,plain,
! [X,Y0] :
( ( ~ ca_Cx6xcomp(X)
| ra_Px6(X,skolemFOFtoCNF_Y0_4(X)) )
& ( ~ ra_Px6(X,Y0)
| ca_Cx6xcomp(X) ) ),
inference(clausify,[],[normalize_0_26]) ).
fof(normalize_0_28,plain,
! [X,Y0] :
( ~ ra_Px6(X,Y0)
| ca_Cx6xcomp(X) ),
inference(conjunct,[],[normalize_0_27]) ).
fof(normalize_0_29,plain,
! [X] :
( ~ ca_Cx1(X)
<=> ( ~ cbxcomp(X)
| ~ ccxcomp(X) ) ),
inference(canonicalize,[],[axiom_11]) ).
fof(normalize_0_30,plain,
! [X] :
( ~ ca_Cx1(X)
<=> ( ~ cbxcomp(X)
| ~ ccxcomp(X) ) ),
inference(specialize,[],[normalize_0_29]) ).
fof(normalize_0_31,plain,
! [X] :
( ( ~ ca_Cx1(X)
| cbxcomp(X) )
& ( ~ ca_Cx1(X)
| ccxcomp(X) )
& ( ~ cbxcomp(X)
| ~ ccxcomp(X)
| ca_Cx1(X) ) ),
inference(clausify,[],[normalize_0_30]) ).
fof(normalize_0_32,plain,
! [X] :
( ~ ca_Cx1(X)
| cbxcomp(X) ),
inference(conjunct,[],[normalize_0_31]) ).
fof(normalize_0_33,plain,
! [X] :
( ~ ca(X)
| ca_Cx1(X) ),
inference(canonicalize,[],[axiom_5]) ).
fof(normalize_0_34,plain,
! [X] :
( ~ ca(X)
| ca_Cx1(X) ),
inference(specialize,[],[normalize_0_33]) ).
fof(normalize_0_35,plain,
! [X] :
( ~ ca_Cx6xcomp(X)
| ca(X) ),
inference(conjunct,[],[normalize_0_19]) ).
fof(normalize_0_36,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
<=> ( ~ ca(X)
| ~ cc(X) ) ),
inference(canonicalize,[],[axiom_18]) ).
fof(normalize_0_37,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
<=> ( ~ ca(X)
| ~ cc(X) ) ),
inference(specialize,[],[normalize_0_36]) ).
fof(normalize_0_38,plain,
! [X] :
( ( ~ ca_Cx7xcomp(X)
| ca(X) )
& ( ~ ca_Cx7xcomp(X)
| cc(X) )
& ( ~ ca(X)
| ~ cc(X)
| ca_Cx7xcomp(X) ) ),
inference(clausify,[],[normalize_0_37]) ).
fof(normalize_0_39,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
| ca(X) ),
inference(conjunct,[],[normalize_0_38]) ).
fof(normalize_0_40,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
<=> ? [Y] : ra_Px7(X,Y) ),
inference(canonicalize,[],[axiom_19]) ).
fof(normalize_0_41,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
<=> ? [Y] : ra_Px7(X,Y) ),
inference(specialize,[],[normalize_0_40]) ).
fof(normalize_0_42,plain,
! [X,Y] :
( ( ~ ca_Cx7xcomp(X)
| ~ ra_Px7(X,Y) )
& ( ca_Cx7xcomp(X)
| ra_Px7(X,skolemFOFtoCNF_Y_5(X)) ) ),
inference(clausify,[],[normalize_0_41]) ).
fof(normalize_0_43,plain,
! [X] :
( ca_Cx7xcomp(X)
| ra_Px7(X,skolemFOFtoCNF_Y_5(X)) ),
inference(conjunct,[],[normalize_0_42]) ).
fof(normalize_0_44,plain,
! [X] :
( ~ ca_Cx7(X)
<=> ! [Y0] : ~ ra_Px7(X,Y0) ),
inference(canonicalize,[],[axiom_17]) ).
fof(normalize_0_45,plain,
! [X] :
( ~ ca_Cx7(X)
<=> ! [Y0] : ~ ra_Px7(X,Y0) ),
inference(specialize,[],[normalize_0_44]) ).
fof(normalize_0_46,plain,
! [X,Y0] :
( ( ~ ca_Cx7(X)
| ra_Px7(X,skolemFOFtoCNF_Y0_5(X)) )
& ( ~ ra_Px7(X,Y0)
| ca_Cx7(X) ) ),
inference(clausify,[],[normalize_0_45]) ).
fof(normalize_0_47,plain,
! [X,Y0] :
( ~ ra_Px7(X,Y0)
| ca_Cx7(X) ),
inference(conjunct,[],[normalize_0_46]) ).
fof(normalize_0_48,plain,
! [X] :
( ~ cUnsatisfiablexcomp(X)
<=> ( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| ~ ca_Cx8(X) ) ),
inference(canonicalize,[],[axiom_3]) ).
fof(normalize_0_49,plain,
! [X] :
( ~ cUnsatisfiablexcomp(X)
<=> ( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| ~ ca_Cx8(X) ) ),
inference(specialize,[],[normalize_0_48]) ).
fof(normalize_0_50,plain,
! [X] :
( ( ~ cUnsatisfiablexcomp(X)
| ca_Cx6(X) )
& ( ~ cUnsatisfiablexcomp(X)
| ca_Cx7(X) )
& ( ~ cUnsatisfiablexcomp(X)
| ca_Cx8(X) )
& ( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| ~ ca_Cx8(X)
| cUnsatisfiablexcomp(X) ) ),
inference(clausify,[],[normalize_0_49]) ).
fof(normalize_0_51,plain,
! [X] :
( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| ~ ca_Cx8(X)
| cUnsatisfiablexcomp(X) ),
inference(conjunct,[],[normalize_0_50]) ).
fof(normalize_0_52,plain,
! [X] :
( ~ cb(X)
| ccxcomp(X) ),
inference(canonicalize,[],[axiom_7]) ).
fof(normalize_0_53,plain,
! [X] :
( ~ cb(X)
| ccxcomp(X) ),
inference(specialize,[],[normalize_0_52]) ).
fof(normalize_0_54,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
<=> ( ~ cb(X)
| ~ cc(X) ) ),
inference(canonicalize,[],[axiom_22]) ).
fof(normalize_0_55,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
<=> ( ~ cb(X)
| ~ cc(X) ) ),
inference(specialize,[],[normalize_0_54]) ).
fof(normalize_0_56,plain,
! [X] :
( ( ~ ca_Cx8xcomp(X)
| cb(X) )
& ( ~ ca_Cx8xcomp(X)
| cc(X) )
& ( ~ cb(X)
| ~ cc(X)
| ca_Cx8xcomp(X) ) ),
inference(clausify,[],[normalize_0_55]) ).
fof(normalize_0_57,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
| cb(X) ),
inference(conjunct,[],[normalize_0_56]) ).
fof(normalize_0_58,plain,
! [X] :
( ~ ca_Cx8(X)
<=> ? [Y] : ra_Px8(X,Y) ),
inference(canonicalize,[],[axiom_20]) ).
fof(normalize_0_59,plain,
! [X] :
( ~ ca_Cx8(X)
<=> ? [Y] : ra_Px8(X,Y) ),
inference(specialize,[],[normalize_0_58]) ).
fof(normalize_0_60,plain,
! [X,Y] :
( ( ~ ca_Cx8(X)
| ~ ra_Px8(X,Y) )
& ( ca_Cx8(X)
| ra_Px8(X,skolemFOFtoCNF_Y_6(X)) ) ),
inference(clausify,[],[normalize_0_59]) ).
fof(normalize_0_61,plain,
! [X] :
( ca_Cx8(X)
| ra_Px8(X,skolemFOFtoCNF_Y_6(X)) ),
inference(conjunct,[],[normalize_0_60]) ).
fof(normalize_0_62,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
<=> ! [Y0] : ~ ra_Px8(X,Y0) ),
inference(canonicalize,[],[axiom_21]) ).
fof(normalize_0_63,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
<=> ! [Y0] : ~ ra_Px8(X,Y0) ),
inference(specialize,[],[normalize_0_62]) ).
fof(normalize_0_64,plain,
! [X,Y0] :
( ( ~ ca_Cx8xcomp(X)
| ra_Px8(X,skolemFOFtoCNF_Y0_6(X)) )
& ( ~ ra_Px8(X,Y0)
| ca_Cx8xcomp(X) ) ),
inference(clausify,[],[normalize_0_63]) ).
fof(normalize_0_65,plain,
! [X,Y0] :
( ~ ra_Px8(X,Y0)
| ca_Cx8xcomp(X) ),
inference(conjunct,[],[normalize_0_64]) ).
fof(normalize_0_66,plain,
! [X] :
( ~ ccxcomp(X)
<=> ? [Y] : ra_Px2(X,Y) ),
inference(canonicalize,[],[axiom_10]) ).
fof(normalize_0_67,plain,
! [X] :
( ~ ccxcomp(X)
<=> ? [Y] : ra_Px2(X,Y) ),
inference(specialize,[],[normalize_0_66]) ).
fof(normalize_0_68,plain,
! [X,Y] :
( ( ~ ccxcomp(X)
| ~ ra_Px2(X,Y) )
& ( ccxcomp(X)
| ra_Px2(X,skolemFOFtoCNF_Y_2(X)) ) ),
inference(clausify,[],[normalize_0_67]) ).
fof(normalize_0_69,plain,
! [X,Y] :
( ~ ccxcomp(X)
| ~ ra_Px2(X,Y) ),
inference(conjunct,[],[normalize_0_68]) ).
fof(normalize_0_70,plain,
! [X] :
( ~ cc(X)
<=> ! [Y0] : ~ ra_Px2(X,Y0) ),
inference(canonicalize,[],[axiom_9]) ).
fof(normalize_0_71,plain,
! [X] :
( ~ cc(X)
<=> ! [Y0] : ~ ra_Px2(X,Y0) ),
inference(specialize,[],[normalize_0_70]) ).
fof(normalize_0_72,plain,
! [X,Y0] :
( ( ~ cc(X)
| ra_Px2(X,skolemFOFtoCNF_Y0_2(X)) )
& ( ~ ra_Px2(X,Y0)
| cc(X) ) ),
inference(clausify,[],[normalize_0_71]) ).
fof(normalize_0_73,plain,
! [X] :
( ~ cc(X)
| ra_Px2(X,skolemFOFtoCNF_Y0_2(X)) ),
inference(conjunct,[],[normalize_0_72]) ).
fof(normalize_0_74,plain,
! [X] :
( ~ ca_Cx8xcomp(X)
| cc(X) ),
inference(conjunct,[],[normalize_0_56]) ).
fof(normalize_0_75,plain,
! [X] :
( ~ ca_Cx7xcomp(X)
| cc(X) ),
inference(conjunct,[],[normalize_0_38]) ).
fof(normalize_0_76,plain,
! [X] :
( ~ ca_Cx1(X)
| ccxcomp(X) ),
inference(conjunct,[],[normalize_0_31]) ).
cnf(refute_0_0,plain,
cUnsatisfiable(i2003_11_14_17_20_50869),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( ~ cUnsatisfiable(X)
| ~ ra_Px5(X,Y) ),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_2,plain,
( ~ cUnsatisfiable(X_115)
| ~ ra_Px5(X_115,skolemFOFtoCNF_Y0(X_115)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_115)),bind(Y,$fot(skolemFOFtoCNF_Y0(X_115)))]]) ).
cnf(refute_0_3,plain,
( ~ cUnsatisfiablexcomp(X)
| ra_Px5(X,skolemFOFtoCNF_Y0(X)) ),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_4,plain,
( ~ cUnsatisfiablexcomp(X_112)
| ra_Px5(X_112,skolemFOFtoCNF_Y0(X_112)) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_112))]]) ).
cnf(refute_0_5,plain,
( ~ cbxcomp(X)
| ~ ra_Px3(X,Y) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_6,plain,
( ~ cbxcomp(X_97)
| ~ ra_Px3(X_97,skolemFOFtoCNF_Y0_1(X_97)) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(X_97)),bind(Y,$fot(skolemFOFtoCNF_Y0_1(X_97)))]]) ).
cnf(refute_0_7,plain,
( ~ cb(X)
| ra_Px3(X,skolemFOFtoCNF_Y0_1(X)) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_8,plain,
( ~ cb(X_60)
| ra_Px3(X_60,skolemFOFtoCNF_Y0_1(X_60)) ),
inference(subst,[],[refute_0_7:[bind(X,$fot(X_60))]]) ).
cnf(refute_0_9,plain,
( ~ ca_Cx6xcomp(X)
| cb(X) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_10,plain,
( ~ ca_Cx6xcomp(X_58)
| cb(X_58) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_58))]]) ).
cnf(refute_0_11,plain,
( ca_Cx6(X)
| ra_Px6(X,skolemFOFtoCNF_Y_4(X)) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_12,plain,
( ca_Cx6(X_56)
| ra_Px6(X_56,skolemFOFtoCNF_Y_4(X_56)) ),
inference(subst,[],[refute_0_11:[bind(X,$fot(X_56))]]) ).
cnf(refute_0_13,plain,
( ~ ra_Px6(X,Y0)
| ca_Cx6xcomp(X) ),
inference(canonicalize,[],[normalize_0_28]) ).
cnf(refute_0_14,plain,
( ~ ra_Px6(X_56,skolemFOFtoCNF_Y_4(X_56))
| ca_Cx6xcomp(X_56) ),
inference(subst,[],[refute_0_13:[bind(X,$fot(X_56)),bind(Y0,$fot(skolemFOFtoCNF_Y_4(X_56)))]]) ).
cnf(refute_0_15,plain,
( ca_Cx6(X_56)
| ca_Cx6xcomp(X_56) ),
inference(resolve,[$cnf( ra_Px6(X_56,skolemFOFtoCNF_Y_4(X_56)) )],[refute_0_12,refute_0_14]) ).
cnf(refute_0_16,plain,
( ca_Cx6(X_58)
| ca_Cx6xcomp(X_58) ),
inference(subst,[],[refute_0_15:[bind(X_56,$fot(X_58))]]) ).
cnf(refute_0_17,plain,
( ca_Cx6(X_58)
| cb(X_58) ),
inference(resolve,[$cnf( ca_Cx6xcomp(X_58) )],[refute_0_16,refute_0_10]) ).
cnf(refute_0_18,plain,
( ca_Cx6(X_60)
| cb(X_60) ),
inference(subst,[],[refute_0_17:[bind(X_58,$fot(X_60))]]) ).
cnf(refute_0_19,plain,
( ca_Cx6(X_60)
| ra_Px3(X_60,skolemFOFtoCNF_Y0_1(X_60)) ),
inference(resolve,[$cnf( cb(X_60) )],[refute_0_18,refute_0_8]) ).
cnf(refute_0_20,plain,
( ca_Cx6(X_97)
| ra_Px3(X_97,skolemFOFtoCNF_Y0_1(X_97)) ),
inference(subst,[],[refute_0_19:[bind(X_60,$fot(X_97))]]) ).
cnf(refute_0_21,plain,
( ~ cbxcomp(X_97)
| ca_Cx6(X_97) ),
inference(resolve,[$cnf( ra_Px3(X_97,skolemFOFtoCNF_Y0_1(X_97)) )],[refute_0_20,refute_0_6]) ).
cnf(refute_0_22,plain,
( ~ cbxcomp(X_107)
| ca_Cx6(X_107) ),
inference(subst,[],[refute_0_21:[bind(X_97,$fot(X_107))]]) ).
cnf(refute_0_23,plain,
( ~ ca_Cx1(X)
| cbxcomp(X) ),
inference(canonicalize,[],[normalize_0_32]) ).
cnf(refute_0_24,plain,
( ~ ca_Cx1(X_106)
| cbxcomp(X_106) ),
inference(subst,[],[refute_0_23:[bind(X,$fot(X_106))]]) ).
cnf(refute_0_25,plain,
( ~ ca(X)
| ca_Cx1(X) ),
inference(canonicalize,[],[normalize_0_34]) ).
cnf(refute_0_26,plain,
( ~ ca(X_105)
| ca_Cx1(X_105) ),
inference(subst,[],[refute_0_25:[bind(X,$fot(X_105))]]) ).
cnf(refute_0_27,plain,
( ~ ca_Cx6xcomp(X)
| ca(X) ),
inference(canonicalize,[],[normalize_0_35]) ).
cnf(refute_0_28,plain,
( ~ ca_Cx6xcomp(X_58)
| ca(X_58) ),
inference(subst,[],[refute_0_27:[bind(X,$fot(X_58))]]) ).
cnf(refute_0_29,plain,
( ca(X_58)
| ca_Cx6(X_58) ),
inference(resolve,[$cnf( ca_Cx6xcomp(X_58) )],[refute_0_16,refute_0_28]) ).
cnf(refute_0_30,plain,
( ca(X_104)
| ca_Cx6(X_104) ),
inference(subst,[],[refute_0_29:[bind(X_58,$fot(X_104))]]) ).
cnf(refute_0_31,plain,
( ~ ca_Cx7xcomp(X)
| ca(X) ),
inference(canonicalize,[],[normalize_0_39]) ).
cnf(refute_0_32,plain,
( ~ ca_Cx7xcomp(X_64)
| ca(X_64) ),
inference(subst,[],[refute_0_31:[bind(X,$fot(X_64))]]) ).
cnf(refute_0_33,plain,
( ca_Cx7xcomp(X)
| ra_Px7(X,skolemFOFtoCNF_Y_5(X)) ),
inference(canonicalize,[],[normalize_0_43]) ).
cnf(refute_0_34,plain,
( ca_Cx7xcomp(X_62)
| ra_Px7(X_62,skolemFOFtoCNF_Y_5(X_62)) ),
inference(subst,[],[refute_0_33:[bind(X,$fot(X_62))]]) ).
cnf(refute_0_35,plain,
( ~ ra_Px7(X,Y0)
| ca_Cx7(X) ),
inference(canonicalize,[],[normalize_0_47]) ).
cnf(refute_0_36,plain,
( ~ ra_Px7(X_62,skolemFOFtoCNF_Y_5(X_62))
| ca_Cx7(X_62) ),
inference(subst,[],[refute_0_35:[bind(X,$fot(X_62)),bind(Y0,$fot(skolemFOFtoCNF_Y_5(X_62)))]]) ).
cnf(refute_0_37,plain,
( ca_Cx7(X_62)
| ca_Cx7xcomp(X_62) ),
inference(resolve,[$cnf( ra_Px7(X_62,skolemFOFtoCNF_Y_5(X_62)) )],[refute_0_34,refute_0_36]) ).
cnf(refute_0_38,plain,
( ca_Cx7(X_64)
| ca_Cx7xcomp(X_64) ),
inference(subst,[],[refute_0_37:[bind(X_62,$fot(X_64))]]) ).
cnf(refute_0_39,plain,
( ca(X_64)
| ca_Cx7(X_64) ),
inference(resolve,[$cnf( ca_Cx7xcomp(X_64) )],[refute_0_38,refute_0_32]) ).
cnf(refute_0_40,plain,
( ca(X_103)
| ca_Cx7(X_103) ),
inference(subst,[],[refute_0_39:[bind(X_64,$fot(X_103))]]) ).
cnf(refute_0_41,plain,
( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| ~ ca_Cx8(X)
| cUnsatisfiablexcomp(X) ),
inference(canonicalize,[],[normalize_0_51]) ).
cnf(refute_0_42,plain,
( ~ cb(X)
| ccxcomp(X) ),
inference(canonicalize,[],[normalize_0_53]) ).
cnf(refute_0_43,plain,
( ~ cb(X_80)
| ccxcomp(X_80) ),
inference(subst,[],[refute_0_42:[bind(X,$fot(X_80))]]) ).
cnf(refute_0_44,plain,
( ~ ca_Cx8xcomp(X)
| cb(X) ),
inference(canonicalize,[],[normalize_0_57]) ).
cnf(refute_0_45,plain,
( ~ ca_Cx8xcomp(X_79)
| cb(X_79) ),
inference(subst,[],[refute_0_44:[bind(X,$fot(X_79))]]) ).
cnf(refute_0_46,plain,
( ca_Cx8(X)
| ra_Px8(X,skolemFOFtoCNF_Y_6(X)) ),
inference(canonicalize,[],[normalize_0_61]) ).
cnf(refute_0_47,plain,
( ca_Cx8(X_77)
| ra_Px8(X_77,skolemFOFtoCNF_Y_6(X_77)) ),
inference(subst,[],[refute_0_46:[bind(X,$fot(X_77))]]) ).
cnf(refute_0_48,plain,
( ~ ra_Px8(X,Y0)
| ca_Cx8xcomp(X) ),
inference(canonicalize,[],[normalize_0_65]) ).
cnf(refute_0_49,plain,
( ~ ra_Px8(X_77,skolemFOFtoCNF_Y_6(X_77))
| ca_Cx8xcomp(X_77) ),
inference(subst,[],[refute_0_48:[bind(X,$fot(X_77)),bind(Y0,$fot(skolemFOFtoCNF_Y_6(X_77)))]]) ).
cnf(refute_0_50,plain,
( ca_Cx8(X_77)
| ca_Cx8xcomp(X_77) ),
inference(resolve,[$cnf( ra_Px8(X_77,skolemFOFtoCNF_Y_6(X_77)) )],[refute_0_47,refute_0_49]) ).
cnf(refute_0_51,plain,
( ca_Cx8(X_79)
| ca_Cx8xcomp(X_79) ),
inference(subst,[],[refute_0_50:[bind(X_77,$fot(X_79))]]) ).
cnf(refute_0_52,plain,
( ca_Cx8(X_79)
| cb(X_79) ),
inference(resolve,[$cnf( ca_Cx8xcomp(X_79) )],[refute_0_51,refute_0_45]) ).
cnf(refute_0_53,plain,
( ca_Cx8(X_80)
| cb(X_80) ),
inference(subst,[],[refute_0_52:[bind(X_79,$fot(X_80))]]) ).
cnf(refute_0_54,plain,
( ca_Cx8(X_80)
| ccxcomp(X_80) ),
inference(resolve,[$cnf( cb(X_80) )],[refute_0_53,refute_0_43]) ).
cnf(refute_0_55,plain,
( ca_Cx8(X_88)
| ccxcomp(X_88) ),
inference(subst,[],[refute_0_54:[bind(X_80,$fot(X_88))]]) ).
cnf(refute_0_56,plain,
( ~ ccxcomp(X)
| ~ ra_Px2(X,Y) ),
inference(canonicalize,[],[normalize_0_69]) ).
cnf(refute_0_57,plain,
( ~ ccxcomp(X_87)
| ~ ra_Px2(X_87,skolemFOFtoCNF_Y0_2(X_87)) ),
inference(subst,[],[refute_0_56:[bind(X,$fot(X_87)),bind(Y,$fot(skolemFOFtoCNF_Y0_2(X_87)))]]) ).
cnf(refute_0_58,plain,
( ~ cc(X)
| ra_Px2(X,skolemFOFtoCNF_Y0_2(X)) ),
inference(canonicalize,[],[normalize_0_73]) ).
cnf(refute_0_59,plain,
( ~ cc(X_81)
| ra_Px2(X_81,skolemFOFtoCNF_Y0_2(X_81)) ),
inference(subst,[],[refute_0_58:[bind(X,$fot(X_81))]]) ).
cnf(refute_0_60,plain,
( ~ ca_Cx8xcomp(X)
| cc(X) ),
inference(canonicalize,[],[normalize_0_74]) ).
cnf(refute_0_61,plain,
( ~ ca_Cx8xcomp(X_79)
| cc(X_79) ),
inference(subst,[],[refute_0_60:[bind(X,$fot(X_79))]]) ).
cnf(refute_0_62,plain,
( ca_Cx8(X_79)
| cc(X_79) ),
inference(resolve,[$cnf( ca_Cx8xcomp(X_79) )],[refute_0_51,refute_0_61]) ).
cnf(refute_0_63,plain,
( ca_Cx8(X_81)
| cc(X_81) ),
inference(subst,[],[refute_0_62:[bind(X_79,$fot(X_81))]]) ).
cnf(refute_0_64,plain,
( ca_Cx8(X_81)
| ra_Px2(X_81,skolemFOFtoCNF_Y0_2(X_81)) ),
inference(resolve,[$cnf( cc(X_81) )],[refute_0_63,refute_0_59]) ).
cnf(refute_0_65,plain,
( ca_Cx8(X_87)
| ra_Px2(X_87,skolemFOFtoCNF_Y0_2(X_87)) ),
inference(subst,[],[refute_0_64:[bind(X_81,$fot(X_87))]]) ).
cnf(refute_0_66,plain,
( ~ ccxcomp(X_87)
| ca_Cx8(X_87) ),
inference(resolve,[$cnf( ra_Px2(X_87,skolemFOFtoCNF_Y0_2(X_87)) )],[refute_0_65,refute_0_57]) ).
cnf(refute_0_67,plain,
( ~ ccxcomp(X_88)
| ca_Cx8(X_88) ),
inference(subst,[],[refute_0_66:[bind(X_87,$fot(X_88))]]) ).
cnf(refute_0_68,plain,
ca_Cx8(X_88),
inference(resolve,[$cnf( ccxcomp(X_88) )],[refute_0_55,refute_0_67]) ).
cnf(refute_0_69,plain,
ca_Cx8(X),
inference(subst,[],[refute_0_68:[bind(X_88,$fot(X))]]) ).
cnf(refute_0_70,plain,
( ~ ca_Cx6(X)
| ~ ca_Cx7(X)
| cUnsatisfiablexcomp(X) ),
inference(resolve,[$cnf( ca_Cx8(X) )],[refute_0_69,refute_0_41]) ).
cnf(refute_0_71,plain,
( ~ ca_Cx6(X_103)
| ~ ca_Cx7(X_103)
| cUnsatisfiablexcomp(X_103) ),
inference(subst,[],[refute_0_70:[bind(X,$fot(X_103))]]) ).
cnf(refute_0_72,plain,
( ~ ca_Cx6(X_103)
| cUnsatisfiablexcomp(X_103)
| ca(X_103) ),
inference(resolve,[$cnf( ca_Cx7(X_103) )],[refute_0_40,refute_0_71]) ).
cnf(refute_0_73,plain,
( ~ ca_Cx6(X_104)
| cUnsatisfiablexcomp(X_104)
| ca(X_104) ),
inference(subst,[],[refute_0_72:[bind(X_103,$fot(X_104))]]) ).
cnf(refute_0_74,plain,
( cUnsatisfiablexcomp(X_104)
| ca(X_104) ),
inference(resolve,[$cnf( ca_Cx6(X_104) )],[refute_0_30,refute_0_73]) ).
cnf(refute_0_75,plain,
( cUnsatisfiablexcomp(X_105)
| ca(X_105) ),
inference(subst,[],[refute_0_74:[bind(X_104,$fot(X_105))]]) ).
cnf(refute_0_76,plain,
( cUnsatisfiablexcomp(X_105)
| ca_Cx1(X_105) ),
inference(resolve,[$cnf( ca(X_105) )],[refute_0_75,refute_0_26]) ).
cnf(refute_0_77,plain,
( cUnsatisfiablexcomp(X_106)
| ca_Cx1(X_106) ),
inference(subst,[],[refute_0_76:[bind(X_105,$fot(X_106))]]) ).
cnf(refute_0_78,plain,
( cUnsatisfiablexcomp(X_106)
| cbxcomp(X_106) ),
inference(resolve,[$cnf( ca_Cx1(X_106) )],[refute_0_77,refute_0_24]) ).
cnf(refute_0_79,plain,
( cUnsatisfiablexcomp(X_107)
| cbxcomp(X_107) ),
inference(subst,[],[refute_0_78:[bind(X_106,$fot(X_107))]]) ).
cnf(refute_0_80,plain,
( cUnsatisfiablexcomp(X_107)
| ca_Cx6(X_107) ),
inference(resolve,[$cnf( cbxcomp(X_107) )],[refute_0_79,refute_0_22]) ).
cnf(refute_0_81,plain,
( cUnsatisfiablexcomp(X_111)
| ca_Cx6(X_111) ),
inference(subst,[],[refute_0_80:[bind(X_107,$fot(X_111))]]) ).
cnf(refute_0_82,plain,
( ~ ca_Cx6(X_110)
| ~ ca_Cx7(X_110)
| cUnsatisfiablexcomp(X_110) ),
inference(subst,[],[refute_0_70:[bind(X,$fot(X_110))]]) ).
cnf(refute_0_83,plain,
( ~ ccxcomp(X_67)
| ~ ra_Px2(X_67,skolemFOFtoCNF_Y0_2(X_67)) ),
inference(subst,[],[refute_0_56:[bind(X,$fot(X_67)),bind(Y,$fot(skolemFOFtoCNF_Y0_2(X_67)))]]) ).
cnf(refute_0_84,plain,
( ~ cc(X_65)
| ra_Px2(X_65,skolemFOFtoCNF_Y0_2(X_65)) ),
inference(subst,[],[refute_0_58:[bind(X,$fot(X_65))]]) ).
cnf(refute_0_85,plain,
( ~ ca_Cx7xcomp(X)
| cc(X) ),
inference(canonicalize,[],[normalize_0_75]) ).
cnf(refute_0_86,plain,
( ~ ca_Cx7xcomp(X_64)
| cc(X_64) ),
inference(subst,[],[refute_0_85:[bind(X,$fot(X_64))]]) ).
cnf(refute_0_87,plain,
( ca_Cx7(X_64)
| cc(X_64) ),
inference(resolve,[$cnf( ca_Cx7xcomp(X_64) )],[refute_0_38,refute_0_86]) ).
cnf(refute_0_88,plain,
( ca_Cx7(X_65)
| cc(X_65) ),
inference(subst,[],[refute_0_87:[bind(X_64,$fot(X_65))]]) ).
cnf(refute_0_89,plain,
( ca_Cx7(X_65)
| ra_Px2(X_65,skolemFOFtoCNF_Y0_2(X_65)) ),
inference(resolve,[$cnf( cc(X_65) )],[refute_0_88,refute_0_84]) ).
cnf(refute_0_90,plain,
( ca_Cx7(X_67)
| ra_Px2(X_67,skolemFOFtoCNF_Y0_2(X_67)) ),
inference(subst,[],[refute_0_89:[bind(X_65,$fot(X_67))]]) ).
cnf(refute_0_91,plain,
( ~ ccxcomp(X_67)
| ca_Cx7(X_67) ),
inference(resolve,[$cnf( ra_Px2(X_67,skolemFOFtoCNF_Y0_2(X_67)) )],[refute_0_90,refute_0_83]) ).
cnf(refute_0_92,plain,
( ~ ccxcomp(X_109)
| ca_Cx7(X_109) ),
inference(subst,[],[refute_0_91:[bind(X_67,$fot(X_109))]]) ).
cnf(refute_0_93,plain,
( ~ ca_Cx1(X)
| ccxcomp(X) ),
inference(canonicalize,[],[normalize_0_76]) ).
cnf(refute_0_94,plain,
( ~ ca_Cx1(X_106)
| ccxcomp(X_106) ),
inference(subst,[],[refute_0_93:[bind(X,$fot(X_106))]]) ).
cnf(refute_0_95,plain,
( cUnsatisfiablexcomp(X_106)
| ccxcomp(X_106) ),
inference(resolve,[$cnf( ca_Cx1(X_106) )],[refute_0_77,refute_0_94]) ).
cnf(refute_0_96,plain,
( cUnsatisfiablexcomp(X_109)
| ccxcomp(X_109) ),
inference(subst,[],[refute_0_95:[bind(X_106,$fot(X_109))]]) ).
cnf(refute_0_97,plain,
( cUnsatisfiablexcomp(X_109)
| ca_Cx7(X_109) ),
inference(resolve,[$cnf( ccxcomp(X_109) )],[refute_0_96,refute_0_92]) ).
cnf(refute_0_98,plain,
( cUnsatisfiablexcomp(X_110)
| ca_Cx7(X_110) ),
inference(subst,[],[refute_0_97:[bind(X_109,$fot(X_110))]]) ).
cnf(refute_0_99,plain,
( ~ ca_Cx6(X_110)
| cUnsatisfiablexcomp(X_110) ),
inference(resolve,[$cnf( ca_Cx7(X_110) )],[refute_0_98,refute_0_82]) ).
cnf(refute_0_100,plain,
( ~ ca_Cx6(X_111)
| cUnsatisfiablexcomp(X_111) ),
inference(subst,[],[refute_0_99:[bind(X_110,$fot(X_111))]]) ).
cnf(refute_0_101,plain,
cUnsatisfiablexcomp(X_111),
inference(resolve,[$cnf( ca_Cx6(X_111) )],[refute_0_81,refute_0_100]) ).
cnf(refute_0_102,plain,
cUnsatisfiablexcomp(X_112),
inference(subst,[],[refute_0_101:[bind(X_111,$fot(X_112))]]) ).
cnf(refute_0_103,plain,
ra_Px5(X_112,skolemFOFtoCNF_Y0(X_112)),
inference(resolve,[$cnf( cUnsatisfiablexcomp(X_112) )],[refute_0_102,refute_0_4]) ).
cnf(refute_0_104,plain,
ra_Px5(X_115,skolemFOFtoCNF_Y0(X_115)),
inference(subst,[],[refute_0_103:[bind(X_112,$fot(X_115))]]) ).
cnf(refute_0_105,plain,
~ cUnsatisfiable(X_115),
inference(resolve,[$cnf( ra_Px5(X_115,skolemFOFtoCNF_Y0(X_115)) )],[refute_0_104,refute_0_2]) ).
cnf(refute_0_106,plain,
~ cUnsatisfiable(i2003_11_14_17_20_50869),
inference(subst,[],[refute_0_105:[bind(X_115,$fot(i2003_11_14_17_20_50869))]]) ).
cnf(refute_0_107,plain,
$false,
inference(resolve,[$cnf( cUnsatisfiable(i2003_11_14_17_20_50869) )],[refute_0_0,refute_0_106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : KRS104+1 : TPTP v8.1.0. Released v3.1.0.
% 0.04/0.15 % Command : metis --show proof --show saturation %s
% 0.14/0.36 % Computer : n027.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Tue Jun 7 09:26:40 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.14/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.21/0.39 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.39
% 0.21/0.39 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.21/0.41
%------------------------------------------------------------------------------