%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV007-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 10:58:54 AM UTC 2026
% Result : Unsatisfiable 0.17s 0.48s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 73
% Syntax : Number of formulae : 268 ( 74 unt; 25 def)
% Number of atoms : 520 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 473 ( 221 ~; 227 |; 0 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 38 ( 37 usr; 26 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 58 ( 0 sgn 58 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ zero(X0)
| ~ connection(X0,X1)
| zero(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_zero1) ).
fof(f2,axiom,
! [X0,X1] :
( ~ one(X0)
| ~ connection(X0,X1)
| one(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_one1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ zero(X1)
| ~ connection(X0,X1)
| zero(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_zero2) ).
fof(f4,axiom,
! [X0,X1] :
( ~ one(X1)
| ~ connection(X0,X1)
| one(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_one2) ).
fof(f5,axiom,
! [X0] :
( ~ one(X0)
| ~ zero(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',unique_value) ).
fof(f7,axiom,
! [X0] :
( ~ and_ok(X0)
| ~ zero(in2(X0))
| zero(out1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_x0_0) ).
fof(f8,axiom,
! [X0] :
( ~ and_ok(X0)
| ~ one(in1(X0))
| ~ one(in2(X0))
| one(out1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_11_1) ).
fof(f10,axiom,
! [X0] :
( ~ and_ok(X0)
| ~ one(out1(X0))
| one(in1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_1_1x) ).
fof(f13,axiom,
! [X0] :
( ~ logic_and(X0)
| and_ok(X0)
| abnormal(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_ok_or_abnormal) ).
fof(f17,axiom,
! [X0] :
( ~ or_ok(X0)
| ~ one(out1(X0))
| one(in1(X0))
| one(in2(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',or_1_11) ).
fof(f19,axiom,
! [X0] :
( ~ or_ok(X0)
| ~ zero(out1(X0))
| zero(in2(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',or_0_01) ).
fof(f21,axiom,
! [X0] :
( ~ logic_or(X0)
| or_ok(X0)
| abnormal(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',or_ok_or_abnormal) ).
fof(f23,axiom,
! [X0] :
( ~ not_ok(X0)
| ~ one(in1(X0))
| zero(out1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',not_1_0_fw) ).
fof(f27,axiom,
! [X0] :
( ~ logic_not(X0)
| not_ok(X0)
| abnormal(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',not_ok_or_abnormal) ).
fof(f28,axiom,
! [X0] :
( ~ halfadder(X0)
| logic_and(and1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_and1) ).
fof(f29,axiom,
! [X0] :
( ~ halfadder(X0)
| logic_and(and2(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_and2) ).
fof(f30,axiom,
! [X0] :
( ~ halfadder(X0)
| logic_not(not1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_not1) ).
fof(f31,axiom,
! [X0] :
( ~ halfadder(X0)
| logic_or(or1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_or1) ).
fof(f32,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(in1(X0),in1(or1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_in1_in1or1) ).
fof(f33,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(in2(X0),in2(or1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_in2_in2or1) ).
fof(f34,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(in1(X0),in1(and2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_in1_in1and2) ).
fof(f35,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(in2(X0),in2(and2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_in2_in2and2) ).
fof(f36,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(outs(X0),out1(and1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_outs_out1and1) ).
fof(f37,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(outc(X0),out1(and2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_outc_out1and2) ).
fof(f38,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(out1(or1(X0)),in1(and1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_out1or1_in1_and1) ).
fof(f39,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(out1(and2(X0)),in1(not1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_out1and2_in1not1) ).
fof(f40,axiom,
! [X0] :
( ~ halfadder(X0)
| connection(out1(not1(X0)),in2(and1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_out1not1_in2and1) ).
fof(f41,axiom,
! [X0] :
( ~ fulladder(X0)
| halfadder(h1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_halfadder1) ).
fof(f42,axiom,
! [X0] :
( ~ fulladder(X0)
| halfadder(h2(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_halfadder2) ).
fof(f43,axiom,
! [X0] :
( ~ fulladder(X0)
| logic_or(or1(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_or1) ).
fof(f44,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(outs(h1(X0)),in2(h2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outsh1_in2h2) ).
fof(f45,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(outc(h1(X0)),in2(or1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outch1_in2or1) ).
fof(f47,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(in1(X0),in1(h2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_in1_in1h2) ).
fof(f48,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(in2(X0),in1(h1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_in2_in1h1) ).
fof(f49,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(inc(X0),in2(h1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_inc_in2h1) ).
fof(f50,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(outs(X0),outs(h2(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outs_outsh2) ).
fof(f51,axiom,
! [X0] :
( ~ fulladder(X0)
| connection(outc(X0),out1(or1(X0))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outc_out1or1) ).
fof(f52,axiom,
fulladder(f),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_isa_fulladder) ).
fof(f53,axiom,
zero(in1(f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in1_1) ).
fof(f54,axiom,
one(in2(f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in2_0) ).
fof(f55,axiom,
one(inc(f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inc_1) ).
fof(f56,axiom,
one(outs(f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outs_1) ).
fof(f57,axiom,
zero(outc(f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outc_0) ).
fof(f58,negated_conjecture,
~ abnormal(and2(h1(f))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h1) ).
fof(f59,negated_conjecture,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h1(f))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_and1h1) ).
fof(f60,negated_conjecture,
( ~ abnormal(or1(f))
| ~ abnormal(not1(h1(f))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_not1h1) ).
fof(f61,negated_conjecture,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h2(f))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_and1h2) ).
fof(f62,negated_conjecture,
( ~ abnormal(or1(f))
| ~ abnormal(or1(h2(f))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_or1h2) ).
fof(f64,definition,
( spl0_1
<=> abnormal(or1(h2(f))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f68,definition,
( spl0_2
<=> abnormal(or1(f)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f70,plain,
( ~ abnormal(or1(f))
| spl0_2 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f71,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f62,f68,f64]) ).
fof(f73,definition,
( spl0_3
<=> abnormal(and1(h2(f))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f76,plain,
( ~ spl0_3
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f61,f68,f73]) ).
fof(f78,definition,
( spl0_4
<=> abnormal(not1(h1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f81,plain,
( ~ spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f60,f68,f78]) ).
fof(f83,definition,
( spl0_5
<=> abnormal(and1(h1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f86,plain,
( ~ spl0_5
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f59,f68,f83]) ).
fof(f90,plain,
halfadder(h1(f)),
inference(resolution,[],[f41,f52]) ).
fof(f92,plain,
logic_not(not1(h1(f))),
inference(resolution,[],[f90,f30]) ).
fof(f93,plain,
logic_and(and2(h1(f))),
inference(resolution,[],[f90,f29]) ).
fof(f94,plain,
logic_and(and1(h1(f))),
inference(resolution,[],[f90,f28]) ).
fof(f95,plain,
halfadder(h2(f)),
inference(resolution,[],[f42,f52]) ).
fof(f96,plain,
logic_or(or1(h2(f))),
inference(resolution,[],[f95,f31]) ).
fof(f99,plain,
logic_and(and1(h2(f))),
inference(resolution,[],[f95,f28]) ).
fof(f100,plain,
logic_or(or1(f)),
inference(resolution,[],[f43,f52]) ).
fof(f101,plain,
( or_ok(or1(f))
| abnormal(or1(f)) ),
inference(resolution,[],[f21,f100]) ).
fof(f112,plain,
( or_ok(or1(f))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f101,f70]) ).
fof(f114,plain,
( not_ok(not1(h1(f)))
| abnormal(not1(h1(f))) ),
inference(resolution,[],[f92,f27]) ).
fof(f116,definition,
( spl0_8
<=> not_ok(not1(h1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f118,plain,
( not_ok(not1(h1(f)))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
( spl0_4
| spl0_8 ),
inference(avatar_split_clause,[],[f114,f116,f78]) ).
fof(f121,plain,
! [X0] :
( ~ connection(in1(f),X0)
| zero(X0) ),
inference(resolution,[],[f1,f53]) ).
fof(f122,plain,
! [X0] :
( ~ connection(outc(f),X0)
| zero(X0) ),
inference(resolution,[],[f1,f57]) ).
fof(f123,plain,
( and_ok(and2(h1(f)))
| abnormal(and2(h1(f))) ),
inference(resolution,[],[f93,f13]) ).
fof(f124,plain,
and_ok(and2(h1(f))),
inference(forward_subsumption_resolution,[],[f123,f58]) ).
fof(f125,plain,
! [X0] :
( ~ connection(in2(f),X0)
| one(X0) ),
inference(resolution,[],[f2,f54]) ).
fof(f126,plain,
! [X0] :
( ~ connection(inc(f),X0)
| one(X0) ),
inference(resolution,[],[f2,f55]) ).
fof(f127,plain,
! [X0] :
( ~ connection(outs(f),X0)
| one(X0) ),
inference(resolution,[],[f2,f56]) ).
fof(f130,plain,
( and_ok(and1(h1(f)))
| abnormal(and1(h1(f))) ),
inference(resolution,[],[f94,f13]) ).
fof(f132,definition,
( spl0_9
<=> and_ok(and1(h1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f134,plain,
( and_ok(and1(h1(f)))
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f135,plain,
( spl0_5
| spl0_9 ),
inference(avatar_split_clause,[],[f130,f132,f83]) ).
fof(f139,plain,
( or_ok(or1(h2(f)))
| abnormal(or1(h2(f))) ),
inference(resolution,[],[f96,f21]) ).
fof(f141,definition,
( spl0_10
<=> or_ok(or1(h2(f))) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f143,plain,
( or_ok(or1(h2(f)))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
( spl0_1
| spl0_10 ),
inference(avatar_split_clause,[],[f139,f141,f64]) ).
fof(f147,definition,
( spl0_11
<=> zero(out1(and2(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f148,plain,
( ~ zero(out1(and2(h1(f))))
| spl0_11 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f149,plain,
( zero(out1(and2(h1(f))))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f163,definition,
( spl0_14
<=> one(in1(and2(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f164,plain,
( ~ one(in1(and2(h1(f))))
| spl0_14 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f167,definition,
( spl0_15
<=> one(out1(and2(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f168,plain,
( one(out1(and2(h1(f))))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f169,plain,
( ~ one(out1(and2(h1(f))))
| spl0_15 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f204,definition,
( spl0_22
<=> zero(out1(or1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f205,plain,
( zero(out1(or1(f)))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( ~ zero(out1(or1(f)))
| spl0_22 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f208,plain,
( ~ zero(out1(or1(f)))
| zero(in2(or1(f)))
| spl0_2 ),
inference(resolution,[],[f19,f112]) ).
fof(f219,plain,
( and_ok(and1(h2(f)))
| abnormal(and1(h2(f))) ),
inference(resolution,[],[f99,f13]) ).
fof(f221,definition,
( spl0_25
<=> and_ok(and1(h2(f))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f223,plain,
( and_ok(and1(h2(f)))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f224,plain,
( spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f219,f221,f73]) ).
fof(f230,plain,
( ~ zero(in2(and1(h1(f))))
| zero(out1(and1(h1(f))))
| ~ spl0_9 ),
inference(resolution,[],[f134,f7]) ).
fof(f233,definition,
( spl0_26
<=> zero(out1(and1(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f235,plain,
( zero(out1(and1(h1(f))))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f242,definition,
( spl0_28
<=> zero(in2(and1(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f244,plain,
( ~ zero(in2(and1(h1(f))))
| spl0_28 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f245,plain,
( spl0_26
| ~ spl0_28
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f230,f132,f242,f233]) ).
fof(f267,definition,
( spl0_32
<=> one(out1(or1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f268,plain,
( ~ one(out1(or1(h2(f))))
| spl0_32 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl0_33
<=> one(in1(or1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f272,plain,
( one(in1(or1(h2(f))))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( ~ one(in1(or1(h2(f))))
| spl0_33 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f276,definition,
( spl0_34
<=> one(in2(or1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f277,plain,
( one(in2(or1(h2(f))))
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f278,plain,
( ~ one(in2(or1(h2(f))))
| spl0_34 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f281,definition,
( spl0_35
<=> zero(in1(or1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f282,plain,
( ~ zero(in1(or1(h2(f))))
| spl0_35 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( zero(in1(or1(h2(f))))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f298,plain,
connection(in1(h2(f)),in1(or1(h2(f)))),
inference(resolution,[],[f32,f95]) ).
fof(f300,plain,
connection(in2(h2(f)),in2(or1(h2(f)))),
inference(resolution,[],[f33,f95]) ).
fof(f301,plain,
connection(in1(h1(f)),in1(and2(h1(f)))),
inference(resolution,[],[f34,f90]) ).
fof(f303,plain,
connection(in2(h1(f)),in2(and2(h1(f)))),
inference(resolution,[],[f35,f90]) ).
fof(f305,plain,
connection(outs(h1(f)),out1(and1(h1(f)))),
inference(resolution,[],[f36,f90]) ).
fof(f306,plain,
connection(outs(h2(f)),out1(and1(h2(f)))),
inference(resolution,[],[f36,f95]) ).
fof(f307,plain,
connection(outc(h1(f)),out1(and2(h1(f)))),
inference(resolution,[],[f37,f90]) ).
fof(f309,plain,
connection(in1(f),in1(h2(f))),
inference(resolution,[],[f47,f52]) ).
fof(f310,plain,
connection(in2(f),in1(h1(f))),
inference(resolution,[],[f48,f52]) ).
fof(f311,plain,
connection(inc(f),in2(h1(f))),
inference(resolution,[],[f49,f52]) ).
fof(f312,plain,
connection(outs(f),outs(h2(f))),
inference(resolution,[],[f50,f52]) ).
fof(f313,plain,
connection(outc(f),out1(or1(f))),
inference(resolution,[],[f51,f52]) ).
fof(f315,plain,
connection(out1(or1(h2(f))),in1(and1(h2(f)))),
inference(resolution,[],[f38,f95]) ).
fof(f316,plain,
connection(out1(and2(h1(f))),in1(not1(h1(f)))),
inference(resolution,[],[f39,f90]) ).
fof(f318,plain,
connection(out1(not1(h1(f))),in2(and1(h1(f)))),
inference(resolution,[],[f40,f90]) ).
fof(f320,plain,
connection(outs(h1(f)),in2(h2(f))),
inference(resolution,[],[f44,f52]) ).
fof(f321,plain,
connection(outc(h1(f)),in2(or1(f))),
inference(resolution,[],[f45,f52]) ).
fof(f323,plain,
( ~ one(in1(and2(h1(f))))
| ~ one(in2(and2(h1(f))))
| one(out1(and2(h1(f)))) ),
inference(resolution,[],[f8,f124]) ).
fof(f326,plain,
( ~ one(in1(and2(h1(f))))
| ~ one(in2(and2(h1(f))))
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f323,f169]) ).
fof(f329,definition,
( spl0_38
<=> one(in2(and2(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f331,plain,
( ~ one(in2(and2(h1(f))))
| spl0_38 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( ~ spl0_38
| ~ spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f326,f167,f163,f329]) ).
fof(f347,definition,
( spl0_39
<=> zero(in2(or1(f))) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f348,plain,
( zero(in2(or1(f)))
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f352,plain,
( ~ one(out1(or1(h2(f))))
| one(in1(or1(h2(f))))
| one(in2(or1(h2(f))))
| ~ spl0_10 ),
inference(resolution,[],[f17,f143]) ).
fof(f353,plain,
( ~ one(out1(or1(h2(f))))
| one(in2(or1(h2(f))))
| ~ spl0_10
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f352,f273]) ).
fof(f355,plain,
( ~ one(out1(or1(h2(f))))
| ~ spl0_10
| spl0_33
| spl0_34 ),
inference(forward_subsumption_resolution,[],[f353,f278]) ).
fof(f357,plain,
( ~ spl0_32
| ~ spl0_10
| spl0_33
| spl0_34 ),
inference(avatar_split_clause,[],[f355,f276,f271,f141,f267]) ).
fof(f359,plain,
zero(in1(h2(f))),
inference(resolution,[],[f309,f121]) ).
fof(f361,plain,
! [X0] :
( ~ connection(in1(h2(f)),X0)
| zero(X0) ),
inference(resolution,[],[f359,f1]) ).
fof(f362,plain,
one(in1(h1(f))),
inference(resolution,[],[f310,f125]) ).
fof(f364,plain,
! [X0] :
( ~ connection(in1(h1(f)),X0)
| one(X0) ),
inference(resolution,[],[f362,f2]) ).
fof(f366,plain,
one(in2(h1(f))),
inference(resolution,[],[f311,f126]) ).
fof(f368,plain,
! [X0] :
( ~ connection(in2(h1(f)),X0)
| one(X0) ),
inference(resolution,[],[f366,f2]) ).
fof(f370,plain,
one(outs(h2(f))),
inference(resolution,[],[f312,f127]) ).
fof(f372,plain,
! [X0] :
( ~ connection(outs(h2(f)),X0)
| one(X0) ),
inference(resolution,[],[f370,f2]) ).
fof(f374,plain,
zero(out1(or1(f))),
inference(resolution,[],[f313,f122]) ).
fof(f375,plain,
( $false
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f374,f206]) ).
fof(f376,plain,
spl0_22,
inference(avatar_contradiction_clause,[],[f375]) ).
fof(f377,plain,
( zero(in2(or1(f)))
| spl0_2
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f208,f205]) ).
fof(f378,plain,
( spl0_39
| spl0_2
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f377,f204,f68,f347]) ).
fof(f391,plain,
( ~ one(in1(not1(h1(f))))
| zero(out1(not1(h1(f))))
| ~ spl0_8 ),
inference(resolution,[],[f118,f23]) ).
fof(f404,definition,
( spl0_42
<=> zero(out1(not1(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f406,plain,
( zero(out1(not1(h1(f))))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f408,definition,
( spl0_43
<=> one(in1(not1(h1(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f410,plain,
( ~ one(in1(not1(h1(f))))
| spl0_43 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f411,plain,
( spl0_42
| ~ spl0_43
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f391,f116,f408,f404]) ).
fof(f417,plain,
( ~ one(out1(and1(h2(f))))
| one(in1(and1(h2(f))))
| ~ spl0_25 ),
inference(resolution,[],[f223,f10]) ).
fof(f435,definition,
( spl0_47
<=> one(in1(and1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f437,plain,
( one(in1(and1(h2(f))))
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f439,definition,
( spl0_48
<=> one(out1(and1(h2(f)))) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f441,plain,
( ~ one(out1(and1(h2(f))))
| spl0_48 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f442,plain,
( spl0_47
| ~ spl0_48
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f417,f221,f439,f435]) ).
fof(f459,plain,
zero(in1(or1(h2(f)))),
inference(resolution,[],[f361,f298]) ).
fof(f461,plain,
( $false
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f459,f282]) ).
fof(f462,plain,
spl0_35,
inference(avatar_contradiction_clause,[],[f461]) ).
fof(f467,plain,
one(in1(and2(h1(f)))),
inference(resolution,[],[f364,f301]) ).
fof(f468,plain,
( $false
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f467,f164]) ).
fof(f469,plain,
spl0_14,
inference(avatar_contradiction_clause,[],[f468]) ).
fof(f475,plain,
one(in2(and2(h1(f)))),
inference(resolution,[],[f368,f303]) ).
fof(f476,plain,
( $false
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f475,f331]) ).
fof(f477,plain,
spl0_38,
inference(avatar_contradiction_clause,[],[f476]) ).
fof(f479,plain,
( ! [X0] :
( ~ connection(out1(and2(h1(f))),X0)
| one(X0) )
| ~ spl0_15 ),
inference(resolution,[],[f168,f2]) ).
fof(f480,plain,
( ~ zero(out1(and2(h1(f))))
| ~ spl0_15 ),
inference(resolution,[],[f168,f5]) ).
fof(f485,plain,
one(out1(and1(h2(f)))),
inference(resolution,[],[f372,f306]) ).
fof(f486,plain,
( $false
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f485,f441]) ).
fof(f487,plain,
spl0_48,
inference(avatar_contradiction_clause,[],[f486]) ).
fof(f496,plain,
( ! [X0] :
( ~ connection(X0,in2(or1(f)))
| zero(X0) )
| ~ spl0_39 ),
inference(resolution,[],[f348,f3]) ).
fof(f498,plain,
( zero(outc(h1(f)))
| ~ spl0_39 ),
inference(resolution,[],[f496,f321]) ).
fof(f500,plain,
( ! [X0] :
( ~ connection(outc(h1(f)),X0)
| zero(X0) )
| ~ spl0_39 ),
inference(resolution,[],[f498,f1]) ).
fof(f501,plain,
( zero(out1(and2(h1(f))))
| ~ spl0_39 ),
inference(resolution,[],[f500,f307]) ).
fof(f503,plain,
( $false
| spl0_11
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f501,f148]) ).
fof(f504,plain,
( spl0_11
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f503]) ).
fof(f507,plain,
( $false
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f480,f149]) ).
fof(f508,plain,
( ~ spl0_11
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f507]) ).
fof(f521,plain,
( ! [X0] :
( ~ connection(X0,in1(and1(h2(f))))
| one(X0) )
| ~ spl0_47 ),
inference(resolution,[],[f437,f4]) ).
fof(f532,plain,
( one(in1(not1(h1(f))))
| ~ spl0_15 ),
inference(resolution,[],[f479,f316]) ).
fof(f533,plain,
( $false
| ~ spl0_15
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f532,f410]) ).
fof(f534,plain,
( ~ spl0_15
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f533]) ).
fof(f536,plain,
( ! [X0] :
( ~ connection(out1(not1(h1(f))),X0)
| zero(X0) )
| ~ spl0_42 ),
inference(resolution,[],[f406,f1]) ).
fof(f556,plain,
( one(out1(or1(h2(f))))
| ~ spl0_47 ),
inference(resolution,[],[f521,f315]) ).
fof(f557,plain,
( $false
| spl0_32
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f556,f268]) ).
fof(f558,plain,
( spl0_32
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f557]) ).
fof(f564,plain,
( ~ zero(in1(or1(h2(f))))
| ~ spl0_33 ),
inference(resolution,[],[f272,f5]) ).
fof(f565,plain,
( $false
| ~ spl0_33
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f564,f283]) ).
fof(f566,plain,
( ~ spl0_33
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f565]) ).
fof(f567,plain,
( ! [X0] :
( ~ connection(X0,in2(or1(h2(f))))
| one(X0) )
| ~ spl0_34 ),
inference(resolution,[],[f277,f4]) ).
fof(f570,plain,
( zero(in2(and1(h1(f))))
| ~ spl0_42 ),
inference(resolution,[],[f536,f318]) ).
fof(f571,plain,
( $false
| spl0_28
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f570,f244]) ).
fof(f572,plain,
( spl0_28
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f571]) ).
fof(f573,plain,
( ! [X0] :
( ~ connection(X0,out1(and1(h1(f))))
| zero(X0) )
| ~ spl0_26 ),
inference(resolution,[],[f235,f3]) ).
fof(f587,plain,
( one(in2(h2(f)))
| ~ spl0_34 ),
inference(resolution,[],[f567,f300]) ).
fof(f588,plain,
( ! [X0] :
( ~ connection(X0,in2(h2(f)))
| one(X0) )
| ~ spl0_34 ),
inference(resolution,[],[f587,f4]) ).
fof(f591,plain,
( zero(outs(h1(f)))
| ~ spl0_26 ),
inference(resolution,[],[f573,f305]) ).
fof(f595,plain,
( one(outs(h1(f)))
| ~ spl0_34 ),
inference(resolution,[],[f588,f320]) ).
fof(f598,plain,
( ~ zero(outs(h1(f)))
| ~ spl0_34 ),
inference(resolution,[],[f595,f5]) ).
fof(f599,plain,
( $false
| ~ spl0_26
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f598,f591]) ).
fof(f600,plain,
( ~ spl0_26
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f599]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f71]) ).
cnf(s2,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f76]) ).
cnf(s3,plain,
( ~ spl0_2
| ~ spl0_4 ),
inference(sat_conversion,[],[f81]) ).
cnf(s4,plain,
( ~ spl0_2
| ~ spl0_5 ),
inference(sat_conversion,[],[f86]) ).
cnf(s6,plain,
( spl0_4
| spl0_8 ),
inference(sat_conversion,[],[f119]) ).
cnf(s7,plain,
( spl0_5
| spl0_9 ),
inference(sat_conversion,[],[f135]) ).
cnf(s8,plain,
( spl0_1
| spl0_10 ),
inference(sat_conversion,[],[f144]) ).
cnf(s17,plain,
( spl0_3
| spl0_25 ),
inference(sat_conversion,[],[f224]) ).
cnf(s20,plain,
( ~ spl0_9
| spl0_26
| ~ spl0_28 ),
inference(sat_conversion,[],[f245]) ).
cnf(s30,plain,
( ~ spl0_14
| spl0_15
| ~ spl0_38 ),
inference(sat_conversion,[],[f332]) ).
cnf(s35,plain,
( ~ spl0_10
| ~ spl0_32
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f357]) ).
cnf(s37,plain,
spl0_22,
inference(sat_conversion,[],[f376]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_22
| spl0_39 ),
inference(sat_conversion,[],[f378]) ).
cnf(s40,plain,
( ~ spl0_8
| spl0_42
| ~ spl0_43 ),
inference(sat_conversion,[],[f411]) ).
cnf(s45,plain,
( ~ spl0_25
| spl0_47
| ~ spl0_48 ),
inference(sat_conversion,[],[f442]) ).
cnf(s49,plain,
spl0_35,
inference(sat_conversion,[],[f462]) ).
cnf(s50,plain,
spl0_14,
inference(sat_conversion,[],[f469]) ).
cnf(s51,plain,
spl0_38,
inference(sat_conversion,[],[f477]) ).
cnf(s52,plain,
spl0_48,
inference(sat_conversion,[],[f487]) ).
cnf(s55,plain,
( spl0_11
| ~ spl0_39 ),
inference(sat_conversion,[],[f504]) ).
cnf(s57,plain,
( ~ spl0_11
| ~ spl0_15 ),
inference(sat_conversion,[],[f508]) ).
cnf(s59,plain,
( ~ spl0_15
| spl0_43 ),
inference(sat_conversion,[],[f534]) ).
cnf(s60,plain,
( spl0_32
| ~ spl0_47 ),
inference(sat_conversion,[],[f558]) ).
cnf(s61,plain,
( ~ spl0_33
| ~ spl0_35 ),
inference(sat_conversion,[],[f566]) ).
cnf(s62,plain,
( spl0_28
| ~ spl0_42 ),
inference(sat_conversion,[],[f572]) ).
cnf(s63,plain,
( ~ spl0_26
| ~ spl0_34 ),
inference(sat_conversion,[],[f600]) ).
cnf(s65,plain,
~ spl0_33,
inference(rat,[],[s61,s49]) ).
cnf(s67,plain,
( ~ spl0_25
| spl0_47 ),
inference(rat,[],[s45,s52]) ).
cnf(s68,plain,
( ~ spl0_10
| ~ spl0_32
| spl0_34 ),
inference(rat,[],[s35,s65]) ).
cnf(s71,plain,
spl0_15,
inference(rat,[],[s30,s51,s50]) ).
cnf(s72,plain,
spl0_43,
inference(rat,[],[s59,s71]) ).
cnf(s74,plain,
~ spl0_11,
inference(rat,[],[s57,s71]) ).
cnf(s75,plain,
~ spl0_39,
inference(rat,[],[s55,s74]) ).
cnf(s76,plain,
spl0_2,
inference(rat,[],[s38,s37,s75]) ).
cnf(s78,plain,
~ spl0_5,
inference(rat,[],[s4,s76]) ).
cnf(s79,plain,
spl0_9,
inference(rat,[],[s7,s78]) ).
cnf(s80,plain,
~ spl0_4,
inference(rat,[],[s3,s76]) ).
cnf(s81,plain,
spl0_8,
inference(rat,[],[s6,s80]) ).
cnf(s82,plain,
spl0_42,
inference(rat,[],[s40,s72,s81]) ).
cnf(s83,plain,
spl0_28,
inference(rat,[],[s62,s82]) ).
cnf(s84,plain,
spl0_26,
inference(rat,[],[s20,s79,s83]) ).
cnf(s85,plain,
~ spl0_34,
inference(rat,[],[s63,s84]) ).
cnf(s86,plain,
~ spl0_3,
inference(rat,[],[s2,s76]) ).
cnf(s87,plain,
spl0_25,
inference(rat,[],[s17,s86]) ).
cnf(s89,plain,
spl0_47,
inference(rat,[],[s67,s87]) ).
cnf(s90,plain,
spl0_32,
inference(rat,[],[s60,s89]) ).
cnf(s91,plain,
~ spl0_10,
inference(rat,[],[s68,s85,s90]) ).
cnf(s92,plain,
spl0_1,
inference(rat,[],[s8,s91]) ).
cnf(s93,plain,
$false,
inference(rat,[],[s1,s76,s92]) ).
fof(f601,plain,
$false,
inference(avatar_sat_refutation,[],[s93]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV007-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n011.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 10:53:00 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 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.17/0.48 % (2220654)Will run a generic schedule for satisfiability detection.
% 0.17/0.48 % (2220660)% WARNING: option uhcvi not known.
% 0.17/0.48 % (2220664)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2290265311:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.48 % (2220661)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=56465173:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.48 % (2220662)dis+10_1_sil=32000:sp=arity:random_seed=3173490876:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.48 % (2220660)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1688840598:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.48 % (2220659)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1477667793_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.48 % (2220663)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1922370068:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.48 % (2220665)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=601015422:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.48 % (2220664) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2220654-2220664"...
% 0.17/0.48 % TRYING [1]
% 0.17/0.48 % TRYING [2]
% 0.17/0.48 % (2220664)...printing done.
% 0.17/0.48 % (2220664)Refutation found. Thanks to Tanya!
% 0.17/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.17/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.48 % (2220664)------------------------------
% 0.17/0.48 % (2220664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.48 % (2220664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.48 % (2220664)CaDiCaL version: 2.1.3
% 0.17/0.48 % (2220664)Termination reason: Refutation
% 0.17/0.48 % (2220664)Time elapsed: 0.006 s
% 0.17/0.48 % (2220664)Peak memory usage: 12 MB
% 0.17/0.48 % (2220664)Instructions burned: 14 (million)
% 0.17/0.48 % (2220654)Success in time 0.046 s
% 0.17/0.48 % Vampire exiting
%------------------------------------------------------------------------------