%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB068+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 01:00:54 PM UTC 2026
% Result : Theorem 0.98s 0.59s
% Output : Refutation 0.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 14
% Syntax : Number of formulae : 94 ( 25 unt; 9 def)
% Number of atoms : 327 ( 59 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 401 ( 168 ~; 188 |; 33 &)
% ( 11 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 13 con; 0-1 aty)
% Number of variables : 104 ( 0 sgn 90 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0,X1] :
( iext(uri_rdf_type,X0,X1)
<=> icext(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax',rdfs_cext_def) ).
fof(f345,axiom,
! [X0,X1] :
( iext(uri_owl_differentFrom,X0,X1)
<=> X0 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax',owl_eqdis_differentfrom) ).
fof(f366,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( iext(uri_rdf_first,X0,X1)
& iext(uri_rdf_rest,X0,X2)
& iext(uri_rdf_first,X2,X3)
& iext(uri_rdf_rest,X2,X4)
& iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,uri_rdf_nil)
& X1 != X3
& X1 != X5
& X3 != X5 )
=> ? [X6] :
( icext(uri_owl_AllDifferent,X6)
& iext(uri_owl_members,X6,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax',owl_ndis_alldifferent_members_fi_003) ).
fof(f559,conjecture,
? [X0,X1,X2,X3] :
( iext(uri_rdf_first,X1,uri_ex_w1)
& iext(uri_rdf_rest,X1,X2)
& iext(uri_rdf_first,X2,uri_ex_w2)
& iext(uri_rdf_rest,X2,X0)
& iext(uri_rdf_type,X3,uri_owl_AllDifferent)
& iext(uri_owl_members,X3,X1)
& iext(uri_rdf_first,X0,uri_ex_w3)
& iext(uri_rdf_rest,X0,uri_rdf_nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conclusion_rdfbased_sem_ndis_alldifferent_bw) ).
fof(f560,negated_conjecture,
~ ? [X0,X1,X2,X3] :
( iext(uri_rdf_first,X1,uri_ex_w1)
& iext(uri_rdf_rest,X1,X2)
& iext(uri_rdf_first,X2,uri_ex_w2)
& iext(uri_rdf_rest,X2,X0)
& iext(uri_rdf_type,X3,uri_owl_AllDifferent)
& iext(uri_owl_members,X3,X1)
& iext(uri_rdf_first,X0,uri_ex_w3)
& iext(uri_rdf_rest,X0,uri_rdf_nil) ),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X0,X1,X2] :
( iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w2)
& iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w3)
& iext(uri_rdf_first,X0,uri_ex_w3)
& iext(uri_rdf_rest,X0,uri_rdf_nil)
& iext(uri_owl_differentFrom,uri_ex_w2,uri_ex_w3)
& iext(uri_rdf_first,X2,uri_ex_w2)
& iext(uri_rdf_rest,X2,X0)
& iext(uri_rdf_first,X1,uri_ex_w1)
& iext(uri_rdf_rest,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_rdfbased_sem_ndis_alldifferent_bw) ).
fof(f814,plain,
! [X0,X1,X2,X3,X4,X5] :
( ? [X6] :
( icext(uri_owl_AllDifferent,X6)
& iext(uri_owl_members,X6,X0) )
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| X1 = X3
| X1 = X5
| X3 = X5 ),
inference(ennf_transformation,[],[f366]) ).
fof(f815,plain,
! [X0,X1,X2,X3,X4,X5] :
( ? [X6] :
( icext(uri_owl_AllDifferent,X6)
& iext(uri_owl_members,X6,X0) )
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| X1 = X3
| X1 = X5
| X3 = X5 ),
inference(flattening,[],[f814]) ).
fof(f980,plain,
! [X0,X1,X2,X3] :
( ~ iext(uri_rdf_first,X1,uri_ex_w1)
| ~ iext(uri_rdf_rest,X1,X2)
| ~ iext(uri_rdf_first,X2,uri_ex_w2)
| ~ iext(uri_rdf_rest,X2,X0)
| ~ iext(uri_rdf_type,X3,uri_owl_AllDifferent)
| ~ iext(uri_owl_members,X3,X1)
| ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil) ),
inference(ennf_transformation,[],[f560]) ).
fof(f1006,plain,
! [X0,X1] :
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ),
inference(cnf_transformation,[],[f25]) ).
fof(f1788,plain,
! [X0,X1] :
( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[],[f345]) ).
fof(f1878,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| X1 = X5
| X1 = X3
| X3 = X5
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| iext(uri_owl_members,sK141(X0),X0) ),
inference(cnf_transformation,[],[f815]) ).
fof(f1879,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| X1 = X5
| X1 = X3
| X3 = X5
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| icext(uri_owl_AllDifferent,sK141(X0)) ),
inference(cnf_transformation,[],[f815]) ).
fof(f2207,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_owl_members,X3,X1)
| ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_type,X3,uri_owl_AllDifferent)
| ~ iext(uri_rdf_rest,X2,X0)
| ~ iext(uri_rdf_first,X2,uri_ex_w2)
| ~ iext(uri_rdf_rest,X1,X2)
| ~ iext(uri_rdf_first,X1,uri_ex_w1) ),
inference(cnf_transformation,[],[f980]) ).
fof(f2208,plain,
iext(uri_rdf_rest,sK206,sK207),
inference(cnf_transformation,[],[f561]) ).
fof(f2209,plain,
iext(uri_rdf_first,sK206,uri_ex_w1),
inference(cnf_transformation,[],[f561]) ).
fof(f2210,plain,
iext(uri_rdf_rest,sK207,sK205),
inference(cnf_transformation,[],[f561]) ).
fof(f2211,plain,
iext(uri_rdf_first,sK207,uri_ex_w2),
inference(cnf_transformation,[],[f561]) ).
fof(f2212,plain,
iext(uri_owl_differentFrom,uri_ex_w2,uri_ex_w3),
inference(cnf_transformation,[],[f561]) ).
fof(f2213,plain,
iext(uri_rdf_rest,sK205,uri_rdf_nil),
inference(cnf_transformation,[],[f561]) ).
fof(f2214,plain,
iext(uri_rdf_first,sK205,uri_ex_w3),
inference(cnf_transformation,[],[f561]) ).
fof(f2215,plain,
iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w3),
inference(cnf_transformation,[],[f561]) ).
fof(f2216,plain,
iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w2),
inference(cnf_transformation,[],[f561]) ).
fof(f2231,plain,
! [X1] : ~ iext(uri_owl_differentFrom,X1,X1),
inference(equality_resolution,[],[f1788]) ).
fof(f2353,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_rdf_rest,X4,X3)
| X0 = X2
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X1)
| ~ iext(uri_rdf_rest,X3,sK205)
| ~ iext(uri_rdf_first,X3,X2)
| X0 = X1
| ~ iext(uri_rdf_first,X4,X0)
| icext(uri_owl_AllDifferent,sK141(X4)) ),
inference(resolution,[],[f1879,f2213]) ).
fof(f2354,plain,
! [X2,X0,X1] :
( X0 = X1
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X2)
| ~ iext(uri_rdf_rest,sK207,sK205)
| ~ iext(uri_rdf_first,sK207,X1)
| X0 = X2
| ~ iext(uri_rdf_first,sK206,X0)
| icext(uri_owl_AllDifferent,sK141(sK206)) ),
inference(resolution,[],[f2353,f2208]) ).
fof(f2357,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_rdf_rest,X4,X3)
| X0 = X2
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X1)
| ~ iext(uri_rdf_rest,X3,sK205)
| ~ iext(uri_rdf_first,X3,X2)
| X0 = X1
| ~ iext(uri_rdf_first,X4,X0)
| iext(uri_owl_members,sK141(X4),X4) ),
inference(resolution,[],[f1878,f2213]) ).
fof(f2358,plain,
! [X2,X0,X1] :
( X0 = X1
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X2)
| ~ iext(uri_rdf_rest,sK207,sK205)
| ~ iext(uri_rdf_first,sK207,X1)
| X0 = X2
| ~ iext(uri_rdf_first,sK206,X0)
| iext(uri_owl_members,sK141(sK206),sK206) ),
inference(resolution,[],[f2357,f2208]) ).
fof(f2464,plain,
! [X2,X0,X1] :
( X0 = X1
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X2)
| ~ iext(uri_rdf_first,sK207,X1)
| X0 = X2
| ~ iext(uri_rdf_first,sK206,X0)
| icext(uri_owl_AllDifferent,sK141(sK206)) ),
inference(forward_subsumption_resolution,[],[f2354,f2210]) ).
fof(f2470,plain,
! [X2,X0,X1] :
( X0 = X1
| X1 = X2
| ~ iext(uri_rdf_first,sK205,X2)
| ~ iext(uri_rdf_first,sK207,X1)
| X0 = X2
| ~ iext(uri_rdf_first,sK206,X0)
| iext(uri_owl_members,sK141(sK206),sK206) ),
inference(forward_subsumption_resolution,[],[f2358,f2210]) ).
fof(f2472,definition,
( spl208_24
<=> icext(uri_owl_AllDifferent,sK141(sK206)) ),
introduced(definition,[new_symbols(definition,[spl208_24])],[avatar_definition]) ).
fof(f2474,plain,
( icext(uri_owl_AllDifferent,sK141(sK206))
| ~ spl208_24 ),
inference(avatar_component_clause,[],[f2472]) ).
fof(f2476,definition,
( spl208_25
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ iext(uri_rdf_first,sK206,X0)
| X0 = X2
| ~ iext(uri_rdf_first,sK207,X1)
| ~ iext(uri_rdf_first,sK205,X2)
| X1 = X2 ) ),
introduced(definition,[new_symbols(definition,[spl208_25])],[avatar_definition]) ).
fof(f2477,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_rdf_first,sK207,X1)
| ~ iext(uri_rdf_first,sK206,X0)
| X0 = X2
| X0 = X1
| ~ iext(uri_rdf_first,sK205,X2)
| X1 = X2 )
| ~ spl208_25 ),
inference(avatar_component_clause,[],[f2476]) ).
fof(f2478,plain,
( spl208_24
| spl208_25 ),
inference(avatar_split_clause,[],[f2464,f2476,f2472]) ).
fof(f2480,definition,
( spl208_26
<=> iext(uri_owl_members,sK141(sK206),sK206) ),
introduced(definition,[new_symbols(definition,[spl208_26])],[avatar_definition]) ).
fof(f2482,plain,
( iext(uri_owl_members,sK141(sK206),sK206)
| ~ spl208_26 ),
inference(avatar_component_clause,[],[f2480]) ).
fof(f2483,plain,
( spl208_26
| spl208_25 ),
inference(avatar_split_clause,[],[f2470,f2476,f2480]) ).
fof(f2535,definition,
( spl208_35
<=> uri_ex_w2 = uri_ex_w3 ),
introduced(definition,[new_symbols(definition,[spl208_35])],[avatar_definition]) ).
fof(f2537,plain,
( uri_ex_w2 = uri_ex_w3
| ~ spl208_35 ),
inference(avatar_component_clause,[],[f2535]) ).
fof(f2540,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,sK206,X0)
| X0 = X1
| uri_ex_w2 = X0
| ~ iext(uri_rdf_first,sK205,X1)
| uri_ex_w2 = X1 )
| ~ spl208_25 ),
inference(resolution,[],[f2477,f2211]) ).
fof(f2541,plain,
( ! [X0] :
( uri_ex_w1 = X0
| uri_ex_w1 = uri_ex_w2
| ~ iext(uri_rdf_first,sK205,X0)
| uri_ex_w2 = X0 )
| ~ spl208_25 ),
inference(resolution,[],[f2540,f2209]) ).
fof(f2543,definition,
( spl208_36
<=> uri_ex_w1 = uri_ex_w2 ),
introduced(definition,[new_symbols(definition,[spl208_36])],[avatar_definition]) ).
fof(f2545,plain,
( uri_ex_w1 = uri_ex_w2
| ~ spl208_36 ),
inference(avatar_component_clause,[],[f2543]) ).
fof(f2547,definition,
( spl208_37
<=> ! [X0] :
( uri_ex_w1 = X0
| uri_ex_w2 = X0
| ~ iext(uri_rdf_first,sK205,X0) ) ),
introduced(definition,[new_symbols(definition,[spl208_37])],[avatar_definition]) ).
fof(f2548,plain,
( ! [X0] :
( ~ iext(uri_rdf_first,sK205,X0)
| uri_ex_w2 = X0
| uri_ex_w1 = X0 )
| ~ spl208_37 ),
inference(avatar_component_clause,[],[f2547]) ).
fof(f2549,plain,
( spl208_36
| spl208_37
| ~ spl208_25 ),
inference(avatar_split_clause,[],[f2541,f2476,f2547,f2543]) ).
fof(f2551,plain,
( iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w1)
| ~ spl208_36 ),
inference(superposition,[],[f2216,f2545]) ).
fof(f2554,plain,
( $false
| ~ spl208_36 ),
inference(forward_subsumption_resolution,[],[f2551,f2231]) ).
fof(f2555,plain,
~ spl208_36,
inference(avatar_contradiction_clause,[],[f2554]) ).
fof(f2556,plain,
( uri_ex_w2 = uri_ex_w3
| uri_ex_w1 = uri_ex_w3
| ~ spl208_37 ),
inference(resolution,[],[f2548,f2214]) ).
fof(f2558,definition,
( spl208_38
<=> uri_ex_w1 = uri_ex_w3 ),
introduced(definition,[new_symbols(definition,[spl208_38])],[avatar_definition]) ).
fof(f2560,plain,
( uri_ex_w1 = uri_ex_w3
| ~ spl208_38 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2561,plain,
( spl208_38
| spl208_35
| ~ spl208_37 ),
inference(avatar_split_clause,[],[f2556,f2547,f2535,f2558]) ).
fof(f2565,plain,
( iext(uri_owl_differentFrom,uri_ex_w2,uri_ex_w2)
| ~ spl208_35 ),
inference(superposition,[],[f2212,f2537]) ).
fof(f2566,plain,
( $false
| ~ spl208_35 ),
inference(forward_subsumption_resolution,[],[f2565,f2231]) ).
fof(f2567,plain,
~ spl208_35,
inference(avatar_contradiction_clause,[],[f2566]) ).
fof(f2571,plain,
( iext(uri_owl_differentFrom,uri_ex_w1,uri_ex_w1)
| ~ spl208_38 ),
inference(superposition,[],[f2215,f2560]) ).
fof(f2574,plain,
( $false
| ~ spl208_38 ),
inference(forward_subsumption_resolution,[],[f2571,f2231]) ).
fof(f2575,plain,
~ spl208_38,
inference(avatar_contradiction_clause,[],[f2574]) ).
fof(f2582,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_type,sK141(sK206),uri_owl_AllDifferent)
| ~ iext(uri_rdf_rest,X1,X0)
| ~ iext(uri_rdf_first,X1,uri_ex_w2)
| ~ iext(uri_rdf_rest,sK206,X1)
| ~ iext(uri_rdf_first,sK206,uri_ex_w1) )
| ~ spl208_26 ),
inference(resolution,[],[f2482,f2207]) ).
fof(f2583,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_type,sK141(sK206),uri_owl_AllDifferent)
| ~ iext(uri_rdf_rest,X1,X0)
| ~ iext(uri_rdf_first,X1,uri_ex_w2)
| ~ iext(uri_rdf_rest,sK206,X1) )
| ~ spl208_26 ),
inference(forward_subsumption_resolution,[],[f2582,f2209]) ).
fof(f2589,definition,
( spl208_39
<=> iext(uri_rdf_type,sK141(sK206),uri_owl_AllDifferent) ),
introduced(definition,[new_symbols(definition,[spl208_39])],[avatar_definition]) ).
fof(f2591,plain,
( ~ iext(uri_rdf_type,sK141(sK206),uri_owl_AllDifferent)
| spl208_39 ),
inference(avatar_component_clause,[],[f2589]) ).
fof(f2593,definition,
( spl208_40
<=> ! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,sK206,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_w2)
| ~ iext(uri_rdf_rest,X1,X0)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil) ) ),
introduced(definition,[new_symbols(definition,[spl208_40])],[avatar_definition]) ).
fof(f2594,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_rest,sK206,X1)
| ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_first,X1,uri_ex_w2)
| ~ iext(uri_rdf_rest,X1,X0)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil) )
| ~ spl208_40 ),
inference(avatar_component_clause,[],[f2593]) ).
fof(f2595,plain,
( ~ spl208_39
| spl208_40
| ~ spl208_26 ),
inference(avatar_split_clause,[],[f2583,f2480,f2593,f2589]) ).
fof(f2603,plain,
( ! [X0] :
( ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_first,sK207,uri_ex_w2)
| ~ iext(uri_rdf_rest,sK207,X0)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil) )
| ~ spl208_40 ),
inference(resolution,[],[f2594,f2208]) ).
fof(f2604,plain,
( ! [X0] :
( ~ iext(uri_rdf_rest,sK207,X0)
| ~ iext(uri_rdf_first,X0,uri_ex_w3)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil) )
| ~ spl208_40 ),
inference(forward_subsumption_resolution,[],[f2603,f2211]) ).
fof(f2605,plain,
( ~ iext(uri_rdf_first,sK205,uri_ex_w3)
| ~ iext(uri_rdf_rest,sK205,uri_rdf_nil)
| ~ spl208_40 ),
inference(resolution,[],[f2604,f2210]) ).
fof(f2606,plain,
( ~ iext(uri_rdf_rest,sK205,uri_rdf_nil)
| ~ spl208_40 ),
inference(forward_subsumption_resolution,[],[f2605,f2214]) ).
fof(f2607,plain,
( $false
| ~ spl208_40 ),
inference(forward_subsumption_resolution,[],[f2606,f2213]) ).
fof(f2608,plain,
~ spl208_40,
inference(avatar_contradiction_clause,[],[f2607]) ).
fof(f2609,plain,
( ~ icext(uri_owl_AllDifferent,sK141(sK206))
| spl208_39 ),
inference(resolution,[],[f2591,f1006]) ).
fof(f2610,plain,
( $false
| ~ spl208_24
| spl208_39 ),
inference(forward_subsumption_resolution,[],[f2609,f2474]) ).
fof(f2611,plain,
( ~ spl208_24
| spl208_39 ),
inference(avatar_contradiction_clause,[],[f2610]) ).
cnf(s15,plain,
( spl208_24
| spl208_25 ),
inference(sat_conversion,[],[f2478]) ).
cnf(s16,plain,
( spl208_25
| spl208_26 ),
inference(sat_conversion,[],[f2483]) ).
cnf(s21,plain,
( ~ spl208_25
| spl208_36
| spl208_37 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s22,plain,
~ spl208_36,
inference(sat_conversion,[],[f2555]) ).
cnf(s23,plain,
( spl208_35
| ~ spl208_37
| spl208_38 ),
inference(sat_conversion,[],[f2561]) ).
cnf(s24,plain,
~ spl208_35,
inference(sat_conversion,[],[f2567]) ).
cnf(s26,plain,
~ spl208_38,
inference(sat_conversion,[],[f2575]) ).
cnf(s27,plain,
( ~ spl208_26
| ~ spl208_39
| spl208_40 ),
inference(sat_conversion,[],[f2595]) ).
cnf(s29,plain,
~ spl208_40,
inference(sat_conversion,[],[f2608]) ).
cnf(s30,plain,
( ~ spl208_24
| spl208_39 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s31,plain,
( ~ spl208_26
| ~ spl208_39 ),
inference(rat,[],[s27,s29]) ).
cnf(s32,plain,
~ spl208_37,
inference(rat,[],[s23,s26,s24]) ).
cnf(s33,plain,
~ spl208_25,
inference(rat,[],[s21,s32,s22]) ).
cnf(s35,plain,
spl208_26,
inference(rat,[],[s16,s33]) ).
cnf(s36,plain,
~ spl208_39,
inference(rat,[],[s31,s35]) ).
cnf(s37,plain,
~ spl208_24,
inference(rat,[],[s30,s36]) ).
cnf(s38,plain,
$false,
inference(rat,[],[s15,s33,s37]) ).
fof(f2612,plain,
$false,
inference(avatar_sat_refutation,[],[s38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB068+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 07:17:27 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.98/0.59 % (1402871)Will run a generic schedule for satisfiability detection.
% 0.98/0.59 % (1402878)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=480059692:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.98/0.59 % (1402877)% WARNING: option uhcvi not known.
% 0.98/0.59 % (1402876)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1070827739_2999 on theBenchmark for (2999ds/0Mi)
% 0.98/0.59 % (1402877)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4085084843:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.98/0.59 % (1402879)dis+10_1_sil=32000:sp=arity:random_seed=3642089533:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.98/0.59 % (1402880)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=211062931:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.98/0.59 % (1402881)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2334464553:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.98/0.59 % (1402882)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=506552321:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.98/0.59 % (1402879)Instruction limit reached!
% 0.98/0.59 % (1402879)------------------------------
% 0.98/0.59 % (1402879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.59 % (1402879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.59 % (1402879)CaDiCaL version: 2.1.3
% 0.98/0.59 % (1402879)Termination reason: Instruction limit
% 0.98/0.59 % (1402879)Termination phase: Saturation
% 0.98/0.59 % (1402879)Time elapsed: 0.054 s
% 0.98/0.59 % (1402879)Peak memory usage: 14 MB
% 0.98/0.59 % (1402879)Instructions burned: 103 (million)
% 0.98/0.59 % (1402880)Instruction limit reached!
% 0.98/0.59 % (1402880)------------------------------
% 0.98/0.59 % (1402880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.59 % (1402880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.59 % (1402880)CaDiCaL version: 2.1.3
% 0.98/0.59 % (1402880)Termination reason: Instruction limit
% 0.98/0.59 % (1402880)Termination phase: Saturation
% 0.98/0.59 % (1402880)Time elapsed: 0.056 s
% 0.98/0.59 % (1402880)Peak memory usage: 13 MB
% 0.98/0.59 % (1402880)Instructions burned: 117 (million)
% 0.98/0.59 % (1402881)Instruction limit reached!
% 0.98/0.59 % (1402881)------------------------------
% 0.98/0.59 % (1402881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.59 % (1402881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.59 % (1402881)CaDiCaL version: 2.1.3
% 0.98/0.59 % (1402881)Termination reason: Instruction limit
% 0.98/0.59 % (1402881)Termination phase: Saturation
% 0.98/0.59 % (1402881)Time elapsed: 0.067 s
% 0.98/0.59 % (1402881)Peak memory usage: 14 MB
% 0.98/0.59 % (1402881)Instructions burned: 131 (million)
% 0.98/0.59 % (1402890)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1242473091:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 0.98/0.59 % (1402891)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=944525521:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.98/0.59 % (1402882)Instruction limit reached!
% 0.98/0.59 % (1402882)------------------------------
% 0.98/0.59 % (1402882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.59 % (1402882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.59 % (1402882)CaDiCaL version: 2.1.3
% 0.98/0.59 % (1402882)Termination reason: Instruction limit
% 0.98/0.59 % (1402882)Termination phase: Saturation
% 0.98/0.59 % (1402882)Time elapsed: 0.085 s
% 0.98/0.59 % (1402882)Peak memory usage: 15 MB
% 0.98/0.59 % (1402882)Instructions burned: 160 (million)
% 0.98/0.59 % (1402892)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=209242161:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.98/0.59 % (1402895)ott-21_1_sil=16000:fs=off:random_seed=3935455101:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.98/0.59 % TRYING [1]
% 0.98/0.59 % TRYING [2]
% 0.98/0.59 % (1402892) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1402871-1402892"...
% 0.98/0.59 % (1402892)...printing done.
% 0.98/0.59 % (1402892)Refutation found. Thanks to Tanya!
% 0.98/0.59 % SZS status Theorem for theBenchmark
% 0.98/0.59 % SZS output start Proof for theBenchmark
% See solution above
% 0.98/0.60 % (1402892)------------------------------
% 0.98/0.60 % (1402892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.60 % (1402892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.60 % (1402892)CaDiCaL version: 2.1.3
% 0.98/0.60 % (1402892)Termination reason: Refutation
% 0.98/0.60 % (1402892)Time elapsed: 0.043 s
% 0.98/0.60 % (1402892)Peak memory usage: 14 MB
% 0.98/0.60 % (1402892)Instructions burned: 80 (million)
% 0.98/0.60 % (1402871)Success in time 0.181 s
% 0.98/0.60 % Vampire exiting
%------------------------------------------------------------------------------