%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL061+2 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:51:04 AM UTC 2026
% Result : Theorem 39.12s 10.06s
% Output : Refutation 65.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 5
% Syntax : Number of formulae : 191 ( 16 unt; 2 def)
% Number of atoms : 489 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 599 ( 301 ~; 294 |; 1 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 3 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 625 ( 0 sgn 625 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( is_a_theorem(implies(X0,X1))
& is_a_theorem(X0) )
=> is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] : is_a_theorem(implies(implies(implies(implies(implies(X0,implies(X1,X0)),implies(implies(X2,implies(X3,implies(X4,X3))),X5)),X5),implies(implies(implies(implies(implies(implies(implies(X6,X7),implies(implies(X7,X8),implies(X6,X8))),implies(implies(implies(n(X9),X9),X9),X10)),X10),implies(implies(X11,implies(n(X11),X12)),X13)),X13),X14)),X14)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f2) ).
fof(f3,conjecture,
is_a_theorem(implies(implies(n(a),c),implies(implies(b,c),implies(implies(a,b),c)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f3) ).
fof(f4,negated_conjecture,
~ is_a_theorem(implies(implies(n(a),c),implies(implies(b,c),implies(implies(a,b),c)))),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
~ is_a_theorem(implies(implies(n(a),c),implies(implies(b,c),implies(implies(a,b),c)))),
inference(flattening,[],[f4]) ).
fof(f6,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f7,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(flattening,[],[f6]) ).
fof(f8,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f9,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] : is_a_theorem(implies(implies(implies(implies(implies(X0,implies(X1,X0)),implies(implies(X2,implies(X3,implies(X4,X3))),X5)),X5),implies(implies(implies(implies(implies(implies(implies(X6,X7),implies(implies(X7,X8),implies(X6,X8))),implies(implies(implies(n(X9),X9),X9),X10)),X10),implies(implies(X11,implies(n(X11),X12)),X13)),X13),X14)),X14)),
inference(cnf_transformation,[],[f2]) ).
fof(f10,plain,
~ is_a_theorem(implies(implies(n(a),c),implies(implies(b,c),implies(implies(a,b),c)))),
inference(cnf_transformation,[],[f5]) ).
fof(f11,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ is_a_theorem(implies(implies(implies(implies(X1,implies(X2,X1)),implies(implies(X3,implies(X4,implies(X5,X4))),X6)),X6),implies(implies(implies(implies(implies(implies(implies(X7,X8),implies(implies(X8,X9),implies(X7,X9))),implies(implies(implies(n(X10),X10),X10),X11)),X11),implies(implies(X12,implies(n(X12),X13)),X14)),X14),X0)))
| is_a_theorem(X0) ),
inference(resolution,[],[f9,f8]) ).
fof(f12,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(resolution,[],[f11,f9]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,X0)),implies(implies(X2,implies(X3,implies(X4,X3))),X5)),X5)),
inference(resolution,[],[f12,f11]) ).
fof(f15,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f13,f11]) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X1,implies(X2,X1)),implies(implies(X3,implies(X4,implies(X5,X4))),X0)))
| is_a_theorem(X0) ),
inference(resolution,[],[f13,f8]) ).
fof(f17,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : is_a_theorem(implies(X0,implies(implies(implies(implies(implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))),implies(implies(implies(n(X4),X4),X4),X5)),X5),implies(implies(X6,implies(n(X6),X7)),X8)),X8))),
inference(resolution,[],[f15,f11]) ).
fof(f19,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( is_a_theorem(implies(implies(implies(implies(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),implies(implies(implies(n(X3),X3),X3),X4)),X4),implies(implies(X5,implies(n(X5),X6)),X7)),X7))
| ~ is_a_theorem(X8) ),
inference(resolution,[],[f17,f8]) ).
fof(f21,definition,
( spl0_1
<=> ! [X8] : ~ is_a_theorem(X8) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f22,plain,
( ! [X8] : ~ is_a_theorem(X8)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f21]) ).
fof(f24,definition,
( spl0_2
<=> ! [X5,X4,X2,X7,X0,X6,X3,X1] : is_a_theorem(implies(implies(implies(implies(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),implies(implies(implies(n(X3),X3),X3),X4)),X4),implies(implies(X5,implies(n(X5),X6)),X7)),X7)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f25,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] : is_a_theorem(implies(implies(implies(implies(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),implies(implies(implies(n(X3),X3),X3),X4)),X4),implies(implies(X5,implies(n(X5),X6)),X7)),X7))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f26,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f19,f24,f21]) ).
fof(f28,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ is_a_theorem(implies(implies(implies(implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))),implies(implies(implies(n(X4),X4),X4),X5)),X5),implies(implies(X6,implies(n(X6),X7)),X0)))
| is_a_theorem(X0) )
| ~ spl0_2 ),
inference(resolution,[],[f25,f8]) ).
fof(f31,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),implies(implies(implies(n(X3),X3),X3),X4)),X4))
| ~ spl0_2 ),
inference(resolution,[],[f28,f12]) ).
fof(f32,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(n(X1),X2))))
| ~ spl0_2 ),
inference(resolution,[],[f28,f15]) ).
fof(f54,plain,
( $false
| ~ spl0_1 ),
inference(resolution,[],[f22,f13]) ).
fof(f67,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f54]) ).
fof(f81,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X0)),X2),implies(X3,X2)))
| ~ spl0_2 ),
inference(resolution,[],[f16,f31]) ).
fof(f83,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(implies(n(X1),X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f16,f25]) ).
fof(f96,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ spl0_2 ),
inference(resolution,[],[f81,f28]) ).
fof(f102,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(X2,X0)) )
| ~ spl0_2 ),
inference(resolution,[],[f96,f8]) ).
fof(f106,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f102,f8]) ).
fof(f112,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X3,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f106,f96]) ).
fof(f114,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X0,X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f106,f12]) ).
fof(f129,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X0)),X2))
| is_a_theorem(X2) )
| ~ spl0_2 ),
inference(resolution,[],[f114,f16]) ).
fof(f137,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2)))
| ~ spl0_2 ),
inference(resolution,[],[f129,f96]) ).
fof(f145,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X3,implies(X4,X3)),implies(X2,X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f129,f112]) ).
fof(f151,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X3,X1),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f137,f106]) ).
fof(f152,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X0),X1))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f137,f8]) ).
fof(f162,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1)))
| ~ spl0_2 ),
inference(resolution,[],[f151,f83]) ).
fof(f186,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3)))
| ~ spl0_2 ),
inference(resolution,[],[f145,f31]) ).
fof(f198,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(n(X0),X1),X2),implies(X0,X2)))
| ~ spl0_2 ),
inference(resolution,[],[f145,f32]) ).
fof(f200,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(n(X0),X0),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f145,f83]) ).
fof(f217,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X1,X3),implies(X0,X3)),X2))
| is_a_theorem(implies(implies(X0,X1),X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f186,f8]) ).
fof(f227,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X3))))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f217,f102]) ).
fof(f230,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(implies(X1,X4),implies(X0,X4)),X3))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f217,f114]) ).
fof(f243,plain,
( ! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(implies(X1,X4),implies(X0,implies(implies(X4,X2),X3))))
| ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f227,f217]) ).
fof(f259,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,n(X1)),implies(X1,implies(X0,X2))))
| ~ spl0_2 ),
inference(resolution,[],[f198,f217]) ).
fof(f261,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(n(X1),X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f198,f106]) ).
fof(f340,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(implies(implies(n(X0),X0),X0),X1),X1))
| ~ spl0_2 ),
inference(resolution,[],[f152,f31]) ).
fof(f382,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(n(X1),X1)),implies(X2,implies(X0,X1))))
| ~ spl0_2 ),
inference(resolution,[],[f340,f230]) ).
fof(f383,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(n(X1),X1)),implies(X0,X1)))
| ~ spl0_2 ),
inference(resolution,[],[f340,f217]) ).
fof(f395,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(n(X0),X1),implies(implies(X1,X0),X0)))
| ~ spl0_2 ),
inference(resolution,[],[f383,f217]) ).
fof(f399,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(n(X1),X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f383,f8]) ).
fof(f403,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f395,f152]) ).
fof(f405,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(n(X0),n(X1)),implies(X1,X0)))
| ~ spl0_2 ),
inference(resolution,[],[f395,f261]) ).
fof(f407,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(implies(n(X1),X0)) )
| ~ spl0_2 ),
inference(resolution,[],[f395,f8]) ).
fof(f445,plain,
( ! [X0,X1] : is_a_theorem(implies(n(X0),implies(X0,X1)))
| ~ spl0_2 ),
inference(resolution,[],[f403,f261]) ).
fof(f461,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(implies(X0,X1)),implies(X2,X1)))
| is_a_theorem(implies(implies(X0,X2),implies(X0,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f407,f217]) ).
fof(f472,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(n(X2),n(X1))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f405,f106]) ).
fof(f573,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ spl0_2 ),
inference(resolution,[],[f461,f445]) ).
fof(f576,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X1))))
| ~ spl0_2 ),
inference(resolution,[],[f461,f15]) ).
fof(f604,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(implies(X0,X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f573,f217]) ).
fof(f611,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X1,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f573,f106]) ).
fof(f620,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(implies(X0,X1),X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f604,f8]) ).
fof(f632,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f611,f227]) ).
fof(f657,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X1,implies(X0,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f632,f152]) ).
fof(f708,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),X1))
| ~ spl0_2 ),
inference(resolution,[],[f620,f162]) ).
fof(f725,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X2),X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f708,f106]) ).
fof(f785,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))
| ~ spl0_2 ),
inference(resolution,[],[f657,f96]) ).
fof(f786,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(n(X0),X0),implies(implies(X0,X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f657,f200]) ).
fof(f844,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f785,f8]) ).
fof(f851,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(n(X1),X1)))
| is_a_theorem(implies(X0,implies(implies(X1,X2),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f786,f106]) ).
fof(f872,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X0),implies(X1,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f844,f611]) ).
fof(f888,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),X3)))
| is_a_theorem(implies(implies(X0,X2),implies(implies(X2,X1),X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f872,f217]) ).
fof(f944,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(X1),X0))
| is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f851,f102]) ).
fof(f997,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(implies(X0,X2),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f944,f445]) ).
fof(f1005,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(n(X0),X0),X0),X1),implies(implies(X1,X2),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f944,f83]) ).
fof(f1023,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X2),X0),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f997,f657]) ).
fof(f1030,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0)))
| ~ spl0_2 ),
inference(resolution,[],[f1023,f129]) ).
fof(f1104,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),X0)))
| ~ spl0_2 ),
inference(resolution,[],[f1030,f888]) ).
fof(f1108,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,implies(X0,X1))))
| ~ spl0_2 ),
inference(resolution,[],[f1030,f217]) ).
fof(f1121,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f1030,f106]) ).
fof(f1142,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X1,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f1108,f8]) ).
fof(f1181,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,n(X0)),implies(X1,n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f1121,f200]) ).
fof(f1227,plain,
( ! [X0] : is_a_theorem(implies(implies(X0,n(X0)),n(X0)))
| ~ spl0_2 ),
inference(resolution,[],[f1181,f399]) ).
fof(f1298,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X2),X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f1104,f217]) ).
fof(f1306,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X3),X1)))
| is_a_theorem(implies(X0,implies(implies(X1,X2),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f1104,f106]) ).
fof(f1321,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X0,X2),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f1298,f657]) ).
fof(f1340,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X3),X2)))
| is_a_theorem(implies(X0,implies(implies(X1,X2),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f1321,f106]) ).
fof(f1358,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(n(X0),X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f1340,f200]) ).
fof(f1368,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X3),X0))
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f1340,f102]) ).
fof(f1419,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(n(X0),X1),implies(implies(X0,X1),X1)))
| ~ spl0_2 ),
inference(resolution,[],[f1358,f657]) ).
fof(f2357,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(implies(n(X0),X2),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f1368,f1419]) ).
fof(f2446,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2)))
| ~ spl0_2 ),
inference(resolution,[],[f2357,f261]) ).
fof(f2469,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2))))
| ~ spl0_2 ),
inference(resolution,[],[f2446,f217]) ).
fof(f2490,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(implies(X1,X3),X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f2446,f106]) ).
fof(f2511,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(implies(X1,X1),X2)),implies(X0,X2)))
| ~ spl0_2 ),
inference(resolution,[],[f2469,f725]) ).
fof(f2577,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(implies(X3,X3),X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f2511,f106]) ).
fof(f2625,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(implies(X3,X3),X2)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f2577,f844]) ).
fof(f3151,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(implies(X2,X0),X1))))
| ~ spl0_2 ),
inference(resolution,[],[f2490,f785]) ).
fof(f3154,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X2,X3),X3),X0))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f2490,f102]) ).
fof(f3238,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(implies(n(X0),X0),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f3154,f1005]) ).
fof(f3244,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(n(X0),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f3154,f198]) ).
fof(f3290,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(X0),implies(X2,X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f3154,f407]) ).
fof(f3366,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(n(X1),implies(X0,X2))))
| ~ spl0_2 ),
inference(resolution,[],[f3244,f217]) ).
fof(f3381,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X3),X2)))
| is_a_theorem(implies(X0,implies(n(X1),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f3244,f106]) ).
fof(f3398,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(n(X1),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f3366,f2577]) ).
fof(f3402,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X0),implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X0)) )
| ~ spl0_2 ),
inference(resolution,[],[f3366,f8]) ).
fof(f3488,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X3,X3),X1)))
| is_a_theorem(implies(X0,implies(n(X1),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f3398,f106]) ).
fof(f3990,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(n(X2),X0)))
| ~ spl0_2 ),
inference(resolution,[],[f3381,f1104]) ).
fof(f4175,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X3),X1)))
| is_a_theorem(implies(X0,implies(n(X1),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f3990,f106]) ).
fof(f4193,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(n(X2),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f4175,f3238]) ).
fof(f4280,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(n(X0),n(X1)),X2),implies(implies(X1,X0),X2)))
| ~ spl0_2 ),
inference(resolution,[],[f4193,f3154]) ).
fof(f4332,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(n(X1),n(X0)))))
| ~ spl0_2 ),
inference(resolution,[],[f4280,f129]) ).
fof(f4336,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,n(X1)),implies(implies(X2,X1),implies(X0,n(X2)))))
| ~ spl0_2 ),
inference(resolution,[],[f4280,f217]) ).
fof(f4387,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,n(X1)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,n(X0)))) )
| ~ spl0_2 ),
inference(resolution,[],[f4336,f8]) ).
fof(f4391,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(n(X2),n(X0)))))
| ~ spl0_2 ),
inference(resolution,[],[f4332,f888]) ).
fof(f4465,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,n(X1)),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f4387,f1227]) ).
fof(f4494,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,n(X1)),n(X2))))
| ~ is_a_theorem(implies(X0,implies(X2,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f4465,f106]) ).
fof(f4656,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(n(X2),n(X0)))))
| ~ spl0_2 ),
inference(resolution,[],[f4391,f2490]) ).
fof(f5086,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(n(X1),X1)),implies(n(X1),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f4656,f611]) ).
fof(f5130,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X2,implies(n(X1),X1))))
| is_a_theorem(implies(X0,implies(n(X1),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f5086,f106]) ).
fof(f5171,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(n(X2),X2)))
| is_a_theorem(implies(implies(X0,X1),implies(n(X2),n(X0)))) )
| ~ spl0_2 ),
inference(resolution,[],[f5130,f844]) ).
fof(f5262,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(implies(X1,X2),X1)),implies(n(X1),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f5171,f3244]) ).
fof(f5378,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X2,implies(implies(X1,X3),X1))))
| is_a_theorem(implies(X0,implies(n(X1),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f5262,f106]) ).
fof(f5537,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(implies(X0,X3),X1)))
| is_a_theorem(implies(implies(X0,X1),implies(n(X1),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f5378,f243]) ).
fof(f5907,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,n(X1)),implies(n(n(X1)),n(X2))))
| ~ is_a_theorem(implies(X2,implies(X1,X0))) )
| ~ spl0_2 ),
inference(resolution,[],[f5537,f4494]) ).
fof(f5977,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(X1,n(X0)),n(X0)))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f5907,f399]) ).
fof(f5990,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,X0),implies(implies(X1,n(X0)),n(X2))))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f5977,f4387]) ).
fof(f6006,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(implies(X2,X0),implies(implies(X1,n(X2)),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f5990,f1340]) ).
fof(f6053,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(n(X1),X1)),implies(implies(X1,n(X0)),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f6006,f83]) ).
fof(f6095,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X2,implies(n(X1),X1))))
| is_a_theorem(implies(X0,implies(implies(X1,n(X2)),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f6053,f106]) ).
fof(f6255,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,implies(n(X2),X2))))
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,n(X0)),n(X0)))) )
| ~ spl0_2 ),
inference(resolution,[],[f6095,f872]) ).
fof(f6623,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(implies(X1,n(X0)),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f6255,f576]) ).
fof(f6714,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(n(X1),n(X0))))
| ~ spl0_2 ),
inference(resolution,[],[f6623,f3381]) ).
fof(f6754,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X2,implies(X2,X1))))
| is_a_theorem(implies(X0,implies(n(X1),n(X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f6714,f106]) ).
fof(f6812,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(n(X2),n(X0))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f6754,f227]) ).
fof(f6905,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X2),implies(implies(X0,X1),n(X0))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f6812,f657]) ).
fof(f8051,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X2),implies(X1,n(X0))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f6905,f151]) ).
fof(f8114,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(n(X1),X2)))
| is_a_theorem(implies(n(X2),implies(X0,X1))) )
| ~ spl0_2 ),
inference(resolution,[],[f8051,f472]) ).
fof(f8182,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X0),implies(implies(X1,X0),X2)))
| ~ is_a_theorem(implies(n(X2),X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f8114,f102]) ).
fof(f8234,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(X0),X1))
| is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X0),X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f8182,f3290]) ).
fof(f8244,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X2),implies(implies(X0,X1),X1)))
| ~ is_a_theorem(implies(n(X0),X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f8182,f1306]) ).
fof(f8301,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,X3),X0),X1)))
| ~ is_a_theorem(implies(X2,X0)) )
| ~ spl0_2 ),
inference(resolution,[],[f8234,f3402]) ).
fof(f8458,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(implies(X2,implies(implies(X0,X1),X3)),implies(X2,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f8301,f2625]) ).
fof(f8523,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(implies(X1,X2),X3)),implies(X0,X3)))
| ~ is_a_theorem(implies(X1,X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f8458,f114]) ).
fof(f8600,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(implies(X0,X1),X3)))
| is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f8523,f8]) ).
fof(f8732,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(X2),X1))
| ~ is_a_theorem(implies(X2,X1))
| is_a_theorem(implies(n(X0),X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f8600,f8244]) ).
fof(f8742,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(n(X3),implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X0)) )
| ~ spl0_2 ),
inference(resolution,[],[f8732,f3402]) ).
fof(f9238,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X1,X3)))
| is_a_theorem(implies(n(X0),implies(X1,X2)))
| ~ is_a_theorem(implies(X3,X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f8742,f844]) ).
fof(f10177,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(n(X0),implies(implies(n(X1),X1),X2)))
| ~ is_a_theorem(implies(X1,X2)) )
| ~ spl0_2 ),
inference(resolution,[],[f9238,f83]) ).
fof(f10318,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,implies(n(X0),X0)),implies(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f10177,f461]) ).
fof(f10554,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(n(X0),X2),implies(implies(X2,X0),X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f10318,f217]) ).
fof(f10993,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,X0),implies(implies(n(X0),X2),X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f10554,f657]) ).
fof(f11068,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,X0),implies(implies(n(X0),X1),X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f10993,f1340]) ).
fof(f11424,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(n(X0),X1))
| is_a_theorem(implies(implies(X2,X0),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f11068,f8600]) ).
fof(f11477,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(X1,implies(X2,X3)))
| ~ is_a_theorem(implies(X2,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f11424,f3402]) ).
fof(f11749,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(X2,implies(X0,X1)))
| is_a_theorem(implies(implies(X0,X4),implies(X2,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f11477,f217]) ).
fof(f11895,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X3),implies(X0,implies(implies(X0,X1),X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f11749,f3151]) ).
fof(f11966,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X1,X2))))
| is_a_theorem(implies(implies(X1,X3),implies(X0,implies(X1,X2)))) )
| ~ spl0_2 ),
inference(resolution,[],[f11749,f1108]) ).
fof(f14663,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(implies(X0,X1),X2),X3),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f11895,f145]) ).
fof(f14963,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X3,implies(X0,X1)),implies(X0,implies(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f14663,f217]) ).
fof(f15049,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f14963,f611]) ).
fof(f15595,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,implies(X0,implies(X0,X1))))
| is_a_theorem(implies(X3,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f15049,f106]) ).
fof(f15665,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(n(X1),X1)),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f15595,f382]) ).
fof(f16525,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,implies(X0,implies(n(X1),X1))))
| is_a_theorem(implies(X3,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f15665,f106]) ).
fof(f16613,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(n(X0),n(X1)),implies(X1,X2)))
| ~ is_a_theorem(implies(X1,implies(X0,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f16525,f259]) ).
fof(f18679,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,implies(n(X1),n(X0))))
| is_a_theorem(implies(X3,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f16613,f106]) ).
fof(f22559,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X0,X2),implies(X0,X3))))
| ~ is_a_theorem(implies(X2,implies(X0,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f11966,f844]) ).
fof(f22698,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X3,implies(implies(X1,X0),implies(X1,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f22559,f1142]) ).
fof(f23520,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X3,implies(X1,X0)),implies(X3,implies(X1,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f22698,f461]) ).
fof(f23566,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X3),implies(implies(X3,X0),implies(X1,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f23520,f217]) ).
fof(f23699,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X0),implies(n(implies(X1,X2)),X3)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f23566,f3488]) ).
fof(f24447,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X3,implies(implies(X1,X2),X4)))
| is_a_theorem(implies(implies(X1,X0),implies(X3,X4)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f23699,f18679]) ).
fof(f25565,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X3))))
| ~ is_a_theorem(implies(X1,implies(X0,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f24447,f96]) ).
fof(f25717,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X0),implies(X3,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X3,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f25565,f8600]) ).
fof(f27657,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),X3)))
| ~ is_a_theorem(implies(X4,implies(X2,X1)))
| is_a_theorem(implies(implies(X0,X2),implies(X4,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f25717,f217]) ).
fof(f28740,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3))))
| is_a_theorem(implies(implies(X2,X1),implies(X0,implies(X2,X3)))) )
| ~ spl0_2 ),
inference(resolution,[],[f27657,f1108]) ).
fof(f34807,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X0,X2),implies(X0,X3))))
| ~ is_a_theorem(implies(X1,implies(X2,X3))) )
| ~ spl0_2 ),
inference(resolution,[],[f28740,f227]) ).
fof(f35957,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(implies(X3,X0),implies(X3,X2)))
| ~ is_a_theorem(implies(X3,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f34807,f8600]) ).
fof(f38387,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(n(X1),X2)),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f35957,f1419]) ).
fof(f40073,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,implies(X0,implies(n(X1),X2))))
| is_a_theorem(implies(X3,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f38387,f106]) ).
fof(f40240,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(n(X3),X2)))
| ~ is_a_theorem(implies(X1,implies(X3,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_2 ),
inference(resolution,[],[f40073,f114]) ).
fof(f40344,plain,
( $false
| ~ spl0_2 ),
inference(unit_resulting_resolution,[],[f40240,f3151,f10,f576]) ).
fof(f40483,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f40344]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f26]) ).
cnf(s9,plain,
~ spl0_1,
inference(sat_conversion,[],[f67]) ).
cnf(s27,plain,
~ spl0_2,
inference(sat_conversion,[],[f40483]) ).
cnf(s28,plain,
$false,
inference(rat,[],[s1,s27,s9]) ).
fof(f40484,plain,
$false,
inference(avatar_sat_refutation,[],[s28]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL061+2 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 15:19:40 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 14.39/2.99 % (3086659)Detected formulas, will run a generic FOF schedule.
% 14.39/2.99 % (3086666)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=2576832782:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.39/2.99 % (3086669)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=704897716:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.39/2.99 % (3086664)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=1914232076:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.39/2.99 % (3086668)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2917562759:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.39/2.99 % (3086667)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3265694189:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.39/2.99 % (3086670)dis-21_1_sil=8000:lcm=predicate:random_seed=1149648466: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)
% 14.39/2.99 % (3086665)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=3068890120:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.39/2.99 % (3086667)Refutation not found, incomplete strategy
% 14.39/2.99 % (3086667)------------------------------
% 14.39/2.99 % (3086667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.39/2.99 % (3086667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.99 % (3086667)CaDiCaL version: 2.1.3
% 14.39/2.99 % (3086667)Termination reason: Refutation not found, incomplete strategy
% 14.39/2.99 % (3086667)Time elapsed: 0.001 s
% 14.39/2.99 % (3086667)Peak memory usage: 87 MB
% 14.39/2.99 % (3086668)Instruction limit reached!
% 14.39/2.99 % (3086668)------------------------------
% 14.39/2.99 % (3086668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.39/2.99 % (3086668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.99 % (3086668)CaDiCaL version: 2.1.3
% 14.39/2.99 % (3086668)Termination reason: Instruction limit
% 14.39/2.99 % (3086668)Termination phase: Saturation
% 14.39/2.99 % (3086668)Time elapsed: 0.076 s
% 14.39/2.99 % (3086668)Peak memory usage: 88 MB
% 14.39/2.99 % (3086668)Instructions burned: 120 (million)
% 14.39/2.99 % (3086670)Instruction limit reached!
% 14.39/2.99 % (3086670)------------------------------
% 14.39/2.99 % (3086670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.39/2.99 % (3086670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.99 % (3086670)CaDiCaL version: 2.1.3
% 14.39/2.99 % (3086670)Termination reason: Instruction limit
% 14.39/2.99 % (3086670)Termination phase: Saturation
% 14.39/2.99 % (3086670)Time elapsed: 0.083 s
% 14.39/2.99 % (3086670)Peak memory usage: 89 MB
% 14.39/2.99 % (3086670)Instructions burned: 129 (million)
% 14.39/2.99 % (3086669)Instruction limit reached!
% 14.39/2.99 % (3086669)------------------------------
% 14.39/2.99 % (3086669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.39/2.99 % (3086669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.99 % (3086669)CaDiCaL version: 2.1.3
% 14.39/2.99 % (3086669)Termination reason: Instruction limit
% 14.39/2.99 % (3086669)Termination phase: Saturation
% 14.39/2.99 % (3086669)Time elapsed: 0.086 s
% 14.39/2.99 % (3086669)Peak memory usage: 89 MB
% 14.39/2.99 % (3086669)Instructions burned: 140 (million)
% 14.39/2.99 % (3086678)lrs+10_1_sil=8000:sp=occurrence:random_seed=2535599960:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 14.39/2.99 % (3086679)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1313996491:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 14.39/2.99 % (3086667)------------------------------
% 14.39/2.99 % (3086667)------------------------------
% 14.39/2.99 % (3086680)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1224596574:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 14.39/2.99 % (3086679)Instruction limit reached!
% 14.39/2.99 % (3086679)------------------------------
% 14.39/2.99 % (3086679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.39/2.99 % (3086679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086679)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086679)Termination reason: Instruction limit
% 21.37/3.97 % (3086679)Termination phase: Saturation
% 21.37/3.97 % (3086679)Time elapsed: 0.091 s
% 21.37/3.97 % (3086679)Peak memory usage: 88 MB
% 21.37/3.97 % (3086679)Instructions burned: 158 (million)
% 21.37/3.97 % (3086683)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2209026025:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 21.37/3.97 % (3086678)Instruction limit reached!
% 21.37/3.97 % (3086678)------------------------------
% 21.37/3.97 % (3086678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086678)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086678)Termination reason: Instruction limit
% 21.37/3.97 % (3086678)Termination phase: Saturation
% 21.37/3.97 % (3086678)Time elapsed: 0.180 s
% 21.37/3.97 % (3086678)Peak memory usage: 91 MB
% 21.37/3.97 % (3086678)Instructions burned: 286 (million)
% 21.37/3.97 % (3086680)Instruction limit reached!
% 21.37/3.97 % (3086680)------------------------------
% 21.37/3.97 % (3086680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086680)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086680)Termination reason: Instruction limit
% 21.37/3.97 % (3086680)Termination phase: Saturation
% 21.37/3.97 % (3086680)Time elapsed: 0.199 s
% 21.37/3.97 % (3086680)Peak memory usage: 90 MB
% 21.37/3.97 % (3086680)Instructions burned: 326 (million)
% 21.37/3.97 % (3086685)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3904281882:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 21.37/3.97 % (3086685)Refutation not found, incomplete strategy
% 21.37/3.97 % (3086685)------------------------------
% 21.37/3.97 % (3086685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086685)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086685)Termination reason: Refutation not found, incomplete strategy
% 21.37/3.97 % (3086685)Time elapsed: 0.001 s
% 21.37/3.97 % (3086685)Peak memory usage: 87 MB
% 21.37/3.97 % (3086683)Instruction limit reached!
% 21.37/3.97 % (3086683)------------------------------
% 21.37/3.97 % (3086683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086683)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086683)Termination reason: Instruction limit
% 21.37/3.97 % (3086683)Termination phase: Saturation
% 21.37/3.97 % (3086683)Time elapsed: 0.142 s
% 21.37/3.97 % (3086683)Peak memory usage: 88 MB
% 21.37/3.97 % (3086683)Instructions burned: 248 (million)
% 21.37/3.97 % (3086687)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4142977702:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 21.37/3.97 % (3086688)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1912530689:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 21.37/3.97 % (3086688)Instruction limit reached!
% 21.37/3.97 % (3086688)------------------------------
% 21.37/3.97 % (3086688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086688)CaDiCaL version: 2.1.3
% 21.37/3.97 % (3086688)Termination reason: Instruction limit
% 21.37/3.97 % (3086688)Termination phase: Saturation
% 21.37/3.97 % (3086688)Time elapsed: 0.066 s
% 21.37/3.97 % (3086688)Peak memory usage: 88 MB
% 21.37/3.97 % (3086688)Instructions burned: 115 (million)
% 21.37/3.97 % (3086690)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2887541389:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 21.37/3.97 % (3086685)------------------------------
% 21.37/3.97 % (3086685)------------------------------
% 21.37/3.97 % (3086690)Instruction limit reached!
% 21.37/3.97 % (3086690)------------------------------
% 21.37/3.97 % (3086690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.97 % (3086690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.97 % (3086690)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086690)Termination reason: Instruction limit
% 57.42/8.96 % (3086690)Termination phase: Saturation
% 57.42/8.96 % (3086690)Time elapsed: 0.071 s
% 57.42/8.96 % (3086690)Peak memory usage: 87 MB
% 57.42/8.96 % (3086690)Instructions burned: 128 (million)
% 57.42/8.96 % (3086693)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2548905281:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 57.42/8.96 % (3086695)lrs+10_1_sil=8000:sp=occurrence:random_seed=628174025:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 57.42/8.96 % (3086693)Instruction limit reached!
% 57.42/8.96 % (3086693)------------------------------
% 57.42/8.96 % (3086693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.42/8.96 % (3086693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/8.96 % (3086693)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086693)Termination reason: Instruction limit
% 57.42/8.96 % (3086693)Termination phase: Saturation
% 57.42/8.96 % (3086693)Time elapsed: 0.063 s
% 57.42/8.96 % (3086693)Peak memory usage: 88 MB
% 57.42/8.96 % (3086693)Instructions burned: 114 (million)
% 57.42/8.96 % (3086696)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=542595845:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 57.42/8.96 % (3086696)Refutation not found, incomplete strategy
% 57.42/8.96 % (3086696)------------------------------
% 57.42/8.96 % (3086696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.42/8.96 % (3086696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/8.96 % (3086696)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086696)Termination reason: Refutation not found, incomplete strategy
% 57.42/8.96 % (3086696)Time elapsed: 0.001 s
% 57.42/8.96 % (3086696)Peak memory usage: 88 MB
% 57.42/8.96 % (3086699)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2614539822:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 57.42/8.96 % (3086696)------------------------------
% 57.42/8.96 % (3086696)------------------------------
% 57.42/8.96 % (3086702)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1414449296:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 57.42/8.96 % (3086702)Instruction limit reached!
% 57.42/8.96 % (3086702)------------------------------
% 57.42/8.96 % (3086702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.42/8.96 % (3086702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/8.96 % (3086702)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086702)Termination reason: Instruction limit
% 57.42/8.96 % (3086702)Termination phase: Saturation
% 57.42/8.96 % (3086702)Time elapsed: 0.076 s
% 57.42/8.96 % (3086702)Peak memory usage: 88 MB
% 57.42/8.96 % (3086702)Instructions burned: 134 (million)
% 57.42/8.96 % (3086695)Instruction limit reached!
% 57.42/8.96 % (3086695)------------------------------
% 57.42/8.96 % (3086695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.42/8.96 % (3086695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/8.96 % (3086695)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086695)Termination reason: Instruction limit
% 57.42/8.96 % (3086695)Termination phase: Saturation
% 57.42/8.96 % (3086695)Time elapsed: 0.558 s
% 57.42/8.96 % (3086695)Peak memory usage: 98 MB
% 57.42/8.96 % (3086695)Instructions burned: 908 (million)
% 57.42/8.96 % (3086704)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2308732118:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 57.42/8.96 % (3086704)Refutation not found, incomplete strategy
% 57.42/8.96 % (3086704)------------------------------
% 57.42/8.96 % (3086704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.42/8.96 % (3086704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/8.96 % (3086704)CaDiCaL version: 2.1.3
% 57.42/8.96 % (3086704)Termination reason: Refutation not found, incomplete strategy
% 57.42/8.96 % (3086704)Time elapsed: 0.001 s
% 57.42/8.96 % (3086704)Peak memory usage: 88 MB
% 57.42/8.96 % (3086705)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3066588114:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 57.42/8.96 % (3086704)------------------------------
% 57.42/8.96 % (3086704)------------------------------
% 57.42/8.96 % (3086708)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1499692846:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 39.12/10.06 % (3086687)Instruction limit reached!
% 39.12/10.06 % (3086687)------------------------------
% 39.12/10.06 % (3086687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086687)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086687)Termination reason: Instruction limit
% 39.12/10.06 % (3086687)Termination phase: Saturation
% 39.12/10.06 % (3086687)Time elapsed: 1.460 s
% 39.12/10.06 % (3086687)Peak memory usage: 142 MB
% 39.12/10.06 % (3086687)Instructions burned: 2351 (million)
% 39.12/10.06 % (3086708)Instruction limit reached!
% 39.12/10.06 % (3086708)------------------------------
% 39.12/10.06 % (3086708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086708)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086708)Termination reason: Instruction limit
% 39.12/10.06 % (3086708)Termination phase: Saturation
% 39.12/10.06 % (3086708)Time elapsed: 0.069 s
% 39.12/10.06 % (3086708)Peak memory usage: 88 MB
% 39.12/10.06 % (3086708)Instructions burned: 125 (million)
% 39.12/10.06 % (3086710)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2919857252:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 39.12/10.06 % (3086711)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2114280189:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 39.12/10.06 % (3086711)Refutation not found, incomplete strategy
% 39.12/10.06 % (3086711)------------------------------
% 39.12/10.06 % (3086711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086711)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086711)Termination reason: Refutation not found, incomplete strategy
% 39.12/10.06 % (3086711)Time elapsed: 0.001 s
% 39.12/10.06 % (3086711)Peak memory usage: 88 MB
% 39.12/10.06 % (3086710)Instruction limit reached!
% 39.12/10.06 % (3086710)------------------------------
% 39.12/10.06 % (3086710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086710)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086710)Termination reason: Instruction limit
% 39.12/10.06 % (3086710)Termination phase: Saturation
% 39.12/10.06 % (3086710)Time elapsed: 0.074 s
% 39.12/10.06 % (3086710)Peak memory usage: 89 MB
% 39.12/10.06 % (3086710)Instructions burned: 134 (million)
% 39.12/10.06 % (3086711)------------------------------
% 39.12/10.06 % (3086711)------------------------------
% 39.12/10.06 % (3086714)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=82996528:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 39.12/10.06 % (3086716)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4263606837:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 39.12/10.06 % (3086714)Instruction limit reached!
% 39.12/10.06 % (3086714)------------------------------
% 39.12/10.06 % (3086714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086714)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086714)Termination reason: Instruction limit
% 39.12/10.06 % (3086714)Termination phase: Saturation
% 39.12/10.06 % (3086714)Time elapsed: 0.248 s
% 39.12/10.06 % (3086714)Peak memory usage: 91 MB
% 39.12/10.06 % (3086714)Instructions burned: 433 (million)
% 39.12/10.06 % (3086718)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1268417632:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 39.12/10.06 % (3086718)Instruction limit reached!
% 39.12/10.06 % (3086718)------------------------------
% 39.12/10.06 % (3086718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086718)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086718)Termination reason: Instruction limit
% 39.12/10.06 % (3086718)Termination phase: Saturation
% 39.12/10.06 % (3086718)Time elapsed: 0.090 s
% 39.12/10.06 % (3086718)Peak memory usage: 89 MB
% 39.12/10.06 % (3086718)Instructions burned: 152 (million)
% 39.12/10.06 % (3086720)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3460123181:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 39.12/10.06 % (3086699)Instruction limit reached!
% 39.12/10.06 % (3086699)------------------------------
% 39.12/10.06 % (3086699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086699)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086699)Termination reason: Instruction limit
% 39.12/10.06 % (3086699)Termination phase: Saturation
% 39.12/10.06 % (3086699)Time elapsed: 3.154 s
% 39.12/10.06 % (3086699)Peak memory usage: 166 MB
% 39.12/10.06 % (3086699)Instructions burned: 5202 (million)
% 39.12/10.06 % (3086722)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1345181717:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi)
% 39.12/10.06 % (3086722)Refutation not found, incomplete strategy
% 39.12/10.06 % (3086722)------------------------------
% 39.12/10.06 % (3086722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086722)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086722)Termination reason: Refutation not found, incomplete strategy
% 39.12/10.06 % (3086722)Time elapsed: 0.001 s
% 39.12/10.06 % (3086722)Peak memory usage: 87 MB
% 39.12/10.06 % (3086722)------------------------------
% 39.12/10.06 % (3086722)------------------------------
% 39.12/10.06 % (3086724)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=26658391:s2a=on:i=185:s2at=1.8:fdi=4_2952 on theBenchmark for (2952ds/185Mi)
% 39.12/10.06 % (3086724)Instruction limit reached!
% 39.12/10.06 % (3086724)------------------------------
% 39.12/10.06 % (3086724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086724)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086724)Termination reason: Instruction limit
% 39.12/10.06 % (3086724)Termination phase: Saturation
% 39.12/10.06 % (3086724)Time elapsed: 0.103 s
% 39.12/10.06 % (3086724)Peak memory usage: 89 MB
% 39.12/10.06 % (3086724)Instructions burned: 185 (million)
% 39.12/10.06 % (3086726)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4261245694:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2949 on theBenchmark for (2949ds/193Mi)
% 39.12/10.06 % (3086726)Instruction limit reached!
% 39.12/10.06 % (3086726)------------------------------
% 39.12/10.06 % (3086726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086726)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086726)Termination reason: Instruction limit
% 39.12/10.06 % (3086726)Termination phase: Saturation
% 39.12/10.06 % (3086726)Time elapsed: 0.121 s
% 39.12/10.06 % (3086726)Peak memory usage: 92 MB
% 39.12/10.06 % (3086726)Instructions burned: 194 (million)
% 39.12/10.06 % (3086728)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1123655495:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi)
% 39.12/10.06 % (3086716)Instruction limit reached!
% 39.12/10.06 % (3086716)------------------------------
% 39.12/10.06 % (3086716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086716)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086716)Termination reason: Instruction limit
% 39.12/10.06 % (3086716)Termination phase: Saturation
% 39.12/10.06 % (3086716)Time elapsed: 3.452 s
% 39.12/10.06 % (3086716)Peak memory usage: 157 MB
% 39.12/10.06 % (3086716)Instructions burned: 6060 (million)
% 39.12/10.06 % (3086730)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1242996079:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 39.12/10.06 % (3086728)Instruction limit reached!
% 39.12/10.06 % (3086728)------------------------------
% 39.12/10.06 % (3086728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086728)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086728)Termination reason: Instruction limit
% 39.12/10.06 % (3086728)Termination phase: Saturation
% 39.12/10.06 % (3086728)Time elapsed: 2.574 s
% 39.12/10.06 % (3086728)Peak memory usage: 128 MB
% 39.12/10.06 % (3086728)Instructions burned: 4851 (million)
% 39.12/10.06 % (3086732)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=574602543:i=319:kws=precedence:fsr=off_2918 on theBenchmark for (2918ds/319Mi)
% 39.12/10.06 % (3086732)Instruction limit reached!
% 39.12/10.06 % (3086732)------------------------------
% 39.12/10.06 % (3086732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086732)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086732)Termination reason: Instruction limit
% 39.12/10.06 % (3086732)Termination phase: Saturation
% 39.12/10.06 % (3086732)Time elapsed: 0.168 s
% 39.12/10.06 % (3086732)Peak memory usage: 92 MB
% 39.12/10.06 % (3086732)Instructions burned: 319 (million)
% 39.12/10.06 % (3086734)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3308101632:i=2064:ep=RST_2915 on theBenchmark for (2915ds/2064Mi)
% 39.12/10.06 % (3086734)Refutation not found, incomplete strategy
% 39.12/10.06 % (3086734)------------------------------
% 39.12/10.06 % (3086734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/10.06 % (3086734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/10.06 % (3086734)CaDiCaL version: 2.1.3
% 39.12/10.06 % (3086734)Termination reason: Refutation not found, incomplete strategy
% 39.12/10.06 % (3086734)Time elapsed: 0.001 s
% 39.12/10.06 % (3086734)Peak memory usage: 88 MB
% 39.12/10.06 % (3086665)First to succeed.
% 39.12/10.06 % (3086665)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3086659"
% 39.12/10.06 % (3086734)------------------------------
% 39.12/10.06 % (3086734)------------------------------
% 39.12/10.06 % (3086736)dis-1011_128_sil=32000:random_seed=2764292718:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 39.12/10.06 % (3086665)Refutation found. Thanks to Tanya!
% 39.12/10.06 % SZS status Theorem for theBenchmark
% 39.12/10.06 % SZS output start Proof for theBenchmark
% See solution above
% 65.66/10.26 % (3086665)------------------------------
% 65.66/10.26 % (3086665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.66/10.26 % (3086665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.66/10.26 % (3086665)CaDiCaL version: 2.1.3
% 65.66/10.26 % (3086665)Termination reason: Refutation
% 65.66/10.26 % (3086665)Time elapsed: 8.647 s
% 65.66/10.26 % (3086665)Peak memory usage: 235 MB
% 65.66/10.26 % (3086665)Instructions burned: 14407 (million)
% 65.66/10.26 % (3086665)------------------------------
% 65.66/10.26 % (3086665)------------------------------
% 65.66/10.26 % (3086659)Success in time 9.199 s
% 65.66/10.26 % Vampire exiting
%------------------------------------------------------------------------------