%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SEU368+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n023.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 : Tue Jul 19 12:40:40 EDT 2022
% Result : Theorem 51.94s 52.18s
% Output : CNFRefutation 52.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 28
% Syntax : Number of formulae : 178 ( 70 unt; 0 def)
% Number of atoms : 345 ( 206 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 317 ( 150 ~; 132 |; 23 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 11 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 255 ( 16 sgn 108 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(free_g1_orders_2,axiom,
! [A,B] :
( relation_of2(B,A,A)
=> ! [C,D] :
( rel_str_of(A,B) = rel_str_of(C,D)
=> ( A = C
& B = D ) ) ) ).
fof(abstractness_v1_orders_2,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ) ).
fof(dt_k1_yellow_1,axiom,
! [A] :
( reflexive(inclusion_order(A))
& antisymmetric(inclusion_order(A))
& transitive(inclusion_order(A))
& v1_partfun1(inclusion_order(A),A,A)
& relation_of2_as_subset(inclusion_order(A),A,A) ) ).
fof(dt_k2_yellow_1,axiom,
! [A] :
( strict_rel_str(incl_POSet(A))
& rel_str(incl_POSet(A)) ) ).
fof(dt_u1_orders_2,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) ).
fof(d1_yellow_1,axiom,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)) ).
fof(t1_yellow_1,conjecture,
! [A] :
( the_carrier(incl_POSet(A)) = A
& the_InternalRel(incl_POSet(A)) = inclusion_order(A) ) ).
fof(subgoal_0,plain,
! [A] : the_carrier(incl_POSet(A)) = A,
inference(strip,[],[t1_yellow_1]) ).
fof(subgoal_1,plain,
! [A] :
( the_carrier(incl_POSet(A)) = A
=> the_InternalRel(incl_POSet(A)) = inclusion_order(A) ),
inference(strip,[],[t1_yellow_1]) ).
fof(negate_0_0,plain,
~ ! [A] : the_carrier(incl_POSet(A)) = A,
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [A] : the_carrier(incl_POSet(A)) != A,
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) != skolemFOFtoCNF_A_7,
inference(skolemize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
( ! [A] : rel_str(incl_POSet(A))
& ! [A] : strict_rel_str(incl_POSet(A)) ),
inference(canonicalize,[],[dt_k2_yellow_1]) ).
fof(normalize_0_3,plain,
! [A] : rel_str(incl_POSet(A)),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [A] : rel_str(incl_POSet(A)),
inference(specialize,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [A] :
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(canonicalize,[],[dt_u1_orders_2]) ).
fof(normalize_0_6,plain,
! [A] :
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(specialize,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [A,B,C] :
( ~ relation_of2(C,A,B)
<=> ~ relation_of2_as_subset(C,A,B) ),
inference(canonicalize,[],[redefinition_m2_relset_1]) ).
fof(normalize_0_8,plain,
! [A,B,C] :
( ~ relation_of2(C,A,B)
<=> ~ relation_of2_as_subset(C,A,B) ),
inference(specialize,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ) ),
inference(clausify,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [A,B,C] :
( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [A,B] :
( ~ relation_of2(B,A,A)
| ! [C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ( A = C
& B = D ) ) ),
inference(canonicalize,[],[free_g1_orders_2]) ).
fof(normalize_0_12,plain,
! [A,B] :
( ~ relation_of2(B,A,A)
| ! [C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ( A = C
& B = D ) ) ),
inference(specialize,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [A,B,C,D] :
( ( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C )
& ( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| B = D ) ),
inference(clausify,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [A,B,C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C ),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [A] : strict_rel_str(incl_POSet(A)),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_16,plain,
! [A] : strict_rel_str(incl_POSet(A)),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [A] :
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(canonicalize,[],[abstractness_v1_orders_2]) ).
fof(normalize_0_18,plain,
! [A] :
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(specialize,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(canonicalize,[],[d1_yellow_1]) ).
fof(normalize_0_20,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(specialize,[],[normalize_0_19]) ).
cnf(refute_0_0,plain,
the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) != skolemFOFtoCNF_A_7,
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
rel_str(incl_POSet(A)),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_2,plain,
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_3,plain,
( ~ rel_str(incl_POSet(A))
| relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))) ),
inference(subst,[],[refute_0_2:[bind(A,$fot(incl_POSet(A)))]]) ).
cnf(refute_0_4,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))),
inference(resolve,[$cnf( rel_str(incl_POSet(A)) )],[refute_0_1,refute_0_3]) ).
cnf(refute_0_5,plain,
( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_6,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A)))
| relation_of2(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))) ),
inference(subst,[],[refute_0_5:[bind(A,$fot(the_carrier(incl_POSet(A)))),bind(B,$fot(the_carrier(incl_POSet(A)))),bind(C,$fot(the_InternalRel(incl_POSet(A))))]]) ).
cnf(refute_0_7,plain,
relation_of2(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))),
inference(resolve,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))) )],[refute_0_4,refute_0_6]) ).
cnf(refute_0_8,plain,
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_9,plain,
( rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != rel_str_of(X_295,X_296)
| ~ relation_of2(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A)))
| the_carrier(incl_POSet(A)) = X_295 ),
inference(subst,[],[refute_0_8:[bind(A,$fot(the_carrier(incl_POSet(A)))),bind(B,$fot(the_InternalRel(incl_POSet(A)))),bind(C,$fot(X_295)),bind(D,$fot(X_296))]]) ).
cnf(refute_0_10,plain,
( rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != rel_str_of(X_295,X_296)
| the_carrier(incl_POSet(A)) = X_295 ),
inference(resolve,[$cnf( relation_of2(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))) )],[refute_0_7,refute_0_9]) ).
cnf(refute_0_11,plain,
strict_rel_str(incl_POSet(A)),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_12,plain,
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_13,plain,
( ~ rel_str(incl_POSet(A))
| ~ strict_rel_str(incl_POSet(A))
| incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
inference(subst,[],[refute_0_12:[bind(A,$fot(incl_POSet(A)))]]) ).
cnf(refute_0_14,plain,
( ~ rel_str(incl_POSet(A))
| incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
inference(resolve,[$cnf( strict_rel_str(incl_POSet(A)) )],[refute_0_11,refute_0_13]) ).
cnf(refute_0_15,plain,
incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),
inference(resolve,[$cnf( rel_str(incl_POSet(A)) )],[refute_0_1,refute_0_14]) ).
cnf(refute_0_16,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_17,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_18,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_16,refute_0_17]) ).
cnf(refute_0_19,plain,
( incl_POSet(A) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = incl_POSet(A) ),
inference(subst,[],[refute_0_18:[bind(X,$fot(incl_POSet(A))),bind(Y,$fot(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))))]]) ).
cnf(refute_0_20,plain,
rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = incl_POSet(A),
inference(resolve,[$cnf( $equal(incl_POSet(A),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) )],[refute_0_15,refute_0_19]) ).
cnf(refute_0_21,plain,
( incl_POSet(A) != rel_str_of(X_295,X_296)
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != incl_POSet(A)
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(X_295,X_296) ),
introduced(tautology,[equality,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),incl_POSet(A)) ),[1],$fot(rel_str_of(X_295,X_296))]]) ).
cnf(refute_0_22,plain,
( incl_POSet(A) != rel_str_of(X_295,X_296)
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(X_295,X_296) ),
inference(resolve,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),incl_POSet(A)) )],[refute_0_20,refute_0_21]) ).
cnf(refute_0_23,plain,
( incl_POSet(A) != rel_str_of(X_295,X_296)
| the_carrier(incl_POSet(A)) = X_295 ),
inference(resolve,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),rel_str_of(X_295,X_296)) )],[refute_0_22,refute_0_10]) ).
cnf(refute_0_24,plain,
( incl_POSet(X_337) != rel_str_of(X_338,inclusion_order(X_338))
| the_carrier(incl_POSet(X_337)) = X_338 ),
inference(subst,[],[refute_0_23:[bind(A,$fot(X_337)),bind(X_295,$fot(X_338)),bind(X_296,$fot(inclusion_order(X_338)))]]) ).
cnf(refute_0_25,plain,
incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_26,plain,
incl_POSet(X_338) = rel_str_of(X_338,inclusion_order(X_338)),
inference(subst,[],[refute_0_25:[bind(A,$fot(X_338))]]) ).
cnf(refute_0_27,plain,
( incl_POSet(X_338) != rel_str_of(X_338,inclusion_order(X_338))
| rel_str_of(X_338,inclusion_order(X_338)) = incl_POSet(X_338) ),
inference(subst,[],[refute_0_18:[bind(X,$fot(incl_POSet(X_338))),bind(Y,$fot(rel_str_of(X_338,inclusion_order(X_338))))]]) ).
cnf(refute_0_28,plain,
rel_str_of(X_338,inclusion_order(X_338)) = incl_POSet(X_338),
inference(resolve,[$cnf( $equal(incl_POSet(X_338),rel_str_of(X_338,inclusion_order(X_338))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
( incl_POSet(X_337) != incl_POSet(X_338)
| rel_str_of(X_338,inclusion_order(X_338)) != incl_POSet(X_338)
| incl_POSet(X_337) = rel_str_of(X_338,inclusion_order(X_338)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(incl_POSet(X_337),rel_str_of(X_338,inclusion_order(X_338))) ),[1],$fot(incl_POSet(X_338))]]) ).
cnf(refute_0_30,plain,
( incl_POSet(X_337) != incl_POSet(X_338)
| incl_POSet(X_337) = rel_str_of(X_338,inclusion_order(X_338)) ),
inference(resolve,[$cnf( $equal(rel_str_of(X_338,inclusion_order(X_338)),incl_POSet(X_338)) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
( incl_POSet(X_337) != incl_POSet(X_338)
| the_carrier(incl_POSet(X_337)) = X_338 ),
inference(resolve,[$cnf( $equal(incl_POSet(X_337),rel_str_of(X_338,inclusion_order(X_338))) )],[refute_0_30,refute_0_24]) ).
cnf(refute_0_32,plain,
( incl_POSet(X_338) != incl_POSet(X_338)
| the_carrier(incl_POSet(X_338)) = X_338 ),
inference(subst,[],[refute_0_31:[bind(X_337,$fot(X_338))]]) ).
cnf(refute_0_33,plain,
incl_POSet(X_338) = incl_POSet(X_338),
introduced(tautology,[refl,[$fot(incl_POSet(X_338))]]) ).
cnf(refute_0_34,plain,
the_carrier(incl_POSet(X_338)) = X_338,
inference(resolve,[$cnf( $equal(incl_POSet(X_338),incl_POSet(X_338)) )],[refute_0_33,refute_0_32]) ).
cnf(refute_0_35,plain,
the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) = skolemFOFtoCNF_A_7,
inference(subst,[],[refute_0_34:[bind(X_338,$fot(skolemFOFtoCNF_A_7))]]) ).
cnf(refute_0_36,plain,
( skolemFOFtoCNF_A_7 != skolemFOFtoCNF_A_7
| the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) != skolemFOFtoCNF_A_7
| the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) = skolemFOFtoCNF_A_7 ),
introduced(tautology,[equality,[$cnf( $equal(the_carrier(incl_POSet(skolemFOFtoCNF_A_7)),skolemFOFtoCNF_A_7) ),[0,0,0],$fot(skolemFOFtoCNF_A_7)]]) ).
cnf(refute_0_37,plain,
( skolemFOFtoCNF_A_7 != skolemFOFtoCNF_A_7
| the_carrier(incl_POSet(skolemFOFtoCNF_A_7)) = skolemFOFtoCNF_A_7 ),
inference(resolve,[$cnf( $equal(the_carrier(incl_POSet(skolemFOFtoCNF_A_7)),skolemFOFtoCNF_A_7) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
skolemFOFtoCNF_A_7 != skolemFOFtoCNF_A_7,
inference(resolve,[$cnf( $equal(the_carrier(incl_POSet(skolemFOFtoCNF_A_7)),skolemFOFtoCNF_A_7) )],[refute_0_37,refute_0_0]) ).
cnf(refute_0_39,plain,
skolemFOFtoCNF_A_7 = skolemFOFtoCNF_A_7,
introduced(tautology,[refl,[$fot(skolemFOFtoCNF_A_7)]]) ).
cnf(refute_0_40,plain,
$false,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_A_7,skolemFOFtoCNF_A_7) )],[refute_0_39,refute_0_38]) ).
fof(negate_1_0,plain,
~ ! [A] :
( the_carrier(incl_POSet(A)) = A
=> the_InternalRel(incl_POSet(A)) = inclusion_order(A) ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
( ! [A] : rel_str(incl_POSet(A))
& ! [A] : strict_rel_str(incl_POSet(A)) ),
inference(canonicalize,[],[dt_k2_yellow_1]) ).
fof(normalize_1_1,plain,
! [A] : rel_str(incl_POSet(A)),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
! [A] : rel_str(incl_POSet(A)),
inference(specialize,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
! [A] :
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(canonicalize,[],[dt_u1_orders_2]) ).
fof(normalize_1_4,plain,
! [A] :
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(specialize,[],[normalize_1_3]) ).
fof(normalize_1_5,plain,
? [A] :
( the_InternalRel(incl_POSet(A)) != inclusion_order(A)
& the_carrier(incl_POSet(A)) = A ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_6,plain,
( the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) != inclusion_order(skolemFOFtoCNF_A_8)
& the_carrier(incl_POSet(skolemFOFtoCNF_A_8)) = skolemFOFtoCNF_A_8 ),
inference(skolemize,[],[normalize_1_5]) ).
fof(normalize_1_7,plain,
the_carrier(incl_POSet(skolemFOFtoCNF_A_8)) = skolemFOFtoCNF_A_8,
inference(conjunct,[],[normalize_1_6]) ).
fof(normalize_1_8,plain,
! [A,B,C] :
( ~ relation_of2(C,A,B)
<=> ~ relation_of2_as_subset(C,A,B) ),
inference(canonicalize,[],[redefinition_m2_relset_1]) ).
fof(normalize_1_9,plain,
! [A,B,C] :
( ~ relation_of2(C,A,B)
<=> ~ relation_of2_as_subset(C,A,B) ),
inference(specialize,[],[normalize_1_8]) ).
fof(normalize_1_10,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ) ),
inference(clausify,[],[normalize_1_9]) ).
fof(normalize_1_11,plain,
! [A,B,C] :
( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ),
inference(conjunct,[],[normalize_1_10]) ).
fof(normalize_1_12,plain,
! [A,B] :
( ~ relation_of2(B,A,A)
| ! [C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ( A = C
& B = D ) ) ),
inference(canonicalize,[],[free_g1_orders_2]) ).
fof(normalize_1_13,plain,
! [A,B] :
( ~ relation_of2(B,A,A)
| ! [C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ( A = C
& B = D ) ) ),
inference(specialize,[],[normalize_1_12]) ).
fof(normalize_1_14,plain,
! [A,B,C,D] :
( ( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C )
& ( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| B = D ) ),
inference(clausify,[],[normalize_1_13]) ).
fof(normalize_1_15,plain,
! [A,B,C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| B = D ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_16,plain,
! [A] : strict_rel_str(incl_POSet(A)),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_17,plain,
! [A] : strict_rel_str(incl_POSet(A)),
inference(specialize,[],[normalize_1_16]) ).
fof(normalize_1_18,plain,
! [A] :
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(canonicalize,[],[abstractness_v1_orders_2]) ).
fof(normalize_1_19,plain,
! [A] :
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(specialize,[],[normalize_1_18]) ).
fof(normalize_1_20,plain,
( ! [A] : antisymmetric(inclusion_order(A))
& ! [A] : reflexive(inclusion_order(A))
& ! [A] : relation_of2_as_subset(inclusion_order(A),A,A)
& ! [A] : transitive(inclusion_order(A))
& ! [A] : v1_partfun1(inclusion_order(A),A,A) ),
inference(canonicalize,[],[dt_k1_yellow_1]) ).
fof(normalize_1_21,plain,
! [A] : relation_of2_as_subset(inclusion_order(A),A,A),
inference(conjunct,[],[normalize_1_20]) ).
fof(normalize_1_22,plain,
! [A] : relation_of2_as_subset(inclusion_order(A),A,A),
inference(specialize,[],[normalize_1_21]) ).
fof(normalize_1_23,plain,
! [A,B,C,D] :
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_24,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(canonicalize,[],[d1_yellow_1]) ).
fof(normalize_1_25,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(specialize,[],[normalize_1_24]) ).
fof(normalize_1_26,plain,
the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) != inclusion_order(skolemFOFtoCNF_A_8),
inference(conjunct,[],[normalize_1_6]) ).
cnf(refute_1_0,plain,
rel_str(incl_POSet(A)),
inference(canonicalize,[],[normalize_1_2]) ).
cnf(refute_1_1,plain,
( ~ rel_str(A)
| relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
inference(canonicalize,[],[normalize_1_4]) ).
cnf(refute_1_2,plain,
( ~ rel_str(incl_POSet(A))
| relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))) ),
inference(subst,[],[refute_1_1:[bind(A,$fot(incl_POSet(A)))]]) ).
cnf(refute_1_3,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(A)),the_carrier(incl_POSet(A)),the_carrier(incl_POSet(A))),
inference(resolve,[$cnf( rel_str(incl_POSet(A)) )],[refute_1_0,refute_1_2]) ).
cnf(refute_1_4,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8))),
inference(subst,[],[refute_1_3:[bind(A,$fot(skolemFOFtoCNF_A_8))]]) ).
cnf(refute_1_5,plain,
the_carrier(incl_POSet(skolemFOFtoCNF_A_8)) = skolemFOFtoCNF_A_8,
inference(canonicalize,[],[normalize_1_7]) ).
cnf(refute_1_6,plain,
( the_carrier(incl_POSet(skolemFOFtoCNF_A_8)) != skolemFOFtoCNF_A_8
| ~ relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)))
| relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) ),
introduced(tautology,[equality,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) ),[1],$fot(skolemFOFtoCNF_A_8)]]) ).
cnf(refute_1_7,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)))
| relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) ),
inference(resolve,[$cnf( $equal(the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8) )],[refute_1_5,refute_1_6]) ).
cnf(refute_1_8,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8))),
inference(resolve,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) )],[refute_1_4,refute_1_7]) ).
cnf(refute_1_9,plain,
( the_carrier(incl_POSet(skolemFOFtoCNF_A_8)) != skolemFOFtoCNF_A_8
| ~ relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8)))
| relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8) ),
introduced(tautology,[equality,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) ),[2],$fot(skolemFOFtoCNF_A_8)]]) ).
cnf(refute_1_10,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8)))
| relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8) ),
inference(resolve,[$cnf( $equal(the_carrier(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8) )],[refute_1_5,refute_1_9]) ).
cnf(refute_1_11,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8),
inference(resolve,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,the_carrier(incl_POSet(skolemFOFtoCNF_A_8))) )],[refute_1_8,refute_1_10]) ).
cnf(refute_1_12,plain,
( ~ relation_of2_as_subset(C,A,B)
| relation_of2(C,A,B) ),
inference(canonicalize,[],[normalize_1_11]) ).
cnf(refute_1_13,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8)
| relation_of2(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8) ),
inference(subst,[],[refute_1_12:[bind(A,$fot(skolemFOFtoCNF_A_8)),bind(B,$fot(skolemFOFtoCNF_A_8)),bind(C,$fot(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))))]]) ).
cnf(refute_1_14,plain,
relation_of2(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8),
inference(resolve,[$cnf( relation_of2_as_subset(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8) )],[refute_1_11,refute_1_13]) ).
cnf(refute_1_15,plain,
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| B = D ),
inference(canonicalize,[],[normalize_1_15]) ).
cnf(refute_1_16,plain,
( rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) != rel_str_of(X_740,X_741)
| ~ relation_of2(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8)
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = X_741 ),
inference(subst,[],[refute_1_15:[bind(A,$fot(skolemFOFtoCNF_A_8)),bind(B,$fot(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)))),bind(C,$fot(X_740)),bind(D,$fot(X_741))]]) ).
cnf(refute_1_17,plain,
( rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) != rel_str_of(X_740,X_741)
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = X_741 ),
inference(resolve,[$cnf( relation_of2(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),skolemFOFtoCNF_A_8,skolemFOFtoCNF_A_8) )],[refute_1_14,refute_1_16]) ).
cnf(refute_1_18,plain,
strict_rel_str(incl_POSet(A)),
inference(canonicalize,[],[normalize_1_17]) ).
cnf(refute_1_19,plain,
( ~ rel_str(A)
| ~ strict_rel_str(A)
| A = rel_str_of(the_carrier(A),the_InternalRel(A)) ),
inference(canonicalize,[],[normalize_1_19]) ).
cnf(refute_1_20,plain,
( ~ rel_str(incl_POSet(A))
| ~ strict_rel_str(incl_POSet(A))
| incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
inference(subst,[],[refute_1_19:[bind(A,$fot(incl_POSet(A)))]]) ).
cnf(refute_1_21,plain,
( ~ rel_str(incl_POSet(A))
| incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
inference(resolve,[$cnf( strict_rel_str(incl_POSet(A)) )],[refute_1_18,refute_1_20]) ).
cnf(refute_1_22,plain,
incl_POSet(A) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),
inference(resolve,[$cnf( rel_str(incl_POSet(A)) )],[refute_1_0,refute_1_21]) ).
cnf(refute_1_23,plain,
relation_of2_as_subset(inclusion_order(A),A,A),
inference(canonicalize,[],[normalize_1_22]) ).
cnf(refute_1_24,plain,
relation_of2_as_subset(inclusion_order(X_418),X_418,X_418),
inference(subst,[],[refute_1_23:[bind(A,$fot(X_418))]]) ).
cnf(refute_1_25,plain,
( ~ relation_of2_as_subset(inclusion_order(X_418),X_418,X_418)
| relation_of2(inclusion_order(X_418),X_418,X_418) ),
inference(subst,[],[refute_1_12:[bind(A,$fot(X_418)),bind(B,$fot(X_418)),bind(C,$fot(inclusion_order(X_418)))]]) ).
cnf(refute_1_26,plain,
relation_of2(inclusion_order(X_418),X_418,X_418),
inference(resolve,[$cnf( relation_of2_as_subset(inclusion_order(X_418),X_418,X_418) )],[refute_1_24,refute_1_25]) ).
cnf(refute_1_27,plain,
relation_of2(inclusion_order(X_635),X_635,X_635),
inference(subst,[],[refute_1_26:[bind(X_418,$fot(X_635))]]) ).
cnf(refute_1_28,plain,
( rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A)
| A = C ),
inference(canonicalize,[],[normalize_1_23]) ).
cnf(refute_1_29,plain,
( rel_str_of(X_635,inclusion_order(X_635)) != rel_str_of(X_637,X_638)
| ~ relation_of2(inclusion_order(X_635),X_635,X_635)
| X_635 = X_637 ),
inference(subst,[],[refute_1_28:[bind(A,$fot(X_635)),bind(B,$fot(inclusion_order(X_635))),bind(C,$fot(X_637)),bind(D,$fot(X_638))]]) ).
cnf(refute_1_30,plain,
( rel_str_of(X_635,inclusion_order(X_635)) != rel_str_of(X_637,X_638)
| X_635 = X_637 ),
inference(resolve,[$cnf( relation_of2(inclusion_order(X_635),X_635,X_635) )],[refute_1_27,refute_1_29]) ).
cnf(refute_1_31,plain,
incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(canonicalize,[],[normalize_1_25]) ).
cnf(refute_1_32,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_1_33,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_1_34,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_1_32,refute_1_33]) ).
cnf(refute_1_35,plain,
( incl_POSet(A) != rel_str_of(A,inclusion_order(A))
| rel_str_of(A,inclusion_order(A)) = incl_POSet(A) ),
inference(subst,[],[refute_1_34:[bind(X,$fot(incl_POSet(A))),bind(Y,$fot(rel_str_of(A,inclusion_order(A))))]]) ).
cnf(refute_1_36,plain,
rel_str_of(A,inclusion_order(A)) = incl_POSet(A),
inference(resolve,[$cnf( $equal(incl_POSet(A),rel_str_of(A,inclusion_order(A))) )],[refute_1_31,refute_1_35]) ).
cnf(refute_1_37,plain,
rel_str_of(X_635,inclusion_order(X_635)) = incl_POSet(X_635),
inference(subst,[],[refute_1_36:[bind(A,$fot(X_635))]]) ).
cnf(refute_1_38,plain,
( incl_POSet(X_635) != rel_str_of(X_637,X_638)
| rel_str_of(X_635,inclusion_order(X_635)) != incl_POSet(X_635)
| rel_str_of(X_635,inclusion_order(X_635)) = rel_str_of(X_637,X_638) ),
introduced(tautology,[equality,[$cnf( $equal(rel_str_of(X_635,inclusion_order(X_635)),incl_POSet(X_635)) ),[1],$fot(rel_str_of(X_637,X_638))]]) ).
cnf(refute_1_39,plain,
( incl_POSet(X_635) != rel_str_of(X_637,X_638)
| rel_str_of(X_635,inclusion_order(X_635)) = rel_str_of(X_637,X_638) ),
inference(resolve,[$cnf( $equal(rel_str_of(X_635,inclusion_order(X_635)),incl_POSet(X_635)) )],[refute_1_37,refute_1_38]) ).
cnf(refute_1_40,plain,
( incl_POSet(X_635) != rel_str_of(X_637,X_638)
| X_635 = X_637 ),
inference(resolve,[$cnf( $equal(rel_str_of(X_635,inclusion_order(X_635)),rel_str_of(X_637,X_638)) )],[refute_1_39,refute_1_30]) ).
cnf(refute_1_41,plain,
( incl_POSet(X_687) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| X_687 = the_carrier(incl_POSet(A)) ),
inference(subst,[],[refute_1_40:[bind(X_635,$fot(X_687)),bind(X_637,$fot(the_carrier(incl_POSet(A)))),bind(X_638,$fot(the_InternalRel(incl_POSet(A))))]]) ).
cnf(refute_1_42,plain,
( incl_POSet(A) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = incl_POSet(A) ),
inference(subst,[],[refute_1_34:[bind(X,$fot(incl_POSet(A))),bind(Y,$fot(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))))]]) ).
cnf(refute_1_43,plain,
rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = incl_POSet(A),
inference(resolve,[$cnf( $equal(incl_POSet(A),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) )],[refute_1_22,refute_1_42]) ).
cnf(refute_1_44,plain,
( incl_POSet(X_687) != incl_POSet(A)
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != incl_POSet(A)
| incl_POSet(X_687) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(incl_POSet(X_687),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) ),[1],$fot(incl_POSet(A))]]) ).
cnf(refute_1_45,plain,
( incl_POSet(X_687) != incl_POSet(A)
| incl_POSet(X_687) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) ),
inference(resolve,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),incl_POSet(A)) )],[refute_1_43,refute_1_44]) ).
cnf(refute_1_46,plain,
( incl_POSet(X_687) != incl_POSet(A)
| X_687 = the_carrier(incl_POSet(A)) ),
inference(resolve,[$cnf( $equal(incl_POSet(X_687),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) )],[refute_1_45,refute_1_41]) ).
cnf(refute_1_47,plain,
( incl_POSet(A) != incl_POSet(A)
| A = the_carrier(incl_POSet(A)) ),
inference(subst,[],[refute_1_46:[bind(X_687,$fot(A))]]) ).
cnf(refute_1_48,plain,
incl_POSet(A) = incl_POSet(A),
introduced(tautology,[refl,[$fot(incl_POSet(A))]]) ).
cnf(refute_1_49,plain,
A = the_carrier(incl_POSet(A)),
inference(resolve,[$cnf( $equal(incl_POSet(A),incl_POSet(A)) )],[refute_1_48,refute_1_47]) ).
cnf(refute_1_50,plain,
( A != the_carrier(incl_POSet(A))
| the_carrier(incl_POSet(A)) = A ),
inference(subst,[],[refute_1_34:[bind(X,$fot(A)),bind(Y,$fot(the_carrier(incl_POSet(A))))]]) ).
cnf(refute_1_51,plain,
the_carrier(incl_POSet(A)) = A,
inference(resolve,[$cnf( $equal(A,the_carrier(incl_POSet(A))) )],[refute_1_49,refute_1_50]) ).
cnf(refute_1_52,plain,
rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),
introduced(tautology,[refl,[$fot(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))))]]) ).
cnf(refute_1_53,plain,
( rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| the_carrier(incl_POSet(A)) != A
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(A,the_InternalRel(incl_POSet(A))) ),
introduced(tautology,[equality,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) ),[1,0],$fot(A)]]) ).
cnf(refute_1_54,plain,
( the_carrier(incl_POSet(A)) != A
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(A,the_InternalRel(incl_POSet(A))) ),
inference(resolve,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) )],[refute_1_52,refute_1_53]) ).
cnf(refute_1_55,plain,
rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) = rel_str_of(A,the_InternalRel(incl_POSet(A))),
inference(resolve,[$cnf( $equal(the_carrier(incl_POSet(A)),A) )],[refute_1_51,refute_1_54]) ).
cnf(refute_1_56,plain,
( incl_POSet(A) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))) != rel_str_of(A,the_InternalRel(incl_POSet(A)))
| incl_POSet(A) = rel_str_of(A,the_InternalRel(incl_POSet(A))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(incl_POSet(A),rel_str_of(A,the_InternalRel(incl_POSet(A)))) ),[0],$fot(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))))]]) ).
cnf(refute_1_57,plain,
( incl_POSet(A) != rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))
| incl_POSet(A) = rel_str_of(A,the_InternalRel(incl_POSet(A))) ),
inference(resolve,[$cnf( $equal(rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A))),rel_str_of(A,the_InternalRel(incl_POSet(A)))) )],[refute_1_55,refute_1_56]) ).
cnf(refute_1_58,plain,
incl_POSet(A) = rel_str_of(A,the_InternalRel(incl_POSet(A))),
inference(resolve,[$cnf( $equal(incl_POSet(A),rel_str_of(the_carrier(incl_POSet(A)),the_InternalRel(incl_POSet(A)))) )],[refute_1_22,refute_1_57]) ).
cnf(refute_1_59,plain,
( incl_POSet(A) != rel_str_of(A,the_InternalRel(incl_POSet(A)))
| rel_str_of(A,the_InternalRel(incl_POSet(A))) = incl_POSet(A) ),
inference(subst,[],[refute_1_34:[bind(X,$fot(incl_POSet(A))),bind(Y,$fot(rel_str_of(A,the_InternalRel(incl_POSet(A)))))]]) ).
cnf(refute_1_60,plain,
rel_str_of(A,the_InternalRel(incl_POSet(A))) = incl_POSet(A),
inference(resolve,[$cnf( $equal(incl_POSet(A),rel_str_of(A,the_InternalRel(incl_POSet(A)))) )],[refute_1_58,refute_1_59]) ).
cnf(refute_1_61,plain,
rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) = incl_POSet(skolemFOFtoCNF_A_8),
inference(subst,[],[refute_1_60:[bind(A,$fot(skolemFOFtoCNF_A_8))]]) ).
cnf(refute_1_62,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != rel_str_of(X_740,X_741)
| rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) != incl_POSet(skolemFOFtoCNF_A_8)
| rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) = rel_str_of(X_740,X_741) ),
introduced(tautology,[equality,[$cnf( $equal(rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))),incl_POSet(skolemFOFtoCNF_A_8)) ),[1],$fot(rel_str_of(X_740,X_741))]]) ).
cnf(refute_1_63,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != rel_str_of(X_740,X_741)
| rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))) = rel_str_of(X_740,X_741) ),
inference(resolve,[$cnf( $equal(rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))),incl_POSet(skolemFOFtoCNF_A_8)) )],[refute_1_61,refute_1_62]) ).
cnf(refute_1_64,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != rel_str_of(X_740,X_741)
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = X_741 ),
inference(resolve,[$cnf( $equal(rel_str_of(skolemFOFtoCNF_A_8,the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8))),rel_str_of(X_740,X_741)) )],[refute_1_63,refute_1_17]) ).
cnf(refute_1_65,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != rel_str_of(X_752,inclusion_order(X_752))
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = inclusion_order(X_752) ),
inference(subst,[],[refute_1_64:[bind(X_740,$fot(X_752)),bind(X_741,$fot(inclusion_order(X_752)))]]) ).
cnf(refute_1_66,plain,
incl_POSet(X_752) = rel_str_of(X_752,inclusion_order(X_752)),
inference(subst,[],[refute_1_31:[bind(A,$fot(X_752))]]) ).
cnf(refute_1_67,plain,
( incl_POSet(X_752) != rel_str_of(X_752,inclusion_order(X_752))
| rel_str_of(X_752,inclusion_order(X_752)) = incl_POSet(X_752) ),
inference(subst,[],[refute_1_34:[bind(X,$fot(incl_POSet(X_752))),bind(Y,$fot(rel_str_of(X_752,inclusion_order(X_752))))]]) ).
cnf(refute_1_68,plain,
rel_str_of(X_752,inclusion_order(X_752)) = incl_POSet(X_752),
inference(resolve,[$cnf( $equal(incl_POSet(X_752),rel_str_of(X_752,inclusion_order(X_752))) )],[refute_1_66,refute_1_67]) ).
cnf(refute_1_69,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != incl_POSet(X_752)
| rel_str_of(X_752,inclusion_order(X_752)) != incl_POSet(X_752)
| incl_POSet(skolemFOFtoCNF_A_8) = rel_str_of(X_752,inclusion_order(X_752)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(incl_POSet(skolemFOFtoCNF_A_8),rel_str_of(X_752,inclusion_order(X_752))) ),[1],$fot(incl_POSet(X_752))]]) ).
cnf(refute_1_70,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != incl_POSet(X_752)
| incl_POSet(skolemFOFtoCNF_A_8) = rel_str_of(X_752,inclusion_order(X_752)) ),
inference(resolve,[$cnf( $equal(rel_str_of(X_752,inclusion_order(X_752)),incl_POSet(X_752)) )],[refute_1_68,refute_1_69]) ).
cnf(refute_1_71,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != incl_POSet(X_752)
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = inclusion_order(X_752) ),
inference(resolve,[$cnf( $equal(incl_POSet(skolemFOFtoCNF_A_8),rel_str_of(X_752,inclusion_order(X_752))) )],[refute_1_70,refute_1_65]) ).
cnf(refute_1_72,plain,
( incl_POSet(skolemFOFtoCNF_A_8) != incl_POSet(skolemFOFtoCNF_A_8)
| the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = inclusion_order(skolemFOFtoCNF_A_8) ),
inference(subst,[],[refute_1_71:[bind(X_752,$fot(skolemFOFtoCNF_A_8))]]) ).
cnf(refute_1_73,plain,
incl_POSet(skolemFOFtoCNF_A_8) = incl_POSet(skolemFOFtoCNF_A_8),
introduced(tautology,[refl,[$fot(incl_POSet(skolemFOFtoCNF_A_8))]]) ).
cnf(refute_1_74,plain,
the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) = inclusion_order(skolemFOFtoCNF_A_8),
inference(resolve,[$cnf( $equal(incl_POSet(skolemFOFtoCNF_A_8),incl_POSet(skolemFOFtoCNF_A_8)) )],[refute_1_73,refute_1_72]) ).
cnf(refute_1_75,plain,
the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)) != inclusion_order(skolemFOFtoCNF_A_8),
inference(canonicalize,[],[normalize_1_26]) ).
cnf(refute_1_76,plain,
$false,
inference(resolve,[$cnf( $equal(the_InternalRel(incl_POSet(skolemFOFtoCNF_A_8)),inclusion_order(skolemFOFtoCNF_A_8)) )],[refute_1_74,refute_1_75]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU368+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n023.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 : Sun Jun 19 20:10:33 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 51.94/52.18 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.94/52.18
% 51.94/52.18 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 52.04/52.18
%------------------------------------------------------------------------------