%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL093-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:57:37 AM UTC 2026
% Result : Unsatisfiable 14.30s 3.22s
% Output : Refutation 14.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 28
% Syntax : Number of formulae : 219 ( 32 unt; 25 def)
% Number of atoms : 607 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 718 ( 330 ~; 363 |; 0 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 27 ( 26 usr; 26 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 564 ( 0 sgn 564 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(X3,X0),implies(X4,implies(X2,X0))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz_5) ).
fof(f3,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_4) ).
fof(f8,definition,
( spl0_2
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f9,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f8]) ).
fof(f15,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f2,f9]) ).
fof(f16,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f15]) ).
fof(f19,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| is_a_theorem(implies(implies(X3,X0),implies(X4,implies(X2,X0)))) ),
inference(resolution,[],[f2,f1]) ).
fof(f26,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),implies(X2,X3)),implies(X4,implies(implies(X5,X2),implies(X2,X3))))),
inference(resolution,[],[f19,f2]) ).
fof(f54,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X2,X3)))
| is_a_theorem(implies(X4,implies(implies(X5,X2),implies(X2,X3)))) ),
inference(resolution,[],[f26,f1]) ).
fof(f61,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))),
inference(resolution,[],[f54,f26]) ).
fof(f94,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2))))) ),
inference(resolution,[],[f61,f1]) ).
fof(f96,definition,
( spl0_12
<=> ! [X2,X1,X3,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f97,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f98,plain,
( spl0_12
| spl0_2 ),
inference(avatar_split_clause,[],[f94,f8,f96]) ).
fof(f99,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X1,X2)),X3),implies(X4,implies(X2,X3))))
| ~ spl0_12 ),
inference(resolution,[],[f97,f19]) ).
fof(f266,definition,
( spl0_26
<=> ! [X2,X1,X3] :
( is_a_theorem(implies(X1,implies(X2,X3)))
| ~ is_a_theorem(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f267,plain,
( ! [X2,X3,X1] :
( is_a_theorem(implies(X1,implies(X2,X3)))
| ~ is_a_theorem(X3) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f276,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| is_a_theorem(implies(X2,X0)) )
| ~ spl0_26 ),
inference(resolution,[],[f267,f1]) ).
fof(f278,definition,
( spl0_27
<=> ! [X2,X0] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X2,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f279,plain,
( ! [X2,X0] :
( is_a_theorem(implies(X2,X0))
| ~ is_a_theorem(X0) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f280,plain,
( spl0_2
| spl0_27
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f276,f266,f278,f8]) ).
fof(f282,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X0,X2))))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_27 ),
inference(resolution,[],[f279,f19]) ).
fof(f532,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))))
| ~ spl0_12 ),
inference(resolution,[],[f99,f54]) ).
fof(f543,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))) )
| ~ spl0_12 ),
inference(resolution,[],[f532,f1]) ).
fof(f544,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,implies(X2,X0))),X3),implies(X4,implies(implies(X5,X0),X3))))
| ~ spl0_12 ),
inference(resolution,[],[f532,f19]) ).
fof(f548,definition,
( spl0_36
<=> ! [X2,X1,X3,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f549,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2)))))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( spl0_36
| spl0_2
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f543,f96,f8,f548]) ).
fof(f551,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X3),implies(X4,implies(X2,X3))))
| ~ spl0_36 ),
inference(resolution,[],[f549,f19]) ).
fof(f557,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X1,implies(X2,implies(X3,X1)))) )
| ~ spl0_36 ),
inference(resolution,[],[f549,f1]) ).
fof(f559,definition,
( spl0_37
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(X3,X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f560,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(X2,implies(X3,X1))))
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f569,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X3,implies(X4,implies(X0,implies(X1,X2))))))
| ~ spl0_12
| ~ spl0_36 ),
inference(resolution,[],[f557,f99]) ).
fof(f601,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),X3))
| is_a_theorem(implies(X4,implies(X2,X3))) )
| ~ spl0_36 ),
inference(resolution,[],[f551,f1]) ).
fof(f625,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(X1,implies(implies(X1,X2),implies(X3,implies(X4,X2))))))
| ~ spl0_36 ),
inference(resolution,[],[f601,f2]) ).
fof(f742,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(X1,X2),implies(X3,implies(X4,X2))))) )
| ~ spl0_36 ),
inference(resolution,[],[f625,f1]) ).
fof(f743,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,implies(X3,X1))),X4),implies(X5,implies(X0,X4))))
| ~ spl0_36 ),
inference(resolution,[],[f625,f19]) ).
fof(f782,definition,
( spl0_41
<=> ! [X4,X3,X2,X1] : is_a_theorem(implies(X1,implies(implies(X1,X2),implies(X3,implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f783,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(X1,implies(implies(X1,X2),implies(X3,implies(X4,X2)))))
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f784,plain,
( spl0_41
| spl0_2
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f742,f548,f8,f782]) ).
fof(f791,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X3),implies(X4,implies(implies(implies(X3,X5),X2),X3))))
| ~ spl0_41 ),
inference(resolution,[],[f783,f19]) ).
fof(f891,definition,
( spl0_45
<=> ! [X2,X3,X4,X5,X1] : is_a_theorem(implies(X2,implies(X3,implies(X1,implies(X4,implies(X5,X1)))))) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f892,plain,
( ! [X2,X3,X1,X4,X5] : is_a_theorem(implies(X2,implies(X3,implies(X1,implies(X4,implies(X5,X1))))))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f929,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X2))))) )
| ~ spl0_45 ),
inference(resolution,[],[f892,f1]) ).
fof(f943,definition,
( spl0_46
<=> ! [X2,X1,X3,X4] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f944,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X2)))))
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f945,plain,
( spl0_46
| spl0_2
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f929,f891,f8,f943]) ).
fof(f946,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,X1)))) )
| ~ spl0_46 ),
inference(resolution,[],[f944,f1]) ).
fof(f1616,plain,
( spl0_37
| spl0_2
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f946,f943,f8,f559]) ).
fof(f1745,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,implies(X2,X3))),X1),implies(X4,implies(X5,X1))))
| ~ spl0_12
| ~ spl0_36 ),
inference(resolution,[],[f569,f19]) ).
fof(f1844,definition,
( spl0_54
<=> ! [X2,X4,X0,X5,X3,X1] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X0,implies(X4,implies(X5,X0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f1845,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X0,implies(X4,implies(X5,X0)))))))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f1844]) ).
fof(f1861,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,X3)))))) )
| ~ spl0_54 ),
inference(resolution,[],[f1845,f1]) ).
fof(f1876,plain,
( spl0_45
| spl0_2
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1861,f1844,f8,f891]) ).
fof(f2231,definition,
( spl0_55
<=> ! [X2,X4,X0,X5,X3] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X2,implies(implies(X0,X3),implies(X4,implies(X5,X3))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f2232,plain,
( ! [X2,X3,X0,X4,X5] :
( is_a_theorem(implies(X2,implies(implies(X0,X3),implies(X4,implies(X5,X3)))))
| ~ is_a_theorem(X0) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f2231]) ).
fof(f2242,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( is_a_theorem(implies(implies(implies(X1,implies(X2,X3)),X4),implies(X5,implies(implies(X0,X3),X4))))
| ~ is_a_theorem(X0) )
| ~ spl0_55 ),
inference(resolution,[],[f2232,f19]) ).
fof(f2875,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(implies(X0,X1),implies(X2,implies(X3,X1))),X4))
| is_a_theorem(implies(X5,implies(X0,X4))) )
| ~ spl0_36 ),
inference(resolution,[],[f743,f1]) ).
fof(f3552,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,implies(X2,X0))),X3))
| is_a_theorem(implies(X4,implies(implies(X5,X0),X3))) )
| ~ spl0_12 ),
inference(resolution,[],[f544,f1]) ).
fof(f3582,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,implies(X4,implies(X2,implies(X5,implies(X6,X2))))))))
| ~ spl0_12
| ~ spl0_36 ),
inference(resolution,[],[f3552,f569]) ).
fof(f3630,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X4,implies(X2,implies(X5,implies(X6,X2))))))) )
| ~ spl0_12
| ~ spl0_36 ),
inference(resolution,[],[f3582,f1]) ).
fof(f5330,definition,
( spl0_71
<=> ! [X5,X3,X4,X6,X2,X1] : is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X4,implies(X2,implies(X5,implies(X6,X2))))))) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f5331,plain,
( ! [X2,X3,X1,X6,X4,X5] : is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X4,implies(X2,implies(X5,implies(X6,X2)))))))
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f5330]) ).
fof(f5332,plain,
( spl0_71
| spl0_2
| ~ spl0_12
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f3630,f548,f96,f8,f5330]) ).
fof(f5333,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,implies(X2,implies(X3,X1)))),X4),implies(X5,implies(X6,X4))))
| ~ spl0_71 ),
inference(resolution,[],[f5331,f19]) ).
fof(f5524,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,implies(X2,implies(X3,X1)))),X4))
| is_a_theorem(implies(X5,implies(X6,X4))) )
| ~ spl0_71 ),
inference(resolution,[],[f5333,f1]) ).
fof(f6441,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(implies(X0,implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,implies(X6,X4))))))))
| ~ spl0_12
| ~ spl0_36
| ~ spl0_71 ),
inference(resolution,[],[f5524,f1745]) ).
fof(f6663,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,implies(X6,X4))))))) )
| ~ spl0_12
| ~ spl0_36
| ~ spl0_71 ),
inference(resolution,[],[f6441,f1]) ).
fof(f6698,plain,
( spl0_54
| spl0_2
| ~ spl0_12
| ~ spl0_36
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f6663,f5330,f548,f96,f8,f1844]) ).
fof(f6701,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,X0))) )
| ~ spl0_37 ),
inference(resolution,[],[f560,f1]) ).
fof(f6713,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X1),implies(X3,implies(X4,X1))))
| ~ spl0_37 ),
inference(resolution,[],[f560,f19]) ).
fof(f6805,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,implies(X1,X3))),implies(X4,implies(X5,implies(X2,implies(X1,X3))))))
| ~ spl0_37 ),
inference(resolution,[],[f6713,f19]) ).
fof(f7831,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X1,implies(X2,X3)),X4))
| ~ is_a_theorem(X0)
| is_a_theorem(implies(X5,implies(implies(X0,X3),X4))) )
| ~ spl0_55 ),
inference(resolution,[],[f2242,f1]) ).
fof(f8497,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( is_a_theorem(implies(X1,implies(implies(X0,X2),implies(implies(X2,X3),implies(X4,implies(X5,X3))))))
| ~ is_a_theorem(X0) )
| ~ spl0_55 ),
inference(resolution,[],[f7831,f2]) ).
fof(f8633,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| is_a_theorem(implies(implies(X0,X2),implies(implies(X2,X3),implies(X4,implies(X5,X3))))) )
| ~ spl0_55 ),
inference(resolution,[],[f8497,f1]) ).
fof(f9132,definition,
( spl0_96
<=> ! [X2,X4,X0,X5,X3] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X0,X2),implies(implies(X2,X3),implies(X4,implies(X5,X3))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f9133,plain,
( ! [X2,X3,X0,X4,X5] :
( is_a_theorem(implies(implies(X0,X2),implies(implies(X2,X3),implies(X4,implies(X5,X3)))))
| ~ is_a_theorem(X0) )
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f9132]) ).
fof(f9134,plain,
( spl0_2
| spl0_96
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f8633,f2231,f9132,f8]) ).
fof(f9383,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(X0,implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,X5)))))))
| ~ spl0_36
| ~ spl0_37 ),
inference(resolution,[],[f6805,f2875]) ).
fof(f9407,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,X5)))))) )
| ~ spl0_36
| ~ spl0_37 ),
inference(resolution,[],[f9383,f1]) ).
fof(f9452,definition,
( spl0_98
<=> ! [X3,X4,X5,X2,X1] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,X5)))))) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f9453,plain,
( ! [X2,X3,X1,X4,X5] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,implies(X5,X5))))))
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f9452]) ).
fof(f9454,plain,
( spl0_98
| spl0_2
| ~ spl0_36
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f9407,f559,f548,f8,f9452]) ).
fof(f9457,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X4))))) )
| ~ spl0_98 ),
inference(resolution,[],[f9453,f1]) ).
fof(f9501,definition,
( spl0_99
<=> ! [X4,X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X4))))) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f9502,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(X1,implies(X2,implies(X3,implies(X4,X4)))))
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f9501]) ).
fof(f9503,plain,
( spl0_99
| spl0_2
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f9457,f9452,f8,f9501]) ).
fof(f9506,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(X3,X3)))) )
| ~ spl0_99 ),
inference(resolution,[],[f9502,f1]) ).
fof(f9550,definition,
( spl0_100
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(X3,X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f9551,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(X2,implies(X3,X3))))
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f9550]) ).
fof(f9552,plain,
( spl0_100
| spl0_2
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f9506,f9501,f8,f9550]) ).
fof(f9555,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,X2))) )
| ~ spl0_100 ),
inference(resolution,[],[f9551,f1]) ).
fof(f9599,definition,
( spl0_101
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f9600,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2)))
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f9599]) ).
fof(f9601,plain,
( spl0_101
| spl0_2
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f9555,f9550,f8,f9599]) ).
fof(f9604,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,X1)) )
| ~ spl0_101 ),
inference(resolution,[],[f9600,f1]) ).
fof(f9618,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X1))))
| ~ spl0_101 ),
inference(resolution,[],[f9600,f19]) ).
fof(f9648,definition,
( spl0_102
<=> ! [X1] : is_a_theorem(implies(X1,X1)) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f9649,plain,
( ! [X1] : is_a_theorem(implies(X1,X1))
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f9648]) ).
fof(f9650,plain,
( spl0_102
| spl0_2
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f9604,f9599,f8,f9648]) ).
fof(f9668,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(X3,X2)))))
| ~ spl0_102 ),
inference(resolution,[],[f9649,f54]) ).
fof(f9690,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,implies(X3,X0))))
| ~ spl0_101 ),
inference(resolution,[],[f9618,f19]) ).
fof(f10083,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,X2)))) )
| ~ spl0_102 ),
inference(resolution,[],[f9668,f1]) ).
fof(f10148,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,implies(X3,X0))) )
| ~ spl0_101 ),
inference(resolution,[],[f9690,f1]) ).
fof(f10163,definition,
( spl0_104
<=> ! [X2,X1,X3] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,X2)))) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f10164,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,X2))))
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f10163]) ).
fof(f10165,plain,
( spl0_104
| spl0_2
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f10083,f9648,f8,f10163]) ).
fof(f10166,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,implies(X1,X2))))
| ~ spl0_104 ),
inference(resolution,[],[f10164,f19]) ).
fof(f10190,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X1,implies(X2,X1))) )
| ~ spl0_104 ),
inference(resolution,[],[f10164,f1]) ).
fof(f10252,definition,
( spl0_105
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f10253,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X1)))
| ~ spl0_105 ),
inference(avatar_component_clause,[],[f10252]) ).
fof(f10254,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0)))
| ~ spl0_102
| ~ spl0_104 ),
inference(resolution,[],[f10190,f9649]) ).
fof(f10503,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))))
| ~ spl0_41
| ~ spl0_101 ),
inference(resolution,[],[f10148,f791]) ).
fof(f10791,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,implies(X1,X2))) )
| ~ spl0_104 ),
inference(resolution,[],[f10166,f1]) ).
fof(f11046,definition,
( spl0_108
<=> ! [X0,X1,X3] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,implies(X3,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f11047,plain,
( ! [X3,X0,X1] :
( is_a_theorem(implies(X0,implies(X3,X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f11046]) ).
fof(f12370,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))) )
| ~ spl0_41
| ~ spl0_101 ),
inference(resolution,[],[f10503,f1]) ).
fof(f12694,plain,
( spl0_105
| ~ spl0_102
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f10254,f10163,f9648,f10252]) ).
fof(f13149,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X3,implies(X0,X2))) )
| ~ spl0_27 ),
inference(resolution,[],[f282,f1]) ).
fof(f13192,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X2,implies(X0,implies(X3,X1))))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_27
| ~ spl0_105 ),
inference(resolution,[],[f13149,f10253]) ).
fof(f13298,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X2)
| is_a_theorem(implies(X0,implies(X3,X1))) )
| ~ spl0_27
| ~ spl0_105 ),
inference(resolution,[],[f13192,f1]) ).
fof(f13335,plain,
( spl0_2
| spl0_108
| ~ spl0_27
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f13298,f10252,f278,f11046,f8]) ).
fof(f13371,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X0,X2))))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_27 ),
inference(resolution,[],[f279,f19]) ).
fof(f13381,plain,
( spl0_26
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f6701,f559,f266]) ).
fof(f13416,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(implies(X2,X1)) )
| ~ spl0_108 ),
inference(resolution,[],[f11047,f1]) ).
fof(f13503,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(X0,X2),implies(X3,implies(X4,X2))))) )
| ~ spl0_41
| ~ spl0_108 ),
inference(resolution,[],[f13416,f783]) ).
fof(f13722,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X3,implies(X0,X2))) )
| ~ spl0_27 ),
inference(resolution,[],[f13371,f1]) ).
fof(f14002,definition,
( spl0_118
<=> ! [X4,X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f14003,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3))))
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f14002]) ).
fof(f14004,plain,
( spl0_118
| spl0_2
| ~ spl0_41
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f12370,f9599,f782,f8,f14002]) ).
fof(f14005,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2))) )
| ~ spl0_118 ),
inference(resolution,[],[f14003,f1]) ).
fof(f14041,definition,
( spl0_119
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2))) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f14042,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2)))
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f14041]) ).
fof(f14043,plain,
( spl0_119
| spl0_2
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f14005,f14002,f8,f14041]) ).
fof(f14044,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) )
| ~ spl0_119 ),
inference(resolution,[],[f14042,f1]) ).
fof(f14053,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(implies(implies(X0,X3),X0),X1))))
| ~ spl0_119 ),
inference(resolution,[],[f14042,f19]) ).
fof(f14079,definition,
( spl0_120
<=> ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f14080,plain,
( ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1))
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f14079]) ).
fof(f14081,plain,
( spl0_120
| spl0_2
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f14044,f14041,f8,f14079]) ).
fof(f14099,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(X0) )
| ~ spl0_120 ),
inference(resolution,[],[f14080,f1]) ).
fof(f14107,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X1)))
| is_a_theorem(implies(X3,implies(X0,X1))) )
| ~ spl0_27
| ~ spl0_120 ),
inference(resolution,[],[f14080,f13722]) ).
fof(f14118,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,implies(X1,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_27
| ~ spl0_120 ),
inference(resolution,[],[f14099,f13371]) ).
fof(f15785,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X2,implies(implies(implies(X0,X3),X0),X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_119 ),
inference(resolution,[],[f14053,f1]) ).
fof(f16117,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X2),X3),implies(X2,X3))))
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f14107,f10166]) ).
fof(f16919,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2)))
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f16117,f14099]) ).
fof(f16982,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) )
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f16919,f1]) ).
fof(f17037,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X3,implies(X0,X2)))))
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f16982,f2]) ).
fof(f17616,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X2),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_119
| ~ spl0_120 ),
inference(resolution,[],[f15785,f14099]) ).
fof(f17707,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_119
| ~ spl0_120 ),
inference(resolution,[],[f17616,f14099]) ).
fof(f17738,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X2),X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) )
| ~ spl0_119
| ~ spl0_120 ),
inference(resolution,[],[f17616,f1]) ).
fof(f17806,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(X2,X0)) )
| ~ spl0_27
| ~ spl0_119
| ~ spl0_120 ),
inference(resolution,[],[f17707,f13371]) ).
fof(f32759,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X3,X1))))
| ~ is_a_theorem(X2) )
| ~ spl0_27
| ~ spl0_96
| ~ spl0_120 ),
inference(resolution,[],[f14118,f9133]) ).
fof(f39146,plain,
( spl0_55
| ~ spl0_41
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f13503,f11046,f782,f2231]) ).
fof(f51104,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),X2)))
| ~ is_a_theorem(X0) )
| ~ spl0_27
| ~ spl0_96
| ~ spl0_120 ),
inference(resolution,[],[f32759,f14118]) ).
fof(f51606,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(implies(X2,X3),X3)))) )
| ~ spl0_27
| ~ spl0_96
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f51104,f10791]) ).
fof(f51921,definition,
( spl0_187
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(implies(X2,X3),X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f51922,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(X2,implies(implies(X2,X3),X3))))
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f51921]) ).
fof(f51923,plain,
( spl0_187
| spl0_2
| ~ spl0_27
| ~ spl0_96
| ~ spl0_104
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f51606,f14079,f10163,f9132,f278,f8,f51921]) ).
fof(f51951,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(implies(X0,X1),X1)),X2))
| is_a_theorem(X2) )
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(resolution,[],[f51922,f17738]) ).
fof(f70642,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f17037,f14118]) ).
fof(f70757,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,X0),implies(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_27
| ~ spl0_104
| ~ spl0_120 ),
inference(resolution,[],[f70642,f1]) ).
fof(f71481,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X0,X1),X1),X2))
| is_a_theorem(implies(X0,X2)) )
| ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(resolution,[],[f70757,f51951]) ).
fof(f72247,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(resolution,[],[f71481,f17806]) ).
fof(f72518,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(resolution,[],[f72247,f70642]) ).
fof(f74368,plain,
( $false
| ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(resolution,[],[f72518,f3]) ).
fof(f74461,plain,
( ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(avatar_contradiction_clause,[],[f74368]) ).
cnf(s11,plain,
~ spl0_2,
inference(sat_conversion,[],[f16]) ).
cnf(s78,plain,
( spl0_2
| spl0_12 ),
inference(sat_conversion,[],[f98]) ).
cnf(s209,plain,
( spl0_2
| ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f280]) ).
cnf(s397,plain,
( spl0_2
| ~ spl0_12
| spl0_36 ),
inference(sat_conversion,[],[f550]) ).
cnf(s563,plain,
( spl0_2
| ~ spl0_36
| spl0_41 ),
inference(sat_conversion,[],[f784]) ).
cnf(s682,plain,
( spl0_2
| ~ spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f945]) ).
cnf(s1094,plain,
( spl0_2
| spl0_37
| ~ spl0_46 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s1316,plain,
( spl0_2
| spl0_45
| ~ spl0_54 ),
inference(sat_conversion,[],[f1876]) ).
cnf(s3617,plain,
( spl0_2
| ~ spl0_12
| ~ spl0_36
| spl0_71 ),
inference(sat_conversion,[],[f5332]) ).
cnf(s4595,plain,
( spl0_2
| ~ spl0_12
| ~ spl0_36
| spl0_54
| ~ spl0_71 ),
inference(sat_conversion,[],[f6698]) ).
cnf(s6138,plain,
( spl0_2
| ~ spl0_55
| spl0_96 ),
inference(sat_conversion,[],[f9134]) ).
cnf(s6380,plain,
( spl0_2
| ~ spl0_36
| ~ spl0_37
| spl0_98 ),
inference(sat_conversion,[],[f9454]) ).
cnf(s6399,plain,
( spl0_2
| ~ spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f9503]) ).
cnf(s6416,plain,
( spl0_2
| ~ spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f9552]) ).
cnf(s6427,plain,
( spl0_2
| ~ spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f9601]) ).
cnf(s6437,plain,
( spl0_2
| ~ spl0_101
| spl0_102 ),
inference(sat_conversion,[],[f9650]) ).
cnf(s6687,plain,
( spl0_2
| ~ spl0_102
| spl0_104 ),
inference(sat_conversion,[],[f10165]) ).
cnf(s8041,plain,
( ~ spl0_102
| ~ spl0_104
| spl0_105 ),
inference(sat_conversion,[],[f12694]) ).
cnf(s8666,plain,
( spl0_2
| ~ spl0_27
| ~ spl0_105
| spl0_108 ),
inference(sat_conversion,[],[f13335]) ).
cnf(s8732,plain,
( spl0_26
| ~ spl0_37 ),
inference(sat_conversion,[],[f13381]) ).
cnf(s9089,plain,
( spl0_2
| ~ spl0_41
| ~ spl0_101
| spl0_118 ),
inference(sat_conversion,[],[f14004]) ).
cnf(s9099,plain,
( spl0_2
| ~ spl0_118
| spl0_119 ),
inference(sat_conversion,[],[f14043]) ).
cnf(s9108,plain,
( spl0_2
| ~ spl0_119
| spl0_120 ),
inference(sat_conversion,[],[f14081]) ).
cnf(s18829,plain,
( ~ spl0_41
| spl0_55
| ~ spl0_108 ),
inference(sat_conversion,[],[f39146]) ).
cnf(s25618,plain,
( spl0_2
| ~ spl0_27
| ~ spl0_96
| ~ spl0_104
| ~ spl0_120
| spl0_187 ),
inference(sat_conversion,[],[f51923]) ).
cnf(s35014,plain,
( ~ spl0_27
| ~ spl0_104
| ~ spl0_119
| ~ spl0_120
| ~ spl0_187 ),
inference(sat_conversion,[],[f74461]) ).
cnf(s35058,plain,
spl0_12,
inference(rat,[],[s78,s11]) ).
cnf(s35063,plain,
spl0_36,
inference(rat,[],[s397,s11,s35058]) ).
cnf(s35070,plain,
spl0_41,
inference(rat,[],[s563,s11,s35063]) ).
cnf(s35073,plain,
spl0_71,
inference(rat,[],[s3617,s35058,s11,s35063]) ).
cnf(s35084,plain,
spl0_54,
inference(rat,[],[s4595,s35063,s35058,s11,s35073]) ).
cnf(s35089,plain,
spl0_45,
inference(rat,[],[s1316,s11,s35084]) ).
cnf(s35091,plain,
spl0_46,
inference(rat,[],[s682,s11,s35089]) ).
cnf(s35093,plain,
spl0_37,
inference(rat,[],[s1094,s11,s35091]) ).
cnf(s35094,plain,
spl0_26,
inference(rat,[],[s8732,s35093]) ).
cnf(s35098,plain,
spl0_98,
inference(rat,[],[s6380,s35063,s11,s35093]) ).
cnf(s35100,plain,
spl0_27,
inference(rat,[],[s209,s11,s35094]) ).
cnf(s35103,plain,
spl0_99,
inference(rat,[],[s6399,s11,s35098]) ).
cnf(s35108,plain,
spl0_100,
inference(rat,[],[s6416,s11,s35103]) ).
cnf(s35110,plain,
spl0_101,
inference(rat,[],[s6427,s11,s35108]) ).
cnf(s35112,plain,
spl0_102,
inference(rat,[],[s6437,s11,s35110]) ).
cnf(s35113,plain,
spl0_118,
inference(rat,[],[s9089,s35070,s11,s35110]) ).
cnf(s35115,plain,
spl0_104,
inference(rat,[],[s6687,s11,s35112]) ).
cnf(s35116,plain,
spl0_119,
inference(rat,[],[s9099,s11,s35113]) ).
cnf(s35118,plain,
spl0_105,
inference(rat,[],[s8041,s35112,s35115]) ).
cnf(s35120,plain,
spl0_120,
inference(rat,[],[s9108,s11,s35116]) ).
cnf(s35122,plain,
spl0_108,
inference(rat,[],[s8666,s35100,s11,s35118]) ).
cnf(s35169,plain,
~ spl0_187,
inference(rat,[],[s35014,s35116,s35115,s35100,s35120]) ).
cnf(s35170,plain,
~ spl0_96,
inference(rat,[],[s25618,s35169,s35115,s35100,s11,s35120]) ).
cnf(s35172,plain,
spl0_55,
inference(rat,[],[s18829,s35070,s35122]) ).
cnf(s35175,plain,
$false,
inference(rat,[],[s6138,s11,s35170,s35172]) ).
fof(f74462,plain,
$false,
inference(avatar_sat_refutation,[],[s35175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL093-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 15:22:24 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.46/3.11 % (1368321)Will run a generic schedule for satisfiability detection.
% 18.46/3.11 % (1368331)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2207115716:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 18.46/3.11 % (1368327)% WARNING: option uhcvi not known.
% 18.46/3.11 % (1368326)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2524143275_2999 on theBenchmark for (2999ds/0Mi)
% 18.46/3.11 % (1368328)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2462086925:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 18.46/3.11 % (1368327)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2898173500:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 18.46/3.11 % (1368329)dis+10_1_sil=32000:sp=arity:random_seed=597808149:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 18.46/3.11 % (1368330)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1650415250:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 18.46/3.11 % (1368332)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=136428001:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 18.46/3.11 % TRYING [1]
% 18.46/3.11 % TRYING [2]
% 18.46/3.11 % TRYING [3]
% 18.46/3.11 % TRYING [4]
% 18.46/3.11 % (1368331)Instruction limit reached!
% 18.46/3.11 % (1368331)------------------------------
% 18.46/3.11 % (1368331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.46/3.11 % (1368331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.11 % (1368331)CaDiCaL version: 2.1.3
% 18.46/3.11 % (1368331)Termination reason: Instruction limit
% 18.46/3.11 % (1368331)Termination phase: Saturation
% 18.46/3.11 % (1368331)Time elapsed: 0.045 s
% 18.46/3.11 % (1368331)Peak memory usage: 12 MB
% 18.46/3.11 % (1368331)Instructions burned: 131 (million)
% 18.46/3.11 % (1368340)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1714666657:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 18.46/3.11 % TRYING [1]
% 18.46/3.11 % TRYING [2]
% 18.46/3.11 % TRYING [3]
% 18.46/3.11 % TRYING [4]
% 18.46/3.11 % (1368329)Instruction limit reached!
% 18.46/3.11 % (1368329)------------------------------
% 18.46/3.11 % (1368329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.46/3.11 % (1368329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.11 % (1368329)CaDiCaL version: 2.1.3
% 18.46/3.11 % (1368329)Termination reason: Instruction limit
% 18.46/3.11 % (1368329)Termination phase: Saturation
% 18.46/3.11 % (1368329)Time elapsed: 0.066 s
% 18.46/3.11 % (1368329)Peak memory usage: 12 MB
% 18.46/3.11 % (1368329)Instructions burned: 104 (million)
% 18.46/3.11 % (1368330)Instruction limit reached!
% 18.46/3.11 % (1368330)------------------------------
% 18.46/3.11 % (1368330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.46/3.11 % (1368330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.11 % (1368330)CaDiCaL version: 2.1.3
% 18.46/3.11 % (1368330)Termination reason: Instruction limit
% 18.46/3.11 % (1368330)Termination phase: Saturation
% 18.46/3.11 % (1368330)Time elapsed: 0.073 s
% 18.46/3.11 % (1368330)Peak memory usage: 11 MB
% 18.46/3.11 % (1368330)Instructions burned: 122 (million)
% 18.46/3.11 % (1368342)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3505355660:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 18.46/3.11 % (1368343)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3941977477:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 18.46/3.11 % (1368332)Instruction limit reached!
% 18.46/3.11 % (1368332)------------------------------
% 18.46/3.11 % (1368332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.46/3.11 % (1368332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.11 % (1368332)CaDiCaL version: 2.1.3
% 18.46/3.11 % (1368332)Termination reason: Instruction limit
% 18.46/3.11 % (1368332)Termination phase: Saturation
% 18.46/3.11 % (1368332)Time elapsed: 0.097 s
% 18.46/3.11 % (1368332)Peak memory usage: 12 MB
% 18.46/3.11 % (1368332)Instructions burned: 160 (million)
% 18.46/3.11 % (1368346)ott-21_1_sil=16000:fs=off:random_seed=3447535846:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 18.46/3.11 % (1368342)Instruction limit reached!
% 18.46/3.11 % (1368342)------------------------------
% 18.46/3.11 % (1368342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.46/3.11 % (1368342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368342)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368342)Termination reason: Instruction limit
% 14.30/3.21 % (1368342)Termination phase: Saturation
% 14.30/3.21 % (1368342)Time elapsed: 0.077 s
% 14.30/3.21 % (1368342)Peak memory usage: 11 MB
% 14.30/3.21 % (1368342)Instructions burned: 131 (million)
% 14.30/3.21 % (1368348)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3476702967:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 14.30/3.21 % (1368346)Instruction limit reached!
% 14.30/3.21 % (1368346)------------------------------
% 14.30/3.21 % (1368346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368346)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368346)Termination reason: Instruction limit
% 14.30/3.21 % (1368346)Termination phase: Saturation
% 14.30/3.21 % (1368346)Time elapsed: 0.104 s
% 14.30/3.21 % (1368346)Peak memory usage: 12 MB
% 14.30/3.21 % (1368346)Instructions burned: 181 (million)
% 14.30/3.21 % (1368350)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=923578591:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 14.30/3.21 % TRYING [1]
% 14.30/3.21 % TRYING [2]
% 14.30/3.21 % TRYING [3]
% 14.30/3.21 % TRYING [4]
% 14.30/3.21 % (1368340)Instruction limit reached!
% 14.30/3.21 % (1368340)------------------------------
% 14.30/3.21 % (1368340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368340)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368340)Termination reason: Instruction limit
% 14.30/3.21 % (1368340)Termination phase: Finite model building SAT solving
% 14.30/3.21 % (1368340)Time elapsed: 0.225 s
% 14.30/3.21 % (1368340)Peak memory usage: 12 MB
% 14.30/3.21 % (1368340)Instructions burned: 716 (million)
% 14.30/3.21 % (1368352)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=31360458:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 14.30/3.21 % (1368348)Instruction limit reached!
% 14.30/3.21 % (1368348)------------------------------
% 14.30/3.21 % (1368348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368348)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368348)Termination reason: Instruction limit
% 14.30/3.21 % (1368348)Termination phase: Saturation
% 14.30/3.21 % (1368348)Time elapsed: 0.279 s
% 14.30/3.21 % (1368348)Peak memory usage: 15 MB
% 14.30/3.21 % (1368348)Instructions burned: 477 (million)
% 14.30/3.21 % (1368354)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4271674555:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 14.30/3.21 % (1368343)Instruction limit reached!
% 14.30/3.21 % (1368343)------------------------------
% 14.30/3.21 % (1368343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368343)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368343)Termination reason: Instruction limit
% 14.30/3.21 % (1368343)Termination phase: Saturation
% 14.30/3.21 % (1368343)Time elapsed: 0.395 s
% 14.30/3.21 % (1368343)Peak memory usage: 19 MB
% 14.30/3.21 % (1368343)Instructions burned: 685 (million)
% 14.30/3.21 % (1368356)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3701976732:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 14.30/3.21 % TRYING [14]
% 14.30/3.21 % TRYING [5]
% 14.30/3.21 % TRYING [5]
% 14.30/3.21 % (1368352)Instruction limit reached!
% 14.30/3.21 % (1368352)------------------------------
% 14.30/3.21 % (1368352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368352)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368352)Termination reason: Instruction limit
% 14.30/3.21 % (1368352)Termination phase: Saturation
% 14.30/3.21 % (1368352)Time elapsed: 0.389 s
% 14.30/3.21 % (1368352)Peak memory usage: 25 MB
% 14.30/3.21 % (1368352)Instructions burned: 1184 (million)
% 14.30/3.21 % (1368358)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2019438679:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 14.30/3.21 % (1368350)Instruction limit reached!
% 14.30/3.21 % (1368350)------------------------------
% 14.30/3.21 % (1368350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368350)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368350)Termination reason: Instruction limit
% 14.30/3.21 % (1368350)Termination phase: Finite model building SAT solving
% 14.30/3.21 % (1368350)Time elapsed: 0.522 s
% 14.30/3.21 % (1368350)Peak memory usage: 12 MB
% 14.30/3.21 % (1368350)Instructions burned: 865 (million)
% 14.30/3.21 % (1368360)fmb+10_1_sil=64000:random_seed=2491314389:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 14.30/3.21 % TRYING [1]
% 14.30/3.21 % TRYING [2]
% 14.30/3.21 % TRYING [3]
% 14.30/3.21 % (1368354)Instruction limit reached!
% 14.30/3.21 % (1368354)------------------------------
% 14.30/3.21 % (1368354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368354)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368354)Termination reason: Instruction limit
% 14.30/3.21 % (1368354)Termination phase: Finite model building constraint generation
% 14.30/3.21 % (1368354)Time elapsed: 0.306 s
% 14.30/3.21 % (1368354)Peak memory usage: 68 MB
% 14.30/3.21 % (1368354)Instructions burned: 889 (million)
% 14.30/3.21 % TRYING [4]
% 14.30/3.21 % (1368362)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3631005257:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 14.30/3.21 % TRYING [20]
% 14.30/3.21 % (1368356)Instruction limit reached!
% 14.30/3.21 % (1368356)------------------------------
% 14.30/3.21 % (1368356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368356)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368356)Termination reason: Instruction limit
% 14.30/3.21 % (1368356)Termination phase: Saturation
% 14.30/3.21 % (1368356)Time elapsed: 0.387 s
% 14.30/3.21 % (1368356)Peak memory usage: 15 MB
% 14.30/3.21 % (1368356)Instructions burned: 692 (million)
% 14.30/3.21 % (1368364)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2019859170:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 14.30/3.21 % TRYING [8]
% 14.30/3.21 % (1368358)Instruction limit reached!
% 14.30/3.21 % (1368358)------------------------------
% 14.30/3.21 % (1368358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368358)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368358)Termination reason: Instruction limit
% 14.30/3.21 % (1368358)Termination phase: Saturation
% 14.30/3.21 % (1368358)Time elapsed: 0.261 s
% 14.30/3.21 % (1368358)Peak memory usage: 16 MB
% 14.30/3.21 % (1368358)Instructions burned: 879 (million)
% 14.30/3.21 % (1368367)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=30276202:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 14.30/3.21 % TRYING [5]
% 14.30/3.21 % (1368364)Instruction limit reached!
% 14.30/3.21 % (1368364)------------------------------
% 14.30/3.21 % (1368364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368364)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368364)Termination reason: Instruction limit
% 14.30/3.21 % (1368364)Termination phase: Finite model building SAT solving
% 14.30/3.21 % (1368364)Time elapsed: 0.495 s
% 14.30/3.21 % (1368364)Peak memory usage: 40 MB
% 14.30/3.21 % (1368364)Instructions burned: 921 (million)
% 14.30/3.21 % (1368369)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=882589416:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 14.30/3.21 % (1368369)Instruction limit reached!
% 14.30/3.21 % (1368369)------------------------------
% 14.30/3.21 % (1368369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.21 % (1368369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.21 % (1368369)CaDiCaL version: 2.1.3
% 14.30/3.21 % (1368369)Termination reason: Instruction limit
% 14.30/3.21 % (1368369)Termination phase: Saturation
% 14.30/3.21 % (1368369)Time elapsed: 0.799 s
% 14.30/3.21 % (1368369)Peak memory usage: 24 MB
% 14.30/3.21 % (1368369)Instructions burned: 1472 (million)
% 14.30/3.21 % (1368371)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2602490488:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 14.30/3.21 % TRYING [77]
% 14.30/3.21 % (1368367)Instruction limit reached!
% 14.30/3.21 % (1368367)------------------------------
% 14.30/3.22 % (1368367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.22 % (1368367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.22 % (1368367)CaDiCaL version: 2.1.3
% 14.30/3.22 % (1368367)Termination reason: Instruction limit
% 14.30/3.22 % (1368367)Termination phase: Saturation
% 14.30/3.22 % (1368367)Time elapsed: 1.686 s
% 14.30/3.22 % (1368367)Peak memory usage: 25 MB
% 14.30/3.22 % (1368367)Instructions burned: 5134 (million)
% 14.30/3.22 % (1368373)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2459948047:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 14.30/3.22 % TRYING [16]
% 14.30/3.22 % (1368328) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1368321-1368328"...
% 14.30/3.22 % (1368328)...printing done.
% 14.30/3.22 % (1368328)Refutation found. Thanks to Tanya!
% 14.30/3.22 % SZS status Unsatisfiable for theBenchmark
% 14.30/3.22 % SZS output start Proof for theBenchmark
% See solution above
% 14.30/3.22 % (1368328)------------------------------
% 14.30/3.22 % (1368328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.30/3.22 % (1368328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.22 % (1368328)CaDiCaL version: 2.1.3
% 14.30/3.22 % (1368328)Termination reason: Refutation
% 14.30/3.22 % (1368328)Time elapsed: 2.709 s
% 14.30/3.22 % (1368328)Peak memory usage: 37 MB
% 14.30/3.22 % (1368328)Instructions burned: 5428 (million)
% 14.30/3.22 % (1368321)Success in time 2.789 s
% 14.30/3.22 % Vampire exiting
%------------------------------------------------------------------------------