%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET862-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:44:52 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.40s
% Output : Refutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 30
% Syntax : Number of formulae : 144 ( 28 unt; 15 def)
% Number of atoms : 412 ( 11 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 454 ( 186 ~; 253 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 16 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 166 ( 0 sgn 166 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| ~ c_lessequals(X1,X0,tc_set(X2))
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
fof(f2,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| ~ c_lessequals(X1,X0,tc_set(X2))
| X0 = X1 ),
inference(reorient_equations,[],[f1]) ).
fof(f3,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,X2)
| ~ c_lessequals(X1,X3,tc_set(X2))
| c_in(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetD_0) ).
fof(f4,axiom,
! [X2,X0,X1] :
( c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_1) ).
fof(f6,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_in(c_Zorn_Ochain__extend__1(X3,X0,X2),X3,tc_set(X2))
| c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zorn_Ochain__extend_0) ).
fof(f7,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X0,X2),X0,tc_set(X2))
| c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zorn_Ochain__extend_1) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X0,X1,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| c_in(X0,X5,X2)
| c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zorn_Omaxchain__super__lemma_0) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X0,X1,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| c_in(X0,X5,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zorn_Omaxchain__super__lemma_1) ).
fof(f10,negated_conjecture,
c_in(v_c,c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f11,negated_conjecture,
c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f12,negated_conjecture,
c_in(v_y,v_S,tc_set(t_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f13,negated_conjecture,
! [X0] :
( c_lessequals(X0,v_y,tc_set(t_a))
| ~ c_in(X0,v_c,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f14,negated_conjecture,
! [X0] :
( c_in(v_x(X0),v_S,tc_set(t_a))
| ~ c_in(X0,v_S,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f15,negated_conjecture,
! [X0] :
( c_lessequals(X0,v_x(X0),tc_set(t_a))
| ~ c_in(X0,v_S,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f16,negated_conjecture,
! [X0] :
( X0 != v_x(X0)
| ~ c_in(X0,v_S,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f17,plain,
! [X0] :
( v_x(X0) != X0
| ~ c_in(X0,v_S,tc_set(t_a)) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,plain,
! [X2,X0,X1] :
( c_lessequals(X1,X0,tc_set(X2))
| c_lessequals(X0,X1,tc_set(X2))
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f19,plain,
! [X2,X3,X0,X1] :
( c_lessequals(X1,X3,tc_set(X2))
| c_in(X0,X1,X2)
| ~ c_in(X0,X3,X2) ),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f20,plain,
! [X2,X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(consistent_polarity_flipping,[],[f4]) ).
fof(f21,plain,
! [X2,X0,X1] :
( c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(consistent_polarity_flipping,[],[f5]) ).
fof(f22,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(c_Zorn_Ochain__extend__1(X3,X0,X2),X3,tc_set(X2))
| c_in(X0,X1,tc_set(X2)) ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f23,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_lessequals(c_Zorn_Ochain__extend__1(X3,X0,X2),X0,tc_set(X2))
| c_in(X0,X1,tc_set(X2)) ),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f24,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| c_in(X0,X1,X2)
| ~ c_in(X0,X5,X2)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2)) ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f25,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| c_in(X0,X1,X2)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(X0,X5,X2) ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f26,plain,
~ c_in(v_c,c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a))),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f27,plain,
~ c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f28,plain,
~ c_in(v_y,v_S,tc_set(t_a)),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f29,plain,
! [X0] :
( c_in(X0,v_c,tc_set(t_a))
| ~ c_lessequals(X0,v_y,tc_set(t_a)) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f30,plain,
! [X0] :
( ~ c_in(v_x(X0),v_S,tc_set(t_a))
| c_in(X0,v_S,tc_set(t_a)) ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f31,plain,
! [X0] :
( c_in(X0,v_S,tc_set(t_a))
| ~ c_lessequals(X0,v_x(X0),tc_set(t_a)) ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f32,plain,
! [X0] :
( c_in(X0,v_S,tc_set(t_a))
| v_x(X0) != X0 ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f33,plain,
v_y != v_x(v_y),
inference(resolution,[],[f32,f28]) ).
fof(f35,plain,
~ c_lessequals(v_y,v_x(v_y),tc_set(t_a)),
inference(resolution,[],[f31,f28]) ).
fof(f84,plain,
( c_lessequals(v_x(v_y),v_y,tc_set(t_a))
| v_y = v_x(v_y) ),
inference(resolution,[],[f18,f35]) ).
fof(f237,definition,
( spl0_29
<=> v_y = v_x(v_y) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f239,plain,
( v_y = v_x(v_y)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f241,definition,
( spl0_30
<=> c_lessequals(v_x(v_y),v_y,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f244,plain,
( spl0_29
| spl0_30 ),
inference(avatar_split_clause,[],[f84,f241,f237]) ).
fof(f245,plain,
( v_y != v_y
| ~ spl0_29 ),
inference(superposition,[],[f33,f239]) ).
fof(f263,plain,
( $false
| ~ spl0_29 ),
inference(trivial_inequality_removal,[],[f245]) ).
fof(f264,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f263]) ).
fof(f325,plain,
! [X0] :
( c_in(X0,v_y,t_a)
| ~ c_in(X0,v_x(v_y),t_a) ),
inference(resolution,[],[f19,f35]) ).
fof(f574,definition,
( spl0_40
<=> c_in(v_x(v_y),v_S,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f575,plain,
( c_in(v_x(v_y),v_S,tc_set(t_a))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( ~ c_in(v_x(v_y),v_S,tc_set(t_a))
| spl0_40 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f615,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(X0,c_Zorn_Omaxchain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,X4,X2)
| ~ c_in(X3,X5,X2)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(X0,X5,X2),X0,tc_set(X2))
| c_in(X0,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_lessequals(c_Zorn_Ochain__extend__1(X0,X4,X2),X4,tc_set(X2))
| c_in(X4,X1,tc_set(X2)) ),
inference(resolution,[],[f24,f23]) ).
fof(f616,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(X0,c_Zorn_Omaxchain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,X4,X2)
| ~ c_in(X3,X5,X2)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(X0,X5,X2),X0,tc_set(X2))
| c_in(X0,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(c_Zorn_Ochain__extend__1(X0,X4,X2),X0,tc_set(X2))
| c_in(X4,X1,tc_set(X2)) ),
inference(resolution,[],[f24,f22]) ).
fof(f718,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(X0,c_Zorn_Omaxchain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,X4,X2)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X0,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,X5,X2)
| c_in(X0,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_lessequals(c_Zorn_Ochain__extend__1(X0,X4,X2),X4,tc_set(X2))
| c_in(X4,X1,tc_set(X2)) ),
inference(resolution,[],[f25,f23]) ).
fof(f719,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(X0,c_Zorn_Omaxchain(X1,X2),tc_set(tc_set(X2)))
| c_in(X3,X4,X2)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X0,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,X5,X2)
| c_in(X0,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(c_Zorn_Ochain__extend__1(X0,X4,X2),X0,tc_set(X2))
| c_in(X4,X1,tc_set(X2)) ),
inference(resolution,[],[f25,f22]) ).
fof(f905,plain,
! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| ~ c_in(X0,X2,t_a)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| c_in(X1,v_S,tc_set(t_a)) ),
inference(resolution,[],[f615,f26]) ).
fof(f908,definition,
( spl0_53
<=> c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f910,plain,
( c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f912,definition,
( spl0_54
<=> ! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_in(X1,v_S,tc_set(t_a))
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f913,plain,
( ! [X2,X0,X1] :
( c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f912]) ).
fof(f914,plain,
( spl0_53
| spl0_54 ),
inference(avatar_split_clause,[],[f905,f912,f908]) ).
fof(f915,plain,
( $false
| ~ spl0_53 ),
inference(resolution,[],[f910,f27]) ).
fof(f916,plain,
~ spl0_53,
inference(avatar_contradiction_clause,[],[f915]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| ~ c_in(X0,X2,t_a)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| c_in(X1,v_S,tc_set(t_a)) ),
inference(resolution,[],[f616,f26]) ).
fof(f1039,definition,
( spl0_59
<=> ! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_in(X1,v_S,tc_set(t_a))
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f1040,plain,
( ! [X2,X0,X1] :
( c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X1,t_a)
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1041,plain,
( spl0_53
| spl0_59 ),
inference(avatar_split_clause,[],[f1036,f1039,f908]) ).
fof(f1098,plain,
! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| c_in(X1,v_S,tc_set(t_a)) ),
inference(resolution,[],[f718,f26]) ).
fof(f1101,definition,
( spl0_62
<=> ! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_in(X1,v_S,tc_set(t_a))
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f1102,plain,
( ! [X2,X0,X1] :
( c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a)) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1103,plain,
( spl0_53
| spl0_62 ),
inference(avatar_split_clause,[],[f1098,f1101,f908]) ).
fof(f1280,plain,
! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| c_in(X1,v_S,tc_set(t_a)) ),
inference(resolution,[],[f719,f26]) ).
fof(f1283,definition,
( spl0_69
<=> ! [X2,X0,X1] :
( c_in(X0,X1,t_a)
| c_in(X1,v_S,tc_set(t_a))
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f1284,plain,
( ! [X2,X0,X1] :
( c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X1,t_a)
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X2,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X2,t_a),X2,tc_set(t_a)) )
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f1283]) ).
fof(f1285,plain,
( spl0_53
| spl0_69 ),
inference(avatar_split_clause,[],[f1280,f1283,f908]) ).
fof(f1376,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X1,t_a) )
| spl0_40
| ~ spl0_54 ),
inference(resolution,[],[f913,f576]) ).
fof(f1406,definition,
( spl0_82
<=> c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f1410,definition,
( spl0_83
<=> ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| ~ c_in(X0,X1,t_a)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),v_c,tc_set(t_a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f1411,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| ~ c_in(X0,X1,t_a)
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),v_c,tc_set(t_a)) )
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f1410]) ).
fof(f1421,plain,
( c_in(v_y,v_S,tc_set(t_a))
| ~ spl0_40 ),
inference(resolution,[],[f575,f30]) ).
fof(f1422,plain,
( $false
| ~ spl0_40 ),
inference(resolution,[],[f1421,f28]) ).
fof(f1423,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f1422]) ).
fof(f1424,plain,
( spl0_82
| spl0_83
| spl0_40
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1376,f912,f574,f1410,f1406]) ).
fof(f1538,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_c,tc_set(t_a))
| ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X1,t_a) )
| spl0_40
| ~ spl0_59 ),
inference(resolution,[],[f1040,f576]) ).
fof(f1559,definition,
( spl0_89
<=> c_in(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_c,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f1561,plain,
( ~ c_in(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_c,tc_set(t_a))
| spl0_89 ),
inference(avatar_component_clause,[],[f1559]) ).
fof(f1562,plain,
( ~ spl0_89
| spl0_83
| spl0_40
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f1538,f1039,f574,f1410,f1559]) ).
fof(f1583,plain,
( ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_y,tc_set(t_a))
| spl0_89 ),
inference(resolution,[],[f1561,f29]) ).
fof(f1598,definition,
( spl0_95
<=> c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_y,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f1599,plain,
( ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_y,tc_set(t_a))
| spl0_95 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1607,plain,
( ! [X0] :
( c_in(X0,c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),t_a)
| ~ c_in(X0,v_y,t_a) )
| spl0_95 ),
inference(resolution,[],[f1599,f19]) ).
fof(f1624,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a))
| ~ c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),X1,tc_set(t_a)) )
| spl0_40
| ~ spl0_62 ),
inference(resolution,[],[f1102,f576]) ).
fof(f1663,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| ~ c_in(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_c,tc_set(t_a))
| ~ c_in(X0,X1,t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),X1,tc_set(t_a)) )
| spl0_40
| ~ spl0_69 ),
inference(resolution,[],[f1284,f576]) ).
fof(f1670,definition,
( spl0_102
<=> ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(X0,X1,t_a) ) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f1671,plain,
( ! [X0,X1] :
( c_in(X0,v_x(v_y),t_a)
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),X1,tc_set(t_a))
| ~ c_in(X0,X1,t_a) )
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f1670]) ).
fof(f1672,plain,
( ~ spl0_89
| spl0_102
| spl0_40
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1663,f1283,f574,f1670,f1559]) ).
fof(f1709,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),X0,t_a),v_y,t_a)
| ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),X0,tc_set(t_a)) )
| spl0_95 ),
inference(resolution,[],[f1607,f20]) ).
fof(f1726,plain,
( spl0_82
| spl0_102
| spl0_40
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1624,f1101,f574,f1670,f1406]) ).
fof(f1760,plain,
( ! [X0,X1] :
( c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,X0,t_a),X0,tc_set(t_a))
| ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X1,t_a),X0,t_a)
| ~ c_lessequals(v_x(v_y),X1,tc_set(t_a)) )
| ~ spl0_102 ),
inference(resolution,[],[f1671,f20]) ).
fof(f1854,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),X0,t_a),v_x(v_y),t_a)
| ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),X0,tc_set(t_a)) )
| spl0_95 ),
inference(resolution,[],[f1709,f325]) ).
fof(f1926,definition,
( spl0_109
<=> c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,v_y,t_a),v_c,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f1927,plain,
( c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,v_y,t_a),v_c,tc_set(t_a))
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f1926]) ).
fof(f1928,plain,
( ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,v_y,t_a),v_c,tc_set(t_a))
| spl0_109 ),
inference(avatar_component_clause,[],[f1926]) ).
fof(f1935,definition,
( spl0_111
<=> ! [X0] :
( ~ c_lessequals(v_x(v_y),X0,tc_set(t_a))
| ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X0,t_a),v_y,t_a) ) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f1936,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X0,t_a),v_y,t_a)
| ~ c_lessequals(v_x(v_y),X0,tc_set(t_a)) )
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f1935]) ).
fof(f1965,plain,
( ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(v_c,v_y,t_a),v_y,tc_set(t_a))
| spl0_109 ),
inference(resolution,[],[f1928,f29]) ).
fof(f2100,plain,
( ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a))
| ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a))
| spl0_95 ),
inference(resolution,[],[f1854,f21]) ).
fof(f2109,plain,
( ~ c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x(v_y),t_a),v_x(v_y),tc_set(t_a))
| spl0_95 ),
inference(duplicate_literal_removal,[],[f2100]) ).
fof(f2110,plain,
( ~ spl0_82
| spl0_95 ),
inference(avatar_split_clause,[],[f2109,f1598,f1406]) ).
fof(f2111,plain,
( ~ spl0_95
| spl0_89 ),
inference(avatar_split_clause,[],[f1583,f1559,f1598]) ).
fof(f2112,plain,
( ~ c_lessequals(v_x(v_y),v_y,tc_set(t_a))
| ~ c_lessequals(v_x(v_y),v_y,tc_set(t_a))
| ~ spl0_111 ),
inference(resolution,[],[f1936,f21]) ).
fof(f2124,plain,
( ~ c_lessequals(v_x(v_y),v_y,tc_set(t_a))
| ~ spl0_111 ),
inference(duplicate_literal_removal,[],[f2112]) ).
fof(f2126,plain,
( ~ spl0_30
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f2124,f1935,f241]) ).
fof(f2137,plain,
( ! [X0,X1] :
( ~ c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,X1,t_a),v_c,tc_set(t_a))
| ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X0,t_a),X1,t_a)
| ~ c_lessequals(v_x(v_y),X0,tc_set(t_a)) )
| ~ spl0_83 ),
inference(resolution,[],[f1411,f20]) ).
fof(f2165,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X0,t_a),v_y,t_a)
| ~ c_lessequals(v_x(v_y),X0,tc_set(t_a)) )
| ~ spl0_102
| spl0_109 ),
inference(resolution,[],[f1760,f1965]) ).
fof(f2167,plain,
( spl0_111
| ~ spl0_102
| spl0_109 ),
inference(avatar_split_clause,[],[f2165,f1926,f1670,f1935]) ).
fof(f2368,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(v_x(v_y),X0,t_a),v_y,t_a)
| ~ c_lessequals(v_x(v_y),X0,tc_set(t_a)) )
| ~ spl0_83
| ~ spl0_109 ),
inference(resolution,[],[f2137,f1927]) ).
fof(f2439,plain,
( spl0_111
| ~ spl0_83
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f2368,f1926,f1410,f1935]) ).
cnf(s15,plain,
( spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f244]) ).
cnf(s16,plain,
~ spl0_29,
inference(sat_conversion,[],[f264]) ).
cnf(s44,plain,
( spl0_53
| spl0_54 ),
inference(sat_conversion,[],[f914]) ).
cnf(s45,plain,
~ spl0_53,
inference(sat_conversion,[],[f916]) ).
cnf(s51,plain,
( spl0_53
| spl0_59 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s55,plain,
( spl0_53
| spl0_62 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s61,plain,
( spl0_53
| spl0_69 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s72,plain,
~ spl0_40,
inference(sat_conversion,[],[f1423]) ).
cnf(s73,plain,
( spl0_40
| ~ spl0_54
| spl0_82
| spl0_83 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s81,plain,
( spl0_40
| ~ spl0_59
| spl0_83
| ~ spl0_89 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s94,plain,
( spl0_40
| ~ spl0_69
| ~ spl0_89
| spl0_102 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s101,plain,
( spl0_40
| ~ spl0_62
| spl0_82
| spl0_102 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s121,plain,
( ~ spl0_82
| spl0_95 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s122,plain,
( spl0_89
| ~ spl0_95 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s125,plain,
( ~ spl0_30
| ~ spl0_111 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s127,plain,
( ~ spl0_102
| spl0_109
| spl0_111 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s155,plain,
( ~ spl0_83
| ~ spl0_109
| spl0_111 ),
inference(sat_conversion,[],[f2439]) ).
cnf(s164,plain,
spl0_69,
inference(rat,[],[s61,s45]) ).
cnf(s165,plain,
spl0_62,
inference(rat,[],[s55,s45]) ).
cnf(s166,plain,
spl0_59,
inference(rat,[],[s51,s45]) ).
cnf(s167,plain,
spl0_54,
inference(rat,[],[s44,s45]) ).
cnf(s170,plain,
spl0_30,
inference(rat,[],[s15,s16]) ).
cnf(s171,plain,
~ spl0_111,
inference(rat,[],[s125,s170]) ).
cnf(s216,plain,
spl0_102,
inference(rat,[],[s121,s122,s101,s94,s72,s165,s164]) ).
cnf(s218,plain,
spl0_109,
inference(rat,[],[s127,s171,s216]) ).
cnf(s219,plain,
~ spl0_83,
inference(rat,[],[s155,s171,s218]) ).
cnf(s221,plain,
~ spl0_89,
inference(rat,[],[s81,s166,s72,s219]) ).
cnf(s222,plain,
spl0_82,
inference(rat,[],[s73,s167,s72,s219]) ).
cnf(s225,plain,
~ spl0_95,
inference(rat,[],[s122,s221]) ).
cnf(s227,plain,
$false,
inference(rat,[],[s121,s225,s222]) ).
fof(f2440,plain,
$false,
inference(avatar_sat_refutation,[],[s227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET862-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Mon Sep 28 03:03:34 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.33 Running first-order model finding
% 0.08/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.40 % (2976175)Will run a generic schedule for satisfiability detection.
% 0.08/0.40 % (2976182)% WARNING: option uhcvi not known.
% 0.08/0.40 % (2976182)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=592901185:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.40 % (2976186)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=698334038:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.40 % (2976183)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1060865239:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.40 % (2976184)dis+10_1_sil=32000:sp=arity:random_seed=2535065246:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.40 % (2976185)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1236731481:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.40 % (2976181)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=866415905_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.40 % (2976187)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2683487044:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.40 % TRYING [1]
% 0.08/0.40 % TRYING [2]
% 0.08/0.40 % TRYING [3]
% 0.08/0.40 % TRYING [4]
% 0.08/0.40 % (2976187) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2976175-2976187"...
% 0.08/0.40 % (2976187)...printing done.
% 0.08/0.40 % (2976187)Refutation found. Thanks to Tanya!
% 0.08/0.40 % SZS status Unsatisfiable for theBenchmark
% 0.08/0.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/0.40 % (2976187)------------------------------
% 0.08/0.40 % (2976187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.40 % (2976187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.40 % (2976187)CaDiCaL version: 2.1.3
% 0.08/0.40 % (2976187)Termination reason: Refutation
% 0.08/0.40 % (2976187)Time elapsed: 0.035 s
% 0.08/0.40 % (2976187)Peak memory usage: 13 MB
% 0.08/0.40 % (2976187)Instructions burned: 85 (million)
% 0.08/0.40 % (2976175)Success in time 0.058 s
% 0.08/0.40 % Vampire exiting
%------------------------------------------------------------------------------