%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN784-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 02:01:59 PM UTC 2026
% Result : Unsatisfiable 7.61s 2.01s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 145
% Number of leaves : 37
% Syntax : Number of formulae : 429 ( 7 unt; 0 def)
% Number of atoms : 1901 ( 0 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 2423 ( 951 ~;1472 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 0 con; 1-1 aty)
% Number of variables : 642 ( 642 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : ssRr(skf3(X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
! [X0] : ssRr(X0,skf2(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f3,negated_conjecture,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ssPv4(X0)
| ssPv2(X1)
| ssPv3(X1)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f4,negated_conjecture,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv2(X0)
| ssPv2(X1)
| ssPv3(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f5,negated_conjecture,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv2(X0)
| ssPv2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f6,negated_conjecture,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X1)
| ssPv1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f7,negated_conjecture,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv3(X1)
| ssPv1(X0)
| ssPv1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f8,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssRr(X0,X1)
| ssPv4(X1)
| ssPv3(X2)
| ssPv3(X0)
| ssPv4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f9,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv2(X0)
| ssPv4(X2)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
fof(f10,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv3(X0)
| ssPv2(X2)
| ssPv3(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
fof(f13,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv4(X2)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
fof(f14,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv4(X2)
| ssPv4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
fof(f15,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv4(X2)
| ssPv3(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
fof(f16,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ssPv1(X2)
| ssPv3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
fof(f17,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv4(X2)
| ssPv3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
fof(f18,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv3(X2)
| ssPv2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
fof(f19,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ssPv2(X1)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
fof(f20,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv4(X2)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ssPv3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
fof(f21,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
fof(f22,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv3(X1)
| ssPv2(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
fof(f23,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
fof(f24,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(X2)
| ~ ssPv3(X0)
| ssPv4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
fof(f25,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1)
| ssPv1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
fof(f26,negated_conjecture,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1)
| ssPv1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
fof(f27,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ssPv4(X2)
| ssPv2(X3)
| ssPv3(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
fof(f28,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssRr(X0,X1)
| ~ ssRr(X1,X3)
| ~ ssPv4(X3)
| ssPv4(X0)
| ssPv3(X2)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
fof(f30,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X0,X3)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv3(X2)
| ssPv1(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
fof(f31,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssPv3(X0)
| ~ ssRr(X1,X2)
| ~ ssPv2(X2)
| ~ ssRr(X0,X1)
| ssPv4(X3)
| ssPv4(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
fof(f32,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssRr(X1,X3)
| ~ ssPv3(X3)
| ssPv4(X2)
| ssPv3(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f34,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssPv2(X0)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv4(X2)
| ssPv3(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X3,X1)
| ~ ssPv4(X0)
| ~ ssRr(X2,X1)
| ~ ssPv2(X2)
| ~ ssRr(X0,X1)
| ssPv1(X3)
| ssPv2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssPv4(X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X3)
| ssPv4(X0)
| ssPv2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssPv2(X0)
| ~ ssRr(X1,X2)
| ~ ssPv4(X2)
| ~ ssRr(X0,X1)
| ssPv3(X3)
| ssPv2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssPv1(X0)
| ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv2(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssPv4(X2)
| ~ ssRr(X0,X1)
| ~ ssPv2(X3)
| ~ ssPv1(X1)
| ssPv4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f41,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X1,X3)
| ~ ssPv2(X0)
| ~ ssRr(X1,X2)
| ~ ssPv2(X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X3)
| ~ ssPv1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X3)
| ~ ssPv1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ ssPv2(skf3(X1))
| ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv1(X1) ),
inference(resolution,[],[f42,f1]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X1),X2)
| ~ ssPv2(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1)) ),
inference(resolution,[],[f41,f1]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ ssPv1(skf2(X1))
| ~ ssRr(X1,X2)
| ~ ssPv2(X2)
| ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv1(X1) ),
inference(resolution,[],[f41,f2]) ).
fof(f49,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[],[f7,f1]) ).
fof(f53,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv1(skf3(X0)) ),
inference(resolution,[],[f6,f1]) ).
fof(f54,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f6,f2]) ).
fof(f57,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f4,f1]) ).
fof(f58,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f4,f2]) ).
fof(f60,plain,
! [X0,X1] :
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ssPv1(X1) ),
inference(resolution,[],[f26,f2]) ).
fof(f62,plain,
! [X0,X1] :
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ~ ssPv3(X1)
| ssPv1(X1) ),
inference(resolution,[],[f25,f2]) ).
fof(f63,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X0)
| ~ ssPv1(skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv1(X1) ),
inference(resolution,[],[f23,f1]) ).
fof(f64,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv1(skf2(X1)) ),
inference(resolution,[],[f23,f2]) ).
fof(f65,plain,
! [X0,X1] :
( ~ ssRr(skf3(X0),X1)
| ssPv4(X1)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f8,f1]) ).
fof(f66,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ssPv4(X1)
| ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[],[f8,f2]) ).
fof(f67,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv3(skf3(X1))
| ssPv4(skf3(X1)) ),
inference(resolution,[],[f24,f1]) ).
fof(f69,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ~ ssPv2(skf3(X1))
| ~ ssPv3(skf3(X1))
| ssPv2(X1) ),
inference(resolution,[],[f22,f1]) ).
fof(f70,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv3(X1)
| ssPv2(skf2(X1)) ),
inference(resolution,[],[f22,f2]) ).
fof(f71,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv3(X0)
| ssPv2(skf3(X1))
| ssPv3(X1) ),
inference(resolution,[],[f10,f1]) ).
fof(f72,plain,
! [X0,X1] :
( ~ ssRr(X0,skf2(X1))
| ~ ssPv2(skf2(X1))
| ssPv3(X0)
| ssPv2(X1)
| ssPv3(skf2(X1)) ),
inference(resolution,[],[f10,f2]) ).
fof(f73,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv4(X1) ),
inference(resolution,[],[f21,f1]) ).
fof(f74,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ssPv4(skf2(X1)) ),
inference(resolution,[],[f21,f2]) ).
fof(f75,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[],[f5,f1]) ).
fof(f78,plain,
! [X0,X1] :
( ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ssPv3(X0) ),
inference(resolution,[],[f20,f2]) ).
fof(f80,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,skf2(X2))
| ~ ssPv4(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,skf2(X2))
| ssPv1(X2)
| ssPv2(skf2(X2)) ),
inference(resolution,[],[f35,f2]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X0),X1)
| ~ ssPv4(X1)
| ~ ssRr(X2,skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ssPv4(X2) ),
inference(resolution,[],[f39,f1]) ).
fof(f82,plain,
! [X2,X0,X1] :
( ~ ssPv2(skf2(X0))
| ~ ssPv4(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv4(X2) ),
inference(resolution,[],[f39,f2]) ).
fof(f86,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv2(X0)
| ssPv4(skf2(X1))
| ssPv4(X1) ),
inference(resolution,[],[f9,f2]) ).
fof(f87,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X0)
| ~ ssRr(skf3(X1),X0)
| ~ ssPv4(skf3(X1))
| ssPv3(X2)
| ssPv1(X1) ),
inference(resolution,[],[f30,f1]) ).
fof(f89,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X1),X2)
| ~ ssPv2(X0)
| ~ ssPv4(X2)
| ~ ssRr(X0,skf3(X1))
| ssPv3(X1)
| ssPv2(skf3(X1)) ),
inference(resolution,[],[f37,f1]) ).
fof(f91,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv3(X2)
| ssPv4(skf3(X1))
| ssPv3(X1) ),
inference(resolution,[],[f32,f1]) ).
fof(f94,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssPv3(X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv2(skf2(X1)) ),
inference(resolution,[],[f38,f2]) ).
fof(f95,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,skf3(X1))
| ssPv4(X1)
| ssPv4(skf3(X1)) ),
inference(resolution,[],[f31,f1]) ).
fof(f96,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,X1)
| ssPv4(skf2(X1))
| ssPv4(X1) ),
inference(resolution,[],[f31,f2]) ).
fof(f98,plain,
! [X2,X0,X1] :
( ~ ssPv3(skf2(X0))
| ~ ssPv4(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ssPv4(X2)
| ssPv2(X0) ),
inference(resolution,[],[f36,f2]) ).
fof(f99,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X1),X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv4(X2)
| ssPv3(X1) ),
inference(resolution,[],[f34,f1]) ).
fof(f100,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv4(X2)
| ssPv3(skf2(X1)) ),
inference(resolution,[],[f34,f2]) ).
fof(f101,plain,
! [X2,X0,X1] :
( ~ ssRr(skf3(X0),X1)
| ~ ssRr(X2,skf3(X0))
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f27,f1]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f27,f2]) ).
fof(f103,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv4(X0)
| ~ ssPv2(skf3(X1))
| ssPv1(X1)
| ssPv3(skf3(X1)) ),
inference(resolution,[],[f16,f1]) ).
fof(f104,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv4(X0)
| ~ ssPv2(X1)
| ssPv1(skf2(X1))
| ssPv3(X1) ),
inference(resolution,[],[f16,f2]) ).
fof(f106,plain,
! [X0,X1] :
( ~ ssRr(X0,skf2(X1))
| ~ ssPv1(X0)
| ~ ssPv4(skf2(X1))
| ssPv3(X1)
| ssPv2(skf2(X1)) ),
inference(resolution,[],[f18,f2]) ).
fof(f107,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ssPv4(skf3(X1))
| ssPv3(X1) ),
inference(resolution,[],[f15,f1]) ).
fof(f108,plain,
! [X0,X1] :
( ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv4(skf2(X1))
| ssPv4(X1)
| ssPv3(skf2(X1)) ),
inference(resolution,[],[f15,f2]) ).
fof(f110,plain,
! [X0,X1] :
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv2(X1)
| ssPv4(X1) ),
inference(resolution,[],[f19,f2]) ).
fof(f112,plain,
! [X0,X1] :
( ~ ssRr(X0,skf2(X1))
| ~ ssPv4(X0)
| ~ ssPv2(skf2(X1))
| ssPv4(X1)
| ssPv4(skf2(X1)) ),
inference(resolution,[],[f13,f2]) ).
fof(f113,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X1))
| ssPv4(X1)
| ssPv3(skf3(X1)) ),
inference(resolution,[],[f17,f1]) ).
fof(f114,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ssPv4(skf2(X1))
| ssPv3(X1) ),
inference(resolution,[],[f17,f2]) ).
fof(f117,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X1))
| ssPv4(X1)
| ssPv4(skf3(X1)) ),
inference(resolution,[],[f14,f1]) ).
fof(f118,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ssPv4(skf2(X1))
| ssPv4(X1) ),
inference(resolution,[],[f14,f2]) ).
fof(f122,plain,
! [X2,X0,X1] :
( ~ ssRr(skf2(X1),X2)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv4(X2)
| ssPv4(X0)
| ssPv3(X1)
| ssPv4(skf2(X1)) ),
inference(resolution,[],[f28,f2]) ).
fof(f125,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(X1)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1)) ),
inference(resolution,[],[f45,f1]) ).
fof(f127,plain,
! [X0] :
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[],[f125,f1]) ).
fof(f129,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f74,f2]) ).
fof(f131,plain,
! [X0,X1] :
( ~ ssPv2(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ssPv4(skf2(X1))
| ssPv4(X1) ),
inference(resolution,[],[f96,f2]) ).
fof(f134,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f70,f1]) ).
fof(f139,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ssPv4(skf2(X1))
| ssPv3(skf2(X1)) ),
inference(resolution,[],[f100,f2]) ).
fof(f141,plain,
! [X0,X1] :
( ~ ssPv3(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ssPv4(skf3(X1))
| ssPv3(X1) ),
inference(resolution,[],[f91,f2]) ).
fof(f146,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf2(X0)) ),
inference(resolution,[],[f64,f1]) ).
fof(f149,plain,
! [X0,X1] :
( ~ ssPv3(skf2(X1))
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv2(skf2(X1)) ),
inference(resolution,[],[f94,f2]) ).
fof(f152,plain,
! [X0,X1] :
( ~ ssRr(skf3(X1),X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf3(X1))
| ssPv3(X1)
| ssPv1(X1) ),
inference(resolution,[],[f87,f1]) ).
fof(f155,plain,
! [X0] :
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f152,f2]) ).
fof(f157,plain,
! [X0] :
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ),
inference(resolution,[],[f73,f2]) ).
fof(f158,plain,
! [X0,X1] :
( ~ ssRr(X1,skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ssPv4(X1) ),
inference(resolution,[],[f81,f1]) ).
fof(f160,plain,
! [X0] :
( ssPv4(skf3(skf3(X0)))
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[],[f158,f1]) ).
fof(f161,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f107,f1]) ).
fof(f166,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[],[f118,f2]) ).
fof(f170,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(X0)
| ~ ssPv4(skf3(X1))
| ssPv4(X1)
| ssPv3(X1) ),
inference(resolution,[],[f99,f1]) ).
fof(f172,plain,
! [X0] :
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f170,f1]) ).
fof(f173,plain,
! [X0] :
( ssPv4(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f114,f1]) ).
fof(f174,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f114,f2]) ).
fof(f178,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f104,f2]) ).
fof(f183,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ssPv1(skf3(X0))
| ssPv4(X1)
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f102,f1]) ).
fof(f185,plain,
! [X0] :
( ~ ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0) ),
inference(resolution,[],[f63,f1]) ).
fof(f189,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[],[f86,f1]) ).
fof(f190,plain,
! [X0] :
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f86,f2]) ).
fof(f191,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(X1)
| ~ ssPv3(X0)
| ssPv4(X1)
| ssPv4(skf3(X1)) ),
inference(resolution,[],[f95,f1]) ).
fof(f193,plain,
! [X0] :
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f191,f1]) ).
fof(f196,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X1)
| ~ ssPv2(X0)
| ssPv3(X1)
| ssPv2(skf3(X1)) ),
inference(resolution,[],[f89,f1]) ).
fof(f198,plain,
! [X0] :
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf3(X0)) ),
inference(resolution,[],[f196,f1]) ).
fof(f200,plain,
! [X0] :
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(skf3(X0))
| ssPv2(X0) ),
inference(resolution,[],[f69,f1]) ).
fof(f201,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f71,f1]) ).
fof(f202,plain,
! [X0] :
( ssPv2(skf3(skf2(X0)))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f71,f2]) ).
fof(f206,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f67,f1]) ).
fof(f207,plain,
! [X0] :
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(skf3(X0))
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f67,f2]) ).
fof(f209,plain,
! [X0,X1] :
( ~ ssRr(X0,skf2(X1))
| ~ ssPv2(X1)
| ~ ssPv4(X0)
| ssPv1(X1)
| ssPv2(skf2(X1)) ),
inference(resolution,[],[f80,f2]) ).
fof(f210,plain,
! [X0] :
( ~ ssPv4(skf3(skf2(X0)))
| ~ ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f209,f1]) ).
fof(f211,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[],[f209,f2]) ).
fof(f212,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f211,f129]) ).
fof(f218,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f212]) ).
fof(f219,plain,
! [X0,X1] :
( ~ ssRr(X0,skf3(X1))
| ssPv1(X0)
| ssPv4(X1)
| ssPv2(X1)
| ssPv3(skf3(X1)) ),
inference(resolution,[],[f101,f1]) ).
fof(f221,plain,
! [X0] :
( ssPv1(skf3(skf3(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f219,f1]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2)
| ~ ssPv1(X0) ),
inference(resolution,[],[f75,f43]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ),
inference(duplicate_literal_removal,[],[f229]) ).
fof(f235,plain,
! [X2,X0,X1] :
( ~ ssRr(X1,X0)
| ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ),
inference(forward_subsumption_resolution,[],[f234,f19]) ).
fof(f236,plain,
! [X0,X1] :
( ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1) ),
inference(resolution,[],[f235,f1]) ).
fof(f246,plain,
! [X0,X1] :
( ~ ssPv4(skf2(skf2(X1)))
| ~ ssRr(X0,skf2(X1))
| ssPv4(X0)
| ssPv3(X1)
| ssPv4(skf2(X1)) ),
inference(resolution,[],[f122,f2]) ).
fof(f254,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[],[f66,f2]) ).
fof(f274,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f139,f1]) ).
fof(f279,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f183,f2]) ).
fof(f301,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf3(X0)) ),
inference(resolution,[],[f57,f198]) ).
fof(f302,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f57,f172]) ).
fof(f304,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f302]) ).
fof(f305,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f301]) ).
fof(f307,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f305,f304]) ).
fof(f358,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[],[f185,f160]) ).
fof(f360,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f358]) ).
fof(f372,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f218,f178]) ).
fof(f374,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X1) ),
inference(resolution,[],[f218,f78]) ).
fof(f377,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(X1) ),
inference(duplicate_literal_removal,[],[f374]) ).
fof(f378,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f372]) ).
fof(f379,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f378,f54]) ).
fof(f384,plain,
! [X0] :
( ~ ssPv4(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f112,f1]) ).
fof(f388,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f72,f2]) ).
fof(f412,plain,
! [X0] :
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f108,f1]) ).
fof(f427,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f103,f1]) ).
fof(f429,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f427,f201]) ).
fof(f430,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f427,f57]) ).
fof(f436,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f430]) ).
fof(f437,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f429]) ).
fof(f438,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f437,f436]) ).
fof(f451,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f377,f1]) ).
fof(f453,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f451,f438]) ).
fof(f455,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f453,f206]) ).
fof(f456,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f453,f161]) ).
fof(f458,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f456]) ).
fof(f459,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(duplicate_literal_removal,[],[f455]) ).
fof(f461,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f459,f458]) ).
fof(f479,plain,
! [X0] :
( ~ ssPv1(skf3(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f106,f1]) ).
fof(f480,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f106,f2]) ).
fof(f485,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f274,f57]) ).
fof(f492,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f485]) ).
fof(f493,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f492,f254]) ).
fof(f497,plain,
! [X0] :
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f117,f2]) ).
fof(f527,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f113,f1]) ).
fof(f528,plain,
! [X0] :
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv4(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f113,f2]) ).
fof(f530,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[],[f527,f49]) ).
fof(f531,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f530]) ).
fof(f532,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f531,f453]) ).
fof(f587,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f65,f1]) ).
fof(f659,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f438,f161]) ).
fof(f664,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f659]) ).
fof(f702,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[],[f53,f453]) ).
fof(f704,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f702]) ).
fof(f706,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f704,f360]) ).
fof(f708,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f706,f461]) ).
fof(f739,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssRr(X1,skf2(X0))
| ssPv4(X1)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f190,f246]) ).
fof(f749,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssRr(X1,skf2(X0))
| ssPv4(X1)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f739]) ).
fof(f750,plain,
! [X0,X1] :
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv4(X1)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f749,f493]) ).
fof(f781,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f750,f2]) ).
fof(f877,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(skf3(X0))
| ssPv2(skf2(skf3(X0))) ),
inference(resolution,[],[f173,f480]) ).
fof(f884,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv2(skf2(skf3(X0))) ),
inference(duplicate_literal_removal,[],[f877]) ).
fof(f983,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f58,f781]) ).
fof(f989,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f983]) ).
fof(f990,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f989,f388]) ).
fof(f995,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[],[f990,f110]) ).
fof(f1007,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1) ),
inference(duplicate_literal_removal,[],[f995]) ).
fof(f1009,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f1007,f3]) ).
fof(f1011,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[],[f1009,f1]) ).
fof(f1012,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f1009,f2]) ).
fof(f1030,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[],[f1011,f166]) ).
fof(f1031,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1011,f174]) ).
fof(f1041,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1031]) ).
fof(f1042,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f1030]) ).
fof(f1089,plain,
! [X0,X1] :
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f1042,f149]) ).
fof(f1099,plain,
! [X0,X1] :
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ssPv2(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1089]) ).
fof(f1103,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv1(X1)
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1099,f166]) ).
fof(f1105,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f1103,f1]) ).
fof(f1107,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1105,f279]) ).
fof(f1112,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1107]) ).
fof(f1115,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1112,f480]) ).
fof(f1121,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1115,f174]) ).
fof(f1136,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f1121]) ).
fof(f1145,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1136,f178]) ).
fof(f1158,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1145]) ).
fof(f1163,plain,
! [X0] :
( ssPv1(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1158,f1011]) ).
fof(f1280,plain,
! [X0,X1] :
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f1041,f149]) ).
fof(f1290,plain,
! [X0,X1] :
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ssPv2(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1280]) ).
fof(f1295,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1290,f480]) ).
fof(f1297,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f1295,f1]) ).
fof(f1299,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1297,f279]) ).
fof(f1302,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(skf2(skf3(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f1297,f221]) ).
fof(f1304,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(skf2(skf3(X0)))
| ssPv4(X0)
| ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f1302]) ).
fof(f1306,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1299]) ).
fof(f1307,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(skf2(skf3(X0)))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1304,f884]) ).
fof(f1308,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1306,f480]) ).
fof(f1309,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ssPv3(skf3(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1307,f528]) ).
fof(f1311,plain,
! [X2,X0,X1] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv4(X2) ),
inference(resolution,[],[f1308,f82]) ).
fof(f1315,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1308,f174]) ).
fof(f1316,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1308,f388]) ).
fof(f1328,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv2(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f1316]) ).
fof(f1329,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f1315]) ).
fof(f1331,plain,
! [X2,X0,X1] :
( ~ ssRr(X2,X0)
| ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ssPv4(X2) ),
inference(duplicate_literal_removal,[],[f1311]) ).
fof(f1336,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1329,f178]) ).
fof(f1347,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1336]) ).
fof(f1379,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f1331,f1]) ).
fof(f1382,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f1379,f2]) ).
fof(f1383,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f1382,f1329]) ).
fof(f1388,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf2(X0)) ),
inference(resolution,[],[f1383,f146]) ).
fof(f1389,plain,
! [X0,X1] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1) ),
inference(resolution,[],[f1383,f236]) ).
fof(f1394,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv3(X1) ),
inference(duplicate_literal_removal,[],[f1389]) ).
fof(f1395,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1388]) ).
fof(f1397,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1395,f1163]) ).
fof(f1401,plain,
! [X2,X0,X1] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssRr(X2,X0)
| ~ ssPv2(X2)
| ~ ssPv1(X0) ),
inference(resolution,[],[f1397,f46]) ).
fof(f1404,plain,
! [X2,X0,X1] :
( ~ ssRr(X2,X0)
| ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv1(X0)
| ~ ssPv2(X2) ),
inference(duplicate_literal_removal,[],[f1401]) ).
fof(f1415,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv3(skf2(X0)) ),
inference(resolution,[],[f1394,f2]) ).
fof(f1416,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1415,f1328]) ).
fof(f1431,plain,
! [X0,X1] :
( ~ ssPv2(skf3(X0))
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[],[f1404,f1]) ).
fof(f1432,plain,
! [X0,X1] :
( ~ ssRr(skf2(X0),X1)
| ssPv3(skf2(X0))
| ~ ssPv2(X1)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(X0) ),
inference(resolution,[],[f1404,f2]) ).
fof(f1433,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f1431,f201]) ).
fof(f1438,plain,
! [X0,X1] :
( ~ ssRr(skf2(X0),X1)
| ~ ssPv2(X1)
| ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1431,f202]) ).
fof(f1444,plain,
! [X0,X1] :
( ~ ssRr(skf2(X0),X1)
| ~ ssPv2(X1)
| ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1438]) ).
fof(f1448,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f1433]) ).
fof(f1450,plain,
! [X0,X1] :
( ~ ssRr(skf2(X0),X1)
| ~ ssPv2(X1)
| ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1444,f1416]) ).
fof(f1451,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f1448,f1416]) ).
fof(f1453,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f1451,f2]) ).
fof(f1454,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f1453,f1308]) ).
fof(f1540,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv2(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(X0) ),
inference(resolution,[],[f1432,f2]) ).
fof(f1541,plain,
! [X0] :
( ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f1540,f1308]) ).
fof(f1543,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f1541,f1347]) ).
fof(f1551,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1543]) ).
fof(f1553,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1551,f1328]) ).
fof(f1614,plain,
! [X0] :
( ~ ssPv2(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1450,f2]) ).
fof(f1615,plain,
! [X0] :
( ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1614,f1308]) ).
fof(f1619,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[],[f1615,f379]) ).
fof(f1627,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1619,f1553]) ).
fof(f1640,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f1627,f155]) ).
fof(f1641,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f1640]) ).
fof(f1645,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1641,f1454]) ).
fof(f1647,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1645,f307]) ).
fof(f1655,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f1647,f664]) ).
fof(f1664,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f1655]) ).
fof(f1669,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1664,f1454]) ).
fof(f1676,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1669,f161]) ).
fof(f1681,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1669,f412]) ).
fof(f1682,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f1681]) ).
fof(f1684,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1676]) ).
fof(f1707,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f1684,f210]) ).
fof(f1718,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(X0)
| ssPv2(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1707,f58]) ).
fof(f1719,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1718,f1012]) ).
fof(f1738,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1719,f388]) ).
fof(f1746,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f1738]) ).
fof(f1748,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f1746,f1328]) ).
fof(f1754,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1748,f141]) ).
fof(f1763,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv2(X0)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(duplicate_literal_removal,[],[f1754]) ).
fof(f1783,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f1763,f1]) ).
fof(f1791,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[],[f1783,f1669]) ).
fof(f1799,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f1791]) ).
fof(f1806,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f1799,f1011]) ).
fof(f1814,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1806,f1647]) ).
fof(f1823,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1814]) ).
fof(f1827,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv1(skf3(X0)) ),
inference(resolution,[],[f1823,f53]) ).
fof(f1835,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1823,f412]) ).
fof(f1836,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f1835]) ).
fof(f1840,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f1836,f1012]) ).
fof(f1842,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f1827,f1416]) ).
fof(f1843,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f1842,f1806]) ).
fof(f1855,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f1843,f479]) ).
fof(f1858,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1855]) ).
fof(f1863,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f1858,f1012]) ).
fof(f1881,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv4(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[],[f1863,f708]) ).
fof(f1886,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1881,f1615]) ).
fof(f1902,plain,
! [X0,X1] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[],[f1840,f131]) ).
fof(f1917,plain,
! [X0,X1] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f1902]) ).
fof(f1921,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ~ ssPv3(X1)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f1917,f1682]) ).
fof(f1943,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f1921,f1]) ).
fof(f1947,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f1943,f587]) ).
fof(f1958,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(duplicate_literal_removal,[],[f1947]) ).
fof(f1960,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f1958,f1684]) ).
fof(f1967,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1960,f141]) ).
fof(f1976,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f1967]) ).
fof(f1979,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f1976,f1]) ).
fof(f1983,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f1979,f587]) ).
fof(f2000,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f1983]) ).
fof(f2003,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2000,f1684]) ).
fof(f2004,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f2003,f384]) ).
fof(f2006,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f2003,f1647]) ).
fof(f2013,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f2006]) ).
fof(f2015,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2004,f1682]) ).
fof(f2016,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2015,f1840]) ).
fof(f2017,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv1(skf3(X0)) ),
inference(resolution,[],[f2013,f53]) ).
fof(f2035,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2017,f2003]) ).
fof(f2039,plain,
! [X2,X0,X1] :
( ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ssPv4(X2)
| ssPv2(X0) ),
inference(resolution,[],[f2016,f98]) ).
fof(f2040,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[],[f2016,f110]) ).
fof(f2046,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(skf3(X0))
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2016,f207]) ).
fof(f2049,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ),
inference(duplicate_literal_removal,[],[f2046]) ).
fof(f2050,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ~ ssPv4(X1)
| ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2040]) ).
fof(f2053,plain,
! [X2,X0,X1] :
( ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ssPv4(X0)
| ~ ssRr(X0,X1)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f2039,f2050]) ).
fof(f2055,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f2050,f2]) ).
fof(f2098,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv4(X1)
| ~ ssPv4(X0)
| ssPv2(X1) ),
inference(resolution,[],[f2053,f1]) ).
fof(f2100,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2098,f1]) ).
fof(f2101,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[],[f2098,f2]) ).
fof(f2118,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f2035,f527]) ).
fof(f2134,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f2118,f532]) ).
fof(f2136,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2134,f708]) ).
fof(f2145,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2136,f2049]) ).
fof(f2152,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2145]) ).
fof(f2230,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[],[f2055,f129]) ).
fof(f2246,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2230]) ).
fof(f2249,plain,
! [X0,X1] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X1) ),
inference(resolution,[],[f2246,f78]) ).
fof(f2254,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f2246,f480]) ).
fof(f2266,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv3(X1) ),
inference(duplicate_literal_removal,[],[f2249]) ).
fof(f2267,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f2254,f211]) ).
fof(f2268,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[],[f2266,f1]) ).
fof(f2269,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[],[f2266,f2]) ).
fof(f2270,plain,
! [X0] :
( ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2269,f1886]) ).
fof(f2271,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f2268,f1669]) ).
fof(f2273,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f2271,f134]) ).
fof(f2280,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2271,f2049]) ).
fof(f2288,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f2280]) ).
fof(f2292,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(duplicate_literal_removal,[],[f2273]) ).
fof(f2293,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2292,f2267]) ).
fof(f2303,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0) ),
inference(resolution,[],[f2288,f185]) ).
fof(f2304,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f2303]) ).
fof(f2307,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2304,f708]) ).
fof(f2320,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ),
inference(resolution,[],[f2293,f157]) ).
fof(f2323,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ),
inference(duplicate_literal_removal,[],[f2320]) ).
fof(f2363,plain,
! [X0] :
( ~ ssPv4(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[],[f2323,f202]) ).
fof(f2372,plain,
! [X0] :
( ~ ssPv4(skf3(skf2(X0)))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f2363,f2270]) ).
fof(f2373,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[],[f2372,f2003]) ).
fof(f2374,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2373,f1863]) ).
fof(f2415,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f2307,f57]) ).
fof(f2425,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2415,f708]) ).
fof(f2427,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2425,f1684]) ).
fof(f2492,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[],[f2270,f1308]) ).
fof(f2498,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[],[f2270,f2293]) ).
fof(f2504,plain,
! [X0] :
( ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f2492]) ).
fof(f2507,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2498,f2246]) ).
fof(f2508,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f2504,f1329]) ).
fof(f2515,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f2508,f54]) ).
fof(f2528,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2515,f2374]) ).
fof(f2529,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2528,f2016]) ).
fof(f2531,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssRr(X1,X0)
| ~ ssPv2(X1)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f2529,f60]) ).
fof(f2532,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssRr(X1,X0)
| ~ ssPv4(X1)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[],[f2529,f62]) ).
fof(f2543,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv4(X1)
| ~ ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f2532]) ).
fof(f2544,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f2531]) ).
fof(f2547,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv3(X0) ),
inference(resolution,[],[f2543,f1]) ).
fof(f2549,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv1(X0)
| ~ ssPv3(X0) ),
inference(resolution,[],[f2544,f1]) ).
fof(f2619,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[],[f2547,f2152]) ).
fof(f2624,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2619]) ).
fof(f2680,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2549,f2100]) ).
fof(f2690,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2549,f1011]) ).
fof(f2693,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f2690,f2547]) ).
fof(f2694,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2680,f2547]) ).
fof(f2695,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2693,f2013]) ).
fof(f2696,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[],[f2694,f2427]) ).
fof(f2710,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[],[f2696,f2003]) ).
fof(f2712,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[],[f2696,f2288]) ).
fof(f2767,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2695,f193]) ).
fof(f2772,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f2767,f2712]) ).
fof(f2778,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[],[f2772,f2696]) ).
fof(f2791,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[],[f2778,f2508]) ).
fof(f2817,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf2(X0)) ),
inference(resolution,[],[f2791,f134]) ).
fof(f2827,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(skf3(X0))
| ssPv2(X0) ),
inference(resolution,[],[f2791,f200]) ).
fof(f2831,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2827]) ).
fof(f2835,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f2817]) ).
fof(f2849,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[],[f2835,f497]) ).
fof(f2862,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2849,f2323]) ).
fof(f2866,plain,
! [X0] :
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2862,f1309]) ).
fof(f2955,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f2866,f2710]) ).
fof(f2994,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[],[f2831,f1669]) ).
fof(f3008,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f2994,f2507]) ).
fof(f3011,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3008,f2955]) ).
fof(f3015,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[],[f3011,f57]) ).
fof(f3025,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv2(X0) ),
inference(duplicate_literal_removal,[],[f3015]) ).
fof(f3027,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3025,f1011]) ).
fof(f3043,plain,
! [X0] :
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[],[f3027,f172]) ).
fof(f3064,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[],[f3027,f2507]) ).
fof(f3066,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv3(X0) ),
inference(duplicate_literal_removal,[],[f3064]) ).
fof(f3076,plain,
! [X0] :
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3043,f3066]) ).
fof(f3085,plain,
! [X0] :
( ssPv3(skf3(skf3(X0)))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3076,f2003]) ).
fof(f3223,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv2(skf3(skf3(X0)))
| ssPv2(skf3(X0)) ),
inference(resolution,[],[f3085,f2831]) ).
fof(f3225,plain,
! [X0] :
( ~ ssPv2(skf3(skf3(X0)))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3223,f3011]) ).
fof(f3228,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(resolution,[],[f3225,f2100]) ).
fof(f3238,plain,
! [X0] :
( ssPv4(skf3(skf3(X0)))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[],[f3228,f2003]) ).
fof(f3243,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0) ),
inference(resolution,[],[f3238,f185]) ).
fof(f3256,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f3243,f2508]) ).
fof(f3259,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f3256,f2710]) ).
fof(f3260,plain,
! [X0] : ssPv3(X0),
inference(forward_subsumption_resolution,[],[f3259,f2003]) ).
fof(f3283,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv2(X0) ),
inference(resolution,[],[f3260,f2831]) ).
fof(f3289,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[],[f3260,f2624]) ).
fof(f3337,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[],[f3283,f189]) ).
fof(f3338,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[],[f3283,f75]) ).
fof(f3345,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literal_removal,[],[f3338]) ).
fof(f3352,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f3345,f2696]) ).
fof(f3353,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(skf2(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f3337,f781]) ).
fof(f3358,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[],[f3353,f2101]) ).
fof(f3362,plain,
! [X0] : ssPv2(X0),
inference(forward_subsumption_resolution,[],[f3358,f3352]) ).
fof(f3417,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[],[f3362,f127]) ).
fof(f3443,plain,
! [X0] : ssPv1(X0),
inference(resolution,[],[f3362,f3289]) ).
fof(f3452,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[],[f3417,f3362]) ).
fof(f3456,plain,
! [X0] : ~ ssPv1(skf3(X0)),
inference(forward_subsumption_resolution,[],[f3452,f3443]) ).
fof(f3458,plain,
$false,
inference(forward_subsumption_resolution,[],[f3456,f3443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN784-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:56:32 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.61/1.98 % (2778995)Input is clausal, will run a generic CNF schedule.
% 7.61/1.98 % (2779003)lrs+10_1_sil=8000:sp=occurrence:random_seed=114338610:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.61/1.98 % (2779003)Instruction limit reached!
% 7.61/1.98 % (2779003)------------------------------
% 7.61/1.98 % (2779003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.98 % (2779003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.98 % (2779003)CaDiCaL version: 2.1.3
% 7.61/1.98 % (2779003)Termination reason: Instruction limit
% 7.61/1.98 % (2779003)Termination phase: Saturation
% 7.61/1.98 % (2779003)Time elapsed: 0.035 s
% 7.61/1.98 % (2779003)Peak memory usage: 88 MB
% 7.61/1.98 % (2779003)Instructions burned: 109 (million)
% 7.61/1.98 % (2779002)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1009780013:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.61/1.98 % (2779004)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3336942496:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.61/1.98 % (2779001)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4183776556:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.61/1.98 % (2779000)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=2368491895:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.61/1.98 % (2779006)dis-21_1_sil=8000:lcm=predicate:random_seed=1771714210:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.61/1.98 % (2779005)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2451358986:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.61/1.98 % (2779006)Instruction limit reached!
% 7.61/1.98 % (2779006)------------------------------
% 7.61/1.98 % (2779006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.98 % (2779006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.98 % (2779006)CaDiCaL version: 2.1.3
% 7.61/1.98 % (2779006)Termination reason: Instruction limit
% 7.61/1.98 % (2779006)Termination phase: Saturation
% 7.61/1.98 % (2779006)Time elapsed: 0.053 s
% 7.61/1.98 % (2779006)Peak memory usage: 87 MB
% 7.61/1.98 % (2779006)Instructions burned: 119 (million)
% 7.61/1.98 % (2779004)Instruction limit reached!
% 7.61/1.98 % (2779004)------------------------------
% 7.61/1.98 % (2779004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.98 % (2779004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.98 % (2779004)CaDiCaL version: 2.1.3
% 7.61/1.98 % (2779004)Termination reason: Instruction limit
% 7.61/1.98 % (2779004)Termination phase: Saturation
% 7.61/1.98 % (2779004)Time elapsed: 0.067 s
% 7.61/1.98 % (2779004)Peak memory usage: 87 MB
% 7.61/1.98 % (2779004)Instructions burned: 115 (million)
% 7.61/1.98 % (2779005)Instruction limit reached!
% 7.61/1.98 % (2779005)------------------------------
% 7.61/1.98 % (2779005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.98 % (2779005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.98 % (2779005)CaDiCaL version: 2.1.3
% 7.61/1.98 % (2779005)Termination reason: Instruction limit
% 7.61/1.98 % (2779005)Termination phase: Saturation
% 7.61/1.98 % (2779005)Time elapsed: 0.088 s
% 7.61/1.98 % (2779005)Peak memory usage: 87 MB
% 7.61/1.98 % (2779005)Instructions burned: 181 (million)
% 7.61/1.98 % (2779008)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=856011004:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.61/1.98 % (2779008)Instruction limit reached!
% 7.61/1.98 % (2779008)------------------------------
% 7.61/1.98 % (2779008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.98 % (2779008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.98 % (2779008)CaDiCaL version: 2.1.3
% 7.61/1.98 % (2779008)Termination reason: Instruction limit
% 7.61/1.98 % (2779008)Termination phase: Saturation
% 7.61/1.98 % (2779008)Time elapsed: 0.044 s
% 7.61/1.98 % (2779008)Peak memory usage: 87 MB
% 7.61/1.98 % (2779008)Instructions burned: 144 (million)
% 7.61/1.98 % (2779015)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=983925601:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.61/2.01 % (2779016)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=390430522:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.61/2.01 % (2779015)Refutation not found, incomplete strategy
% 7.61/2.01 % (2779015)------------------------------
% 7.61/2.01 % (2779015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779015)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779015)Termination reason: Refutation not found, incomplete strategy
% 7.61/2.01 % (2779015)Time elapsed: 0.009 s
% 7.61/2.01 % (2779015)Peak memory usage: 87 MB
% 7.61/2.01 % (2779015)Instructions burned: 15 (million)
% 7.61/2.01 % (2779017)lrs+10_64_to=lpo:sil=8000:random_seed=3022546136:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.61/2.01 % (2779019)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1935535408:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 7.61/2.01 % (2779019)Instruction limit reached!
% 7.61/2.01 % (2779019)------------------------------
% 7.61/2.01 % (2779019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779019)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779019)Termination reason: Instruction limit
% 7.61/2.01 % (2779019)Termination phase: Saturation
% 7.61/2.01 % (2779019)Time elapsed: 0.057 s
% 7.61/2.01 % (2779019)Peak memory usage: 88 MB
% 7.61/2.01 % (2779019)Instructions burned: 197 (million)
% 7.61/2.01 % (2779017)Instruction limit reached!
% 7.61/2.01 % (2779017)------------------------------
% 7.61/2.01 % (2779017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779017)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779017)Termination reason: Instruction limit
% 7.61/2.01 % (2779017)Termination phase: Saturation
% 7.61/2.01 % (2779017)Time elapsed: 0.069 s
% 7.61/2.01 % (2779017)Peak memory usage: 87 MB
% 7.61/2.01 % (2779017)Instructions burned: 126 (million)
% 7.61/2.01 % (2779016)Instruction limit reached!
% 7.61/2.01 % (2779016)------------------------------
% 7.61/2.01 % (2779016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779016)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779016)Termination reason: Instruction limit
% 7.61/2.01 % (2779016)Termination phase: Saturation
% 7.61/2.01 % (2779016)Time elapsed: 0.128 s
% 7.61/2.01 % (2779016)Peak memory usage: 87 MB
% 7.61/2.01 % (2779016)Instructions burned: 221 (million)
% 7.61/2.01 % (2779025)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3885136760:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 7.61/2.01 % (2779015)------------------------------
% 7.61/2.01 % (2779015)------------------------------
% 7.61/2.01 % (2779024)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=933608130:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 7.61/2.01 % (2779026)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=77101500:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 7.61/2.01 % (2779026)Refutation not found, incomplete strategy
% 7.61/2.01 % (2779026)------------------------------
% 7.61/2.01 % (2779026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779026)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779026)Termination reason: Refutation not found, incomplete strategy
% 7.61/2.01 % (2779026)Time elapsed: 0.003 s
% 7.61/2.01 % (2779026)Peak memory usage: 87 MB
% 7.61/2.01 % (2779026)Instructions burned: 5 (million)
% 7.61/2.01 % (2779024)Instruction limit reached!
% 7.61/2.01 % (2779024)------------------------------
% 7.61/2.01 % (2779024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779024)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779024)Termination reason: Instruction limit
% 7.61/2.01 % (2779024)Termination phase: Saturation
% 7.61/2.01 % (2779024)Time elapsed: 0.093 s
% 7.61/2.01 % (2779024)Peak memory usage: 88 MB
% 7.61/2.01 % (2779024)Instructions burned: 158 (million)
% 7.61/2.01 % (2779001)Refutation not found, incomplete strategy
% 7.61/2.01 % (2779001)------------------------------
% 7.61/2.01 % (2779001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779001)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779001)Termination reason: Refutation not found, incomplete strategy
% 7.61/2.01 % (2779001)Time elapsed: 0.585 s
% 7.61/2.01 % (2779001)Peak memory usage: 125 MB
% 7.61/2.01 % (2779001)Instructions burned: 870 (million)
% 7.61/2.01 % (2779028)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=67612083:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 7.61/2.01 % (2779028)Instruction limit reached!
% 7.61/2.01 % (2779028)------------------------------
% 7.61/2.01 % (2779028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779028)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779028)Termination reason: Instruction limit
% 7.61/2.01 % (2779028)Termination phase: Saturation
% 7.61/2.01 % (2779028)Time elapsed: 0.063 s
% 7.61/2.01 % (2779028)Peak memory usage: 87 MB
% 7.61/2.01 % (2779028)Instructions burned: 108 (million)
% 7.61/2.01 % (2779026)------------------------------
% 7.61/2.01 % (2779026)------------------------------
% 7.61/2.01 % (2779031)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3668034592:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 7.61/2.01 % (2779001)------------------------------
% 7.61/2.01 % (2779001)------------------------------
% 7.61/2.01 % (2779033)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3123092449:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 7.61/2.01 % (2779031)Instruction limit reached!
% 7.61/2.01 % (2779031)------------------------------
% 7.61/2.01 % (2779031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779031)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779031)Termination reason: Instruction limit
% 7.61/2.01 % (2779031)Termination phase: Saturation
% 7.61/2.01 % (2779031)Time elapsed: 0.130 s
% 7.61/2.01 % (2779031)Peak memory usage: 89 MB
% 7.61/2.01 % (2779031)Instructions burned: 242 (million)
% 7.61/2.01 % (2779034)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1943184000:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 7.61/2.01 % (2779000)First to succeed.
% 7.61/2.01 % (2779000)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2778995"
% 7.61/2.01 % (2779025)Also succeeded, but the first one will report.
% 7.61/2.01 % (2779034)Instruction limit reached!
% 7.61/2.01 % (2779034)------------------------------
% 7.61/2.01 % (2779034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779034)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779034)Termination reason: Instruction limit
% 7.61/2.01 % (2779034)Termination phase: Saturation
% 7.61/2.01 % (2779034)Time elapsed: 0.072 s
% 7.61/2.01 % (2779034)Peak memory usage: 88 MB
% 7.61/2.01 % (2779034)Instructions burned: 134 (million)
% 7.61/2.01 % (2779036)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=218601110:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 7.61/2.01 % (2779038)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4017016963:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 7.61/2.01 % (2779040)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1754252564:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 7.61/2.01 % (2779038)Instruction limit reached!
% 7.61/2.01 % (2779038)------------------------------
% 7.61/2.01 % (2779038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.01 % (2779038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.01 % (2779038)CaDiCaL version: 2.1.3
% 7.61/2.01 % (2779038)Termination reason: Instruction limit
% 7.61/2.01 % (2779038)Termination phase: Saturation
% 7.61/2.01 % (2779038)Time elapsed: 0.104 s
% 7.61/2.01 % (2779038)Peak memory usage: 88 MB
% 7.61/2.01 % (2779038)Instructions burned: 192 (million)
% 7.61/2.01 % (2779002)Also succeeded, but the first one will report.
% 7.61/2.01 % (2779000)Refutation found. Thanks to Tanya!
% 7.61/2.01 % SZS status Unsatisfiable for theBenchmark
% 7.61/2.01 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/2.21 % (2779000)------------------------------
% 0.21/2.21 % (2779000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/2.21 % (2779000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/2.21 % (2779000)CaDiCaL version: 2.1.3
% 0.21/2.21 % (2779000)Termination reason: Refutation
% 0.21/2.21 % (2779000)Time elapsed: 0.905 s
% 0.21/2.21 % (2779000)Peak memory usage: 128 MB
% 0.21/2.21 % (2779000)Instructions burned: 1294 (million)
% 0.21/2.21 % (2779000)------------------------------
% 0.21/2.21 % (2779000)------------------------------
% 0.21/2.21 % (2778995)Success in time 1.338 s
% 0.21/2.21 % Vampire exiting
%------------------------------------------------------------------------------