%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 11:41:47 AM UTC 2026
% Result : Theorem 2.14s 1.30s
% Output : Refutation 2.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 52
% Syntax : Number of formulae : 252 ( 70 unt; 24 def)
% Number of atoms : 800 ( 0 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 923 ( 375 ~; 384 |; 120 &)
% ( 40 <=>; 3 =>; 0 <=; 1 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 48 ( 47 usr; 25 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-1 aty)
% Number of variables : 143 ( 0 sgn 114 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f3,axiom,
! [X0] :
( cC10(X0)
<=> ( cC4(X0)
& cC8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f6,axiom,
! [X0] :
( cC14(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(f14,axiom,
! [X0] :
( cC20(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(f30,axiom,
! [X0] :
( cC34(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC32xcomp(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f36,axiom,
! [X0] :
( cC4(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_35) ).
fof(f45,axiom,
! [X0] :
( cC48(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
fof(f58,axiom,
! [X0] :
( cC58(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_57) ).
fof(f62,axiom,
! [X0] :
( cC60(X0)
<=> ( cC2xcomp(X0)
& cC58(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_61) ).
fof(f63,axiom,
! [X0] :
( cC62(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC60(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_62) ).
fof(f80,axiom,
! [X0] :
( cC8(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC6xcomp(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_79) ).
fof(f81,axiom,
! [X0] :
( cC80(X0)
<=> ( cC78xcomp(X0)
& cC2xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_80) ).
fof(f83,axiom,
! [X0] :
( cC82(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC80(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_82) ).
fof(f104,axiom,
rR1(iV8467,iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_103) ).
fof(f105,axiom,
rR1(iV8467,iV8470),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_104) ).
fof(f106,axiom,
rR1(iV8467,iV8469),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_105) ).
fof(f107,axiom,
rR1(iV8467,iV8474),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_106) ).
fof(f111,axiom,
rR1(iV8467,iV8472),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
fof(f114,axiom,
cC6xcomp(iV8469),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_113) ).
fof(f117,axiom,
cTOP(iV8470),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_116) ).
fof(f119,axiom,
cC78xcomp(iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_118) ).
fof(f120,axiom,
cC2xcomp(iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_119) ).
fof(f123,axiom,
cC2xcomp(iV8472),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_122) ).
fof(f125,axiom,
rR1(iV8472,iV8476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_124) ).
fof(f128,axiom,
cC32xcomp(iV8474),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_127) ).
fof(f133,axiom,
cC2(iV8476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_132) ).
fof(f135,conjecture,
( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f136,negated_conjecture,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
inference(negated_conjecture,[status(cth)],[f135]) ).
fof(f137,plain,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
inference(rectify,[],[f136]) ).
fof(f138,plain,
! [X0] :
( ( cC4(X0)
& cC8(X0) )
=> cC10(X0) ),
inference(unused_predicate_definition_removal,[],[f3]) ).
fof(f139,plain,
! [X0] :
( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
=> cC4(X0) ),
inference(unused_predicate_definition_removal,[],[f36]) ).
fof(f140,plain,
! [X0] :
( ? [X1] :
( rR1(X0,X1)
& cC6xcomp(X1) )
=> cC8(X0) ),
inference(unused_predicate_definition_removal,[],[f80]) ).
fof(f146,plain,
! [X0] :
( cC10(X0)
| ~ cC4(X0)
| ~ cC8(X0) ),
inference(ennf_transformation,[],[f138]) ).
fof(f147,plain,
! [X0] :
( cC10(X0)
| ~ cC4(X0)
| ~ cC8(X0) ),
inference(flattening,[],[f146]) ).
fof(f155,plain,
! [X0] :
( cC4(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) ),
inference(ennf_transformation,[],[f139]) ).
fof(f166,plain,
! [X0] :
( cC8(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC6xcomp(X1) ) ),
inference(ennf_transformation,[],[f140]) ).
fof(f174,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(ennf_transformation,[],[f137]) ).
fof(f175,plain,
! [X0] :
( ( xsd_string(X0)
| xsd_integer(X0) )
& ( ~ xsd_integer(X0)
| ~ xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f179,plain,
! [X0] :
( ( cC14(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cTOP(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cTOP(X1) )
| ~ cC14(X0) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f180,plain,
! [X0] :
( ( cC14(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cTOP(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cTOP(X2) )
| ~ cC14(X0) ) ),
inference(rectify,[],[f179]) ).
fof(f181,plain,
! [X0] :
( ( cC14(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cTOP(X1) ) )
& ( ( rR1(X0,sK1(X0))
& cTOP(sK1(X0)) )
| ~ cC14(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0))],[f180]) ).
fof(f197,plain,
! [X0] :
( ( cC20(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
| ~ cC20(X0) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f198,plain,
! [X0] :
( ( cC20(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2xcomp(X2) )
| ~ cC20(X0) ) ),
inference(rectify,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ( cC20(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ( rR1(X0,sK7(X0))
& cC2xcomp(sK7(X0)) )
| ~ cC20(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0))],[f198]) ).
fof(f235,plain,
! [X0] :
( ( cC34(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC32xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC32xcomp(X1) )
| ~ cC34(X0) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f236,plain,
! [X0] :
( ( cC34(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC32xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC32xcomp(X2) )
| ~ cC34(X0) ) ),
inference(rectify,[],[f235]) ).
fof(f237,plain,
! [X0] :
( ( cC34(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC32xcomp(X1) ) )
& ( ( rR1(X0,sK19(X0))
& cC32xcomp(sK19(X0)) )
| ~ cC34(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X2,sK19(X0))],[f236]) ).
fof(f268,plain,
! [X0] :
( ( cC48(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
| ~ cC48(X0) ) ),
inference(nnf_transformation,[],[f45]) ).
fof(f269,plain,
! [X0] :
( ( cC48(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2xcomp(X2) )
| ~ cC48(X0) ) ),
inference(rectify,[],[f268]) ).
fof(f270,plain,
! [X0] :
( ( cC48(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ( rR1(X0,sK30(X0))
& cC2xcomp(sK30(X0)) )
| ~ cC48(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(X2,sK30(X0))],[f269]) ).
fof(f297,plain,
! [X0] :
( ( cC58(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2(X1) )
| ~ cC58(X0) ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f298,plain,
! [X0] :
( ( cC58(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2(X2) )
| ~ cC58(X0) ) ),
inference(rectify,[],[f297]) ).
fof(f299,plain,
! [X0] :
( ( cC58(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2(X1) ) )
& ( ( rR1(X0,sK39(X0))
& cC2(sK39(X0)) )
| ~ cC58(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X2,sK39(X0))],[f298]) ).
fof(f309,plain,
! [X0] :
( ( cC60(X0)
| ~ cC2xcomp(X0)
| ~ cC58(X0) )
& ( ( cC2xcomp(X0)
& cC58(X0) )
| ~ cC60(X0) ) ),
inference(nnf_transformation,[],[f62]) ).
fof(f310,plain,
! [X0] :
( ( cC60(X0)
| ~ cC2xcomp(X0)
| ~ cC58(X0) )
& ( ( cC2xcomp(X0)
& cC58(X0) )
| ~ cC60(X0) ) ),
inference(flattening,[],[f309]) ).
fof(f311,plain,
! [X0] :
( ( cC62(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC60(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC60(X1) )
| ~ cC62(X0) ) ),
inference(nnf_transformation,[],[f63]) ).
fof(f312,plain,
! [X0] :
( ( cC62(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC60(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC60(X2) )
| ~ cC62(X0) ) ),
inference(rectify,[],[f311]) ).
fof(f313,plain,
! [X0] :
( ( cC62(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC60(X1) ) )
& ( ( rR1(X0,sK43(X0))
& cC60(sK43(X0)) )
| ~ cC62(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X2,sK43(X0))],[f312]) ).
fof(f351,plain,
! [X0] :
( ( cC80(X0)
| ~ cC78xcomp(X0)
| ~ cC2xcomp(X0) )
& ( ( cC78xcomp(X0)
& cC2xcomp(X0) )
| ~ cC80(X0) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f352,plain,
! [X0] :
( ( cC80(X0)
| ~ cC78xcomp(X0)
| ~ cC2xcomp(X0) )
& ( ( cC78xcomp(X0)
& cC2xcomp(X0) )
| ~ cC80(X0) ) ),
inference(flattening,[],[f351]) ).
fof(f356,plain,
! [X0] :
( ( cC82(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC80(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC80(X1) )
| ~ cC82(X0) ) ),
inference(nnf_transformation,[],[f83]) ).
fof(f357,plain,
! [X0] :
( ( cC82(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC80(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC80(X2) )
| ~ cC82(X0) ) ),
inference(rectify,[],[f356]) ).
fof(f358,plain,
! [X0] :
( ( cC82(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC80(X1) ) )
& ( ( rR1(X0,sK56(X0))
& cC80(sK56(X0)) )
| ~ cC82(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X2,sK56(X0))],[f357]) ).
fof(f391,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( ( xsd_integer(X1)
| ~ xsd_string(X1) )
& ( ~ xsd_integer(X1)
| xsd_string(X1) ) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(nnf_transformation,[],[f174]) ).
fof(f392,plain,
( ~ cowlThing(sK67)
| cowlNothing(sK67)
| ( ( xsd_integer(sK68)
| ~ xsd_string(sK68) )
& ( ~ xsd_integer(sK68)
| xsd_string(sK68) ) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67,sK68]),skolemize(X0,sK67),skolemize(X1,sK68)],[f391]) ).
fof(f393,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f394,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f395,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f396,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f397,plain,
! [X0] :
( cC10(X0)
| ~ cC4(X0)
| ~ cC8(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f402,plain,
! [X0,X1] :
( ~ cTOP(X1)
| ~ rR1(X0,X1)
| cC14(X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f416,plain,
! [X0,X1] :
( cC20(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f199]) ).
fof(f449,plain,
! [X0,X1] :
( ~ cC32xcomp(X1)
| ~ rR1(X0,X1)
| cC34(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f462,plain,
! [X0,X1] :
( cC4(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f155]) ).
fof(f479,plain,
! [X0,X1] :
( cC48(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f270]) ).
fof(f504,plain,
! [X0,X1] :
( cC58(X0)
| ~ rR1(X0,X1)
| ~ cC2(X1) ),
inference(cnf_transformation,[],[f299]) ).
fof(f514,plain,
! [X0] :
( cC60(X0)
| ~ cC2xcomp(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[],[f310]) ).
fof(f517,plain,
! [X0,X1] :
( cC62(X0)
| ~ rR1(X0,X1)
| ~ cC60(X1) ),
inference(cnf_transformation,[],[f313]) ).
fof(f552,plain,
! [X0,X1] :
( ~ cC6xcomp(X1)
| ~ rR1(X0,X1)
| cC8(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f555,plain,
! [X0] :
( ~ cC78xcomp(X0)
| cC80(X0)
| ~ cC2xcomp(X0) ),
inference(cnf_transformation,[],[f352]) ).
fof(f560,plain,
! [X0,X1] :
( cC82(X0)
| ~ rR1(X0,X1)
| ~ cC80(X1) ),
inference(cnf_transformation,[],[f358]) ).
fof(f596,plain,
rR1(iV8467,iV8471),
inference(cnf_transformation,[],[f104]) ).
fof(f597,plain,
rR1(iV8467,iV8470),
inference(cnf_transformation,[],[f105]) ).
fof(f598,plain,
rR1(iV8467,iV8469),
inference(cnf_transformation,[],[f106]) ).
fof(f599,plain,
rR1(iV8467,iV8474),
inference(cnf_transformation,[],[f107]) ).
fof(f603,plain,
rR1(iV8467,iV8472),
inference(cnf_transformation,[],[f111]) ).
fof(f606,plain,
cC6xcomp(iV8469),
inference(cnf_transformation,[],[f114]) ).
fof(f609,plain,
cTOP(iV8470),
inference(cnf_transformation,[],[f117]) ).
fof(f611,plain,
cC78xcomp(iV8471),
inference(cnf_transformation,[],[f119]) ).
fof(f612,plain,
cC2xcomp(iV8471),
inference(cnf_transformation,[],[f120]) ).
fof(f615,plain,
cC2xcomp(iV8472),
inference(cnf_transformation,[],[f123]) ).
fof(f617,plain,
rR1(iV8472,iV8476),
inference(cnf_transformation,[],[f125]) ).
fof(f620,plain,
cC32xcomp(iV8474),
inference(cnf_transformation,[],[f128]) ).
fof(f625,plain,
cC2(iV8476),
inference(cnf_transformation,[],[f133]) ).
fof(f627,plain,
( ~ cowlThing(sK67)
| cowlNothing(sK67)
| ~ xsd_integer(sK68)
| xsd_string(sK68)
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(cnf_transformation,[],[f392]) ).
fof(f628,plain,
( ~ cowlThing(sK67)
| cowlNothing(sK67)
| xsd_integer(sK68)
| ~ xsd_string(sK68)
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(cnf_transformation,[],[f392]) ).
fof(f630,definition,
( spl69_1
<=> cowlThing(iV8472) ),
introduced(definition,[new_symbols(definition,[spl69_1])],[avatar_definition]) ).
fof(f631,plain,
( ~ cowlThing(iV8472)
| spl69_1 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f633,definition,
( spl69_2
<=> cC60(iV8472) ),
introduced(definition,[new_symbols(definition,[spl69_2])],[avatar_definition]) ).
fof(f634,plain,
( ~ cC60(iV8472)
| spl69_2 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,definition,
( spl69_3
<=> cC58(iV8472) ),
introduced(definition,[new_symbols(definition,[spl69_3])],[avatar_definition]) ).
fof(f637,plain,
( ~ cC58(iV8472)
| spl69_3 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f639,definition,
( spl69_4
<=> cC80(iV8471) ),
introduced(definition,[new_symbols(definition,[spl69_4])],[avatar_definition]) ).
fof(f642,definition,
( spl69_5
<=> cowlThing(iV8471) ),
introduced(definition,[new_symbols(definition,[spl69_5])],[avatar_definition]) ).
fof(f643,plain,
( ~ cowlThing(iV8471)
| spl69_5 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f645,definition,
( spl69_6
<=> cC48(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_6])],[avatar_definition]) ).
fof(f646,plain,
( ~ cC48(iV8467)
| spl69_6 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f648,definition,
( spl69_7
<=> cowlThing(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_7])],[avatar_definition]) ).
fof(f649,plain,
( ~ cowlThing(iV8467)
| spl69_7 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,definition,
( spl69_8
<=> cC10(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_8])],[avatar_definition]) ).
fof(f652,plain,
( ~ cC10(iV8467)
| spl69_8 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f654,definition,
( spl69_9
<=> cC34(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_9])],[avatar_definition]) ).
fof(f655,plain,
( ~ cC34(iV8467)
| spl69_9 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f657,definition,
( spl69_10
<=> cC14(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_10])],[avatar_definition]) ).
fof(f658,plain,
( ~ cC14(iV8467)
| spl69_10 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f660,definition,
( spl69_11
<=> cC62(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_11])],[avatar_definition]) ).
fof(f661,plain,
( ~ cC62(iV8467)
| spl69_11 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,definition,
( spl69_12
<=> cC82(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_12])],[avatar_definition]) ).
fof(f664,plain,
( ~ cC82(iV8467)
| spl69_12 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f666,definition,
( spl69_13
<=> cC8(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_13])],[avatar_definition]) ).
fof(f667,plain,
( ~ cC8(iV8467)
| spl69_13 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f669,definition,
( spl69_14
<=> cC4(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_14])],[avatar_definition]) ).
fof(f670,plain,
( ~ cC4(iV8467)
| spl69_14 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,definition,
( spl69_15
<=> cC20(iV8467) ),
introduced(definition,[new_symbols(definition,[spl69_15])],[avatar_definition]) ).
fof(f673,plain,
( ~ cC20(iV8467)
| spl69_15 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,definition,
( spl69_16
<=> xsd_string(sK68) ),
introduced(definition,[new_symbols(definition,[spl69_16])],[avatar_definition]) ).
fof(f678,definition,
( spl69_17
<=> xsd_integer(sK68) ),
introduced(definition,[new_symbols(definition,[spl69_17])],[avatar_definition]) ).
fof(f679,plain,
( ~ xsd_integer(sK68)
| spl69_17 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,definition,
( spl69_18
<=> cowlNothing(sK67) ),
introduced(definition,[new_symbols(definition,[spl69_18])],[avatar_definition]) ).
fof(f682,plain,
( cowlNothing(sK67)
| ~ spl69_18 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,definition,
( spl69_19
<=> cowlThing(sK67) ),
introduced(definition,[new_symbols(definition,[spl69_19])],[avatar_definition]) ).
fof(f685,plain,
( ~ cowlThing(sK67)
| spl69_19 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f686,plain,
( ~ spl69_1
| ~ spl69_2
| ~ spl69_3
| ~ spl69_4
| ~ spl69_5
| ~ spl69_6
| ~ spl69_7
| ~ spl69_8
| ~ spl69_9
| ~ spl69_10
| ~ spl69_11
| ~ spl69_12
| ~ spl69_13
| ~ spl69_14
| ~ spl69_15
| spl69_16
| ~ spl69_17
| spl69_18
| ~ spl69_19 ),
inference(avatar_split_clause,[],[f627,f684,f681,f678,f675,f672,f669,f666,f663,f660,f657,f654,f651,f648,f645,f642,f639,f636,f633,f630]) ).
fof(f688,plain,
( xsd_integer(sK68)
| ~ spl69_17 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f689,plain,
( ~ spl69_1
| ~ spl69_2
| ~ spl69_3
| ~ spl69_4
| ~ spl69_5
| ~ spl69_6
| ~ spl69_7
| ~ spl69_8
| ~ spl69_9
| ~ spl69_10
| ~ spl69_11
| ~ spl69_12
| ~ spl69_13
| ~ spl69_14
| ~ spl69_15
| ~ spl69_16
| spl69_17
| spl69_18
| ~ spl69_19 ),
inference(avatar_split_clause,[],[f628,f684,f681,f678,f675,f672,f669,f666,f663,f660,f657,f654,f651,f648,f645,f642,f639,f636,f633,f630]) ).
fof(f690,plain,
( $false
| spl69_1 ),
inference(resolution,[],[f394,f631]) ).
fof(f691,plain,
spl69_1,
inference(avatar_contradiction_clause,[],[f690]) ).
fof(f778,plain,
( ~ cC2xcomp(iV8472)
| ~ cC58(iV8472)
| spl69_2 ),
inference(resolution,[],[f514,f634]) ).
fof(f782,definition,
( spl69_20
<=> cC2xcomp(iV8472) ),
introduced(definition,[new_symbols(definition,[spl69_20])],[avatar_definition]) ).
fof(f783,plain,
( ~ cC2xcomp(iV8472)
| spl69_20 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f784,plain,
( ~ spl69_3
| ~ spl69_20
| spl69_2 ),
inference(avatar_split_clause,[],[f778,f633,f782,f636]) ).
fof(f804,plain,
( cC80(iV8471)
| ~ cC2xcomp(iV8471) ),
inference(resolution,[],[f555,f611]) ).
fof(f807,definition,
( spl69_21
<=> cC2xcomp(iV8471) ),
introduced(definition,[new_symbols(definition,[spl69_21])],[avatar_definition]) ).
fof(f808,plain,
( ~ cC2xcomp(iV8471)
| spl69_21 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f809,plain,
( cC80(iV8471)
| ~ spl69_4 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f810,plain,
( ~ spl69_21
| spl69_4 ),
inference(avatar_split_clause,[],[f804,f639,f807]) ).
fof(f811,plain,
( $false
| spl69_21 ),
inference(resolution,[],[f808,f612]) ).
fof(f813,plain,
spl69_21,
inference(avatar_contradiction_clause,[],[f811]) ).
fof(f834,plain,
! [X0] :
( cC14(X0)
| ~ rR1(X0,iV8470) ),
inference(resolution,[],[f402,f609]) ).
fof(f857,plain,
! [X0] :
( cC34(X0)
| ~ rR1(X0,iV8474) ),
inference(resolution,[],[f449,f620]) ).
fof(f887,plain,
( ! [X0] :
( ~ cC2(X0)
| ~ rR1(iV8472,X0) )
| spl69_3 ),
inference(resolution,[],[f504,f637]) ).
fof(f888,plain,
( ~ rR1(iV8472,iV8476)
| spl69_3 ),
inference(resolution,[],[f887,f625]) ).
fof(f892,plain,
( $false
| spl69_3 ),
inference(resolution,[],[f888,f617]) ).
fof(f893,plain,
spl69_3,
inference(avatar_contradiction_clause,[],[f892]) ).
fof(f894,plain,
( $false
| spl69_20 ),
inference(resolution,[],[f783,f615]) ).
fof(f896,plain,
spl69_20,
inference(avatar_contradiction_clause,[],[f894]) ).
fof(f897,plain,
( $false
| spl69_5 ),
inference(resolution,[],[f643,f394]) ).
fof(f898,plain,
spl69_5,
inference(avatar_contradiction_clause,[],[f897]) ).
fof(f899,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV8467,X0) )
| spl69_6 ),
inference(resolution,[],[f646,f479]) ).
fof(f901,plain,
( ~ rR1(iV8467,iV8471)
| spl69_6 ),
inference(resolution,[],[f899,f612]) ).
fof(f906,plain,
( $false
| spl69_6 ),
inference(resolution,[],[f901,f596]) ).
fof(f907,plain,
spl69_6,
inference(avatar_contradiction_clause,[],[f906]) ).
fof(f908,plain,
( $false
| spl69_7 ),
inference(resolution,[],[f649,f394]) ).
fof(f909,plain,
spl69_7,
inference(avatar_contradiction_clause,[],[f908]) ).
fof(f910,plain,
( ~ cC4(iV8467)
| ~ cC8(iV8467)
| spl69_8 ),
inference(resolution,[],[f652,f397]) ).
fof(f911,plain,
( ~ spl69_13
| ~ spl69_14
| spl69_8 ),
inference(avatar_split_clause,[],[f910,f651,f669,f666]) ).
fof(f932,plain,
! [X0] :
( cC8(X0)
| ~ rR1(X0,iV8469) ),
inference(resolution,[],[f552,f606]) ).
fof(f934,plain,
( ~ rR1(iV8467,iV8469)
| spl69_13 ),
inference(resolution,[],[f932,f667]) ).
fof(f935,plain,
( $false
| spl69_13 ),
inference(resolution,[],[f934,f598]) ).
fof(f936,plain,
spl69_13,
inference(avatar_contradiction_clause,[],[f935]) ).
fof(f937,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV8467,X0) )
| spl69_14 ),
inference(resolution,[],[f670,f462]) ).
fof(f939,plain,
( ~ rR1(iV8467,iV8471)
| spl69_14 ),
inference(resolution,[],[f937,f612]) ).
fof(f946,plain,
( $false
| spl69_14 ),
inference(resolution,[],[f939,f596]) ).
fof(f947,plain,
spl69_14,
inference(avatar_contradiction_clause,[],[f946]) ).
fof(f948,plain,
( ~ rR1(iV8467,iV8474)
| spl69_9 ),
inference(resolution,[],[f655,f857]) ).
fof(f949,plain,
( $false
| spl69_9 ),
inference(resolution,[],[f948,f599]) ).
fof(f950,plain,
spl69_9,
inference(avatar_contradiction_clause,[],[f949]) ).
fof(f951,plain,
( ~ rR1(iV8467,iV8470)
| spl69_10 ),
inference(resolution,[],[f658,f834]) ).
fof(f952,plain,
( $false
| spl69_10 ),
inference(resolution,[],[f951,f597]) ).
fof(f953,plain,
spl69_10,
inference(avatar_contradiction_clause,[],[f952]) ).
fof(f954,plain,
( ! [X0] :
( ~ cC60(X0)
| ~ rR1(iV8467,X0) )
| spl69_11 ),
inference(resolution,[],[f661,f517]) ).
fof(f955,plain,
( ! [X0] :
( ~ cC58(X0)
| ~ cC2xcomp(X0)
| ~ rR1(iV8467,X0) )
| spl69_11 ),
inference(resolution,[],[f954,f514]) ).
fof(f956,plain,
( ! [X0,X1] :
( ~ cC2(X1)
| ~ rR1(iV8467,X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X0) )
| spl69_11 ),
inference(resolution,[],[f955,f504]) ).
fof(f957,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(X0,iV8476)
| ~ rR1(iV8467,X0) )
| spl69_11 ),
inference(resolution,[],[f956,f625]) ).
fof(f966,plain,
( ~ rR1(iV8472,iV8476)
| ~ rR1(iV8467,iV8472)
| spl69_11 ),
inference(resolution,[],[f957,f615]) ).
fof(f968,definition,
( spl69_22
<=> rR1(iV8467,iV8472) ),
introduced(definition,[new_symbols(definition,[spl69_22])],[avatar_definition]) ).
fof(f969,plain,
( ~ rR1(iV8467,iV8472)
| spl69_22 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f971,definition,
( spl69_23
<=> rR1(iV8472,iV8476) ),
introduced(definition,[new_symbols(definition,[spl69_23])],[avatar_definition]) ).
fof(f972,plain,
( ~ rR1(iV8472,iV8476)
| spl69_23 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f973,plain,
( ~ spl69_22
| ~ spl69_23
| spl69_11 ),
inference(avatar_split_clause,[],[f966,f660,f971,f968]) ).
fof(f996,definition,
( spl69_30
<=> rR1(iV8467,iV8471) ),
introduced(definition,[new_symbols(definition,[spl69_30])],[avatar_definition]) ).
fof(f997,plain,
( ~ rR1(iV8467,iV8471)
| spl69_30 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f1002,plain,
( $false
| spl69_22 ),
inference(resolution,[],[f969,f603]) ).
fof(f1003,plain,
spl69_22,
inference(avatar_contradiction_clause,[],[f1002]) ).
fof(f1008,plain,
( $false
| spl69_23 ),
inference(resolution,[],[f972,f617]) ).
fof(f1009,plain,
spl69_23,
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1010,plain,
( ! [X0] :
( ~ cC80(X0)
| ~ rR1(iV8467,X0) )
| spl69_12 ),
inference(resolution,[],[f664,f560]) ).
fof(f1011,plain,
( ~ rR1(iV8467,iV8471)
| ~ spl69_4
| spl69_12 ),
inference(resolution,[],[f1010,f809]) ).
fof(f1012,plain,
( ~ spl69_30
| ~ spl69_4
| spl69_12 ),
inference(avatar_split_clause,[],[f1011,f663,f639,f996]) ).
fof(f1015,plain,
( $false
| spl69_30 ),
inference(resolution,[],[f997,f596]) ).
fof(f1016,plain,
spl69_30,
inference(avatar_contradiction_clause,[],[f1015]) ).
fof(f1017,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV8467,X0) )
| spl69_15 ),
inference(resolution,[],[f673,f416]) ).
fof(f1019,plain,
( ~ rR1(iV8467,iV8471)
| spl69_15 ),
inference(resolution,[],[f1017,f612]) ).
fof(f1028,plain,
( ~ spl69_30
| spl69_15 ),
inference(avatar_split_clause,[],[f1019,f672,f996]) ).
fof(f1029,plain,
( $false
| spl69_19 ),
inference(resolution,[],[f685,f394]) ).
fof(f1030,plain,
spl69_19,
inference(avatar_contradiction_clause,[],[f1029]) ).
fof(f1031,plain,
( xsd_string(sK68)
| spl69_17 ),
inference(resolution,[],[f679,f396]) ).
fof(f1032,plain,
( spl69_16
| spl69_17 ),
inference(avatar_split_clause,[],[f1031,f678,f675]) ).
fof(f1033,plain,
( ~ xsd_string(sK68)
| ~ spl69_17 ),
inference(resolution,[],[f688,f395]) ).
fof(f1034,plain,
( ~ spl69_16
| ~ spl69_17 ),
inference(avatar_split_clause,[],[f1033,f678,f675]) ).
fof(f1036,plain,
( $false
| ~ spl69_18 ),
inference(resolution,[],[f682,f393]) ).
fof(f1037,plain,
~ spl69_18,
inference(avatar_contradiction_clause,[],[f1036]) ).
cnf(s1,plain,
( ~ spl69_1
| ~ spl69_2
| ~ spl69_3
| ~ spl69_4
| ~ spl69_5
| ~ spl69_6
| ~ spl69_7
| ~ spl69_8
| ~ spl69_9
| ~ spl69_10
| ~ spl69_11
| ~ spl69_12
| ~ spl69_13
| ~ spl69_14
| ~ spl69_15
| spl69_16
| ~ spl69_17
| spl69_18
| ~ spl69_19 ),
inference(sat_conversion,[],[f686]) ).
cnf(s2,plain,
( ~ spl69_1
| ~ spl69_2
| ~ spl69_3
| ~ spl69_4
| ~ spl69_5
| ~ spl69_6
| ~ spl69_7
| ~ spl69_8
| ~ spl69_9
| ~ spl69_10
| ~ spl69_11
| ~ spl69_12
| ~ spl69_13
| ~ spl69_14
| ~ spl69_15
| ~ spl69_16
| spl69_17
| spl69_18
| ~ spl69_19 ),
inference(sat_conversion,[],[f689]) ).
cnf(s3,plain,
spl69_1,
inference(sat_conversion,[],[f691]) ).
cnf(s4,plain,
( spl69_2
| ~ spl69_3
| ~ spl69_20 ),
inference(sat_conversion,[],[f784]) ).
cnf(s5,plain,
( spl69_4
| ~ spl69_21 ),
inference(sat_conversion,[],[f810]) ).
cnf(s6,plain,
spl69_21,
inference(sat_conversion,[],[f813]) ).
cnf(s7,plain,
spl69_3,
inference(sat_conversion,[],[f893]) ).
cnf(s8,plain,
spl69_20,
inference(sat_conversion,[],[f896]) ).
cnf(s9,plain,
spl69_5,
inference(sat_conversion,[],[f898]) ).
cnf(s10,plain,
spl69_6,
inference(sat_conversion,[],[f907]) ).
cnf(s11,plain,
spl69_7,
inference(sat_conversion,[],[f909]) ).
cnf(s12,plain,
( spl69_8
| ~ spl69_13
| ~ spl69_14 ),
inference(sat_conversion,[],[f911]) ).
cnf(s13,plain,
spl69_13,
inference(sat_conversion,[],[f936]) ).
cnf(s14,plain,
spl69_14,
inference(sat_conversion,[],[f947]) ).
cnf(s15,plain,
spl69_9,
inference(sat_conversion,[],[f950]) ).
cnf(s16,plain,
spl69_10,
inference(sat_conversion,[],[f953]) ).
cnf(s17,plain,
( spl69_11
| ~ spl69_22
| ~ spl69_23 ),
inference(sat_conversion,[],[f973]) ).
cnf(s22,plain,
spl69_22,
inference(sat_conversion,[],[f1003]) ).
cnf(s23,plain,
spl69_23,
inference(sat_conversion,[],[f1009]) ).
cnf(s24,plain,
( ~ spl69_4
| spl69_12
| ~ spl69_30 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s26,plain,
spl69_30,
inference(sat_conversion,[],[f1016]) ).
cnf(s31,plain,
( spl69_15
| ~ spl69_30 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s32,plain,
spl69_19,
inference(sat_conversion,[],[f1030]) ).
cnf(s33,plain,
( spl69_16
| spl69_17 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s34,plain,
( ~ spl69_16
| ~ spl69_17 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s35,plain,
~ spl69_18,
inference(sat_conversion,[],[f1037]) ).
cnf(s36,plain,
spl69_15,
inference(rat,[],[s31,s26]) ).
cnf(s37,plain,
( ~ spl69_4
| spl69_12 ),
inference(rat,[],[s24,s26]) ).
cnf(s40,plain,
spl69_11,
inference(rat,[],[s17,s23,s22]) ).
cnf(s41,plain,
spl69_8,
inference(rat,[],[s12,s14,s13]) ).
cnf(s42,plain,
spl69_4,
inference(rat,[],[s5,s6]) ).
cnf(s43,plain,
spl69_12,
inference(rat,[],[s37,s42]) ).
cnf(s44,plain,
spl69_2,
inference(rat,[],[s4,s8,s7]) ).
cnf(s45,plain,
( ~ spl69_16
| spl69_17 ),
inference(rat,[],[s2,s32,s35,s36,s14,s13,s43,s40,s16,s15,s41,s11,s10,s9,s42,s7,s44,s3]) ).
cnf(s46,plain,
( spl69_16
| ~ spl69_17 ),
inference(rat,[],[s1,s32,s35,s36,s14,s13,s43,s40,s16,s15,s41,s11,s10,s9,s42,s7,s44,s3]) ).
cnf(s47,plain,
spl69_16,
inference(rat,[],[s46,s33]) ).
cnf(s48,plain,
~ spl69_17,
inference(rat,[],[s34,s47]) ).
cnf(s49,plain,
$false,
inference(rat,[],[s45,s48,s47]) ).
fof(f1038,plain,
$false,
inference(avatar_sat_refutation,[],[s49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 13:32:15 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.14/1.30 % (970799)Detected formulas, will run a generic FOF schedule.
% 2.14/1.30 % (970808)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4050760114:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.14/1.30 % (970808)Refutation not found, incomplete strategy
% 2.14/1.30 % (970808)------------------------------
% 2.14/1.30 % (970808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/1.30 % (970808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/1.30 % (970808)CaDiCaL version: 2.1.3
% 2.14/1.30 % (970808)Termination reason: Refutation not found, incomplete strategy
% 2.14/1.30 % (970808)Time elapsed: 0.001 s
% 2.14/1.30 % (970808)Peak memory usage: 87 MB
% 2.14/1.30 % (970806)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1856352080:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.14/1.30 % (970810)dis-21_1_sil=8000:lcm=predicate:random_seed=3563957541:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.14/1.30 % (970805)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3182607865:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.14/1.30 % (970804)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1997741169:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.14/1.30 % (970807)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2991564327:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.14/1.30 % (970809)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3733399508:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.14/1.30 % (970807)Refutation not found, incomplete strategy
% 2.14/1.30 % (970807)------------------------------
% 2.14/1.30 % (970807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/1.30 % (970807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/1.30 % (970807)CaDiCaL version: 2.1.3
% 2.14/1.30 % (970807)Termination reason: Refutation not found, incomplete strategy
% 2.14/1.30 % (970807)Time elapsed: 0.001 s
% 2.14/1.30 % (970807)Peak memory usage: 87 MB
% 2.14/1.30 % (970810)First to succeed.
% 2.14/1.30 % (970810)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-970799"
% 2.14/1.30 % (970809)Also succeeded, but the first one will report.
% 2.14/1.30 % (970808)------------------------------
% 2.14/1.30 % (970808)------------------------------
% 2.14/1.30 % (970807)------------------------------
% 2.14/1.30 % (970807)------------------------------
% 2.14/1.30 % (970810)Refutation found. Thanks to Tanya!
% 2.14/1.30 % SZS status Theorem for theBenchmark
% 2.14/1.30 % SZS output start Proof for theBenchmark
% See solution above
% 2.14/1.40 % (970810)------------------------------
% 2.14/1.40 % (970810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/1.40 % (970810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/1.40 % (970810)CaDiCaL version: 2.1.3
% 2.14/1.40 % (970810)Termination reason: Refutation
% 2.14/1.40 % (970810)Time elapsed: 0.013 s
% 2.14/1.40 % (970810)Peak memory usage: 89 MB
% 2.14/1.40 % (970810)Instructions burned: 19 (million)
% 2.14/1.40 % (970810)------------------------------
% 2.14/1.40 % (970810)------------------------------
% 2.14/1.40 % (970799)Success in time 0.449 s
% 2.14/1.40 % Vampire exiting
%------------------------------------------------------------------------------