%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL124-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:17 AM UTC 2026
% Result : Unsatisfiable 20.32s 3.73s
% Output : Refutation 21.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 53
% Syntax : Number of formulae : 305 ( 58 unt; 50 def)
% Number of atoms : 894 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1298 ( 709 ~; 539 |; 0 &)
% ( 50 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 52 ( 51 usr; 51 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 335 ( 0 sgn 335 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lg_2) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))),equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_lg_5) ).
fof(f5,definition,
( spl0_1
<=> is_a_theorem(equivalent(equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))),equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f)))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( ~ is_a_theorem(equivalent(equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))),equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f))))
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f8,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f3,f5]) ).
fof(f10,definition,
( spl0_2
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f10]) ).
fof(f12,plain,
spl0_2,
inference(avatar_split_clause,[],[f1,f10]) ).
fof(f14,definition,
( spl0_3
<=> ! [X0,X3,X2,X1] : is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f15,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3))))))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f14]) ).
fof(f16,plain,
spl0_3,
inference(avatar_split_clause,[],[f2,f14]) ).
fof(f17,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3))))) )
| ~ spl0_2
| ~ spl0_3 ),
inference(resolution,[],[f15,f11]) ).
fof(f19,definition,
( spl0_4
<=> ! [X0,X3,X2,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f20,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))))
| ~ is_a_theorem(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f19]) ).
fof(f21,plain,
( spl0_4
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f17,f14,f10,f19]) ).
fof(f22,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X0)
| is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))) )
| ~ spl0_2
| ~ spl0_4 ),
inference(resolution,[],[f20,f11]) ).
fof(f23,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))) )
| ~ spl0_2
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f22]) ).
fof(f25,definition,
( spl0_5
<=> ! [X2,X1,X3] : is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f26,plain,
( ! [X2,X3,X1] : is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X1,X3),equivalent(X2,X3))))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f25]) ).
fof(f28,definition,
( spl0_6
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f29,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f28]) ).
fof(f30,plain,
( spl0_5
| spl0_6
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f23,f19,f10,f28,f25]) ).
fof(f31,plain,
( $false
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f29,f15]) ).
fof(f33,plain,
( ~ spl0_3
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f31]) ).
fof(f34,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2))) )
| ~ spl0_2
| ~ spl0_5 ),
inference(resolution,[],[f26,f11]) ).
fof(f36,definition,
( spl0_7
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f37,plain,
( ! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f38,plain,
( spl0_7
| ~ spl0_2
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f34,f25,f10,f36]) ).
fof(f39,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,X2))
| is_a_theorem(equivalent(X1,X2)) )
| ~ spl0_2
| ~ spl0_7 ),
inference(resolution,[],[f37,f11]) ).
fof(f41,definition,
( spl0_8
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,X2))
| is_a_theorem(equivalent(X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f42,plain,
( ! [X2,X0,X1] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f41]) ).
fof(f43,plain,
( spl0_8
| ~ spl0_2
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f39,f36,f10,f41]) ).
fof(f44,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))))) )
| spl0_1
| ~ spl0_8 ),
inference(resolution,[],[f42,f7]) ).
fof(f45,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| is_a_theorem(X1) )
| ~ spl0_2
| ~ spl0_8 ),
inference(resolution,[],[f42,f11]) ).
fof(f47,definition,
( spl0_9
<=> ! [X0] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f48,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(a,equivalent(f,c)),equivalent(equivalent(b,equivalent(f,e)),f))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f)))))) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f47]) ).
fof(f49,plain,
( spl0_9
| spl0_1
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f44,f41,f5,f47]) ).
fof(f50,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c)))) )
| ~ spl0_7
| ~ spl0_9 ),
inference(resolution,[],[f48,f37]) ).
fof(f53,definition,
( spl0_10
<=> ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f54,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c)))) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f55,plain,
( spl0_10
| ~ spl0_7
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f50,f47,f36,f53]) ).
fof(f56,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)))) )
| ~ spl0_8
| ~ spl0_10 ),
inference(resolution,[],[f54,f42]) ).
fof(f72,definition,
( spl0_12
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f73,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f))))
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(f,c)))) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f74,plain,
( spl0_12
| ~ spl0_8
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f56,f53,f41,f72]) ).
fof(f86,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7
| ~ spl0_12 ),
inference(resolution,[],[f73,f37]) ).
fof(f115,definition,
( spl0_18
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f116,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f117,plain,
( spl0_18
| ~ spl0_7
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f86,f72,f36,f115]) ).
fof(f123,definition,
( spl0_20
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| is_a_theorem(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f124,plain,
( ! [X2,X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f125,plain,
( spl0_20
| ~ spl0_2
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f45,f41,f10,f123]) ).
fof(f140,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_7
| ~ spl0_18 ),
inference(resolution,[],[f116,f37]) ).
fof(f175,definition,
( spl0_26
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f176,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(f,c))))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f177,plain,
( spl0_26
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f140,f115,f36,f175]) ).
fof(f207,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_5
| ~ spl0_26 ),
inference(resolution,[],[f176,f26]) ).
fof(f211,definition,
( spl0_31
<=> ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f212,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f)),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f213,plain,
( spl0_31
| ~ spl0_5
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f207,f175,f25,f211]) ).
fof(f214,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f)))) )
| ~ spl0_8
| ~ spl0_31 ),
inference(resolution,[],[f212,f42]) ).
fof(f461,definition,
( spl0_51
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f462,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,f),equivalent(equivalent(b,equivalent(f,e)),f))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( spl0_51
| ~ spl0_8
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f214,f211,f41,f461]) ).
fof(f487,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(b,equivalent(f,e))),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_5
| ~ spl0_51 ),
inference(resolution,[],[f462,f26]) ).
fof(f492,definition,
( spl0_55
<=> ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(b,equivalent(f,e))),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f493,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(b,equivalent(f,e))),equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f494,plain,
( spl0_55
| ~ spl0_5
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f487,f461,f25,f492]) ).
fof(f495,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(b,equivalent(f,e))))) )
| ~ spl0_8
| ~ spl0_55 ),
inference(resolution,[],[f493,f42]) ).
fof(f498,definition,
( spl0_56
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(b,equivalent(f,e))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f499,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,equivalent(b,equivalent(f,e)))))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( spl0_56
| ~ spl0_8
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f495,f492,f41,f498]) ).
fof(f506,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X2,equivalent(X1,equivalent(b,equivalent(f,e)))))
| ~ is_a_theorem(equivalent(X2,X0)) )
| ~ spl0_8
| ~ spl0_56 ),
inference(resolution,[],[f499,f42]) ).
fof(f1292,definition,
( spl0_122
<=> ! [X0] : ~ is_a_theorem(equivalent(X0,a)) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1293,plain,
( ! [X0] : ~ is_a_theorem(equivalent(X0,a))
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1403,definition,
( spl0_126
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X2,equivalent(X1,equivalent(b,equivalent(f,e)))))
| ~ is_a_theorem(equivalent(X2,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1404,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(X2,equivalent(X1,equivalent(b,equivalent(f,e)))))
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a)) )
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f1403]) ).
fof(f1405,plain,
( spl0_126
| ~ spl0_8
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f506,f498,f41,f1403]) ).
fof(f1464,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,b),X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a)) )
| ~ spl0_5
| ~ spl0_126 ),
inference(resolution,[],[f1404,f26]) ).
fof(f1483,definition,
( spl0_137
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,b),X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1484,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(a,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(X0,b),X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a)) )
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f1483]) ).
fof(f1485,plain,
( spl0_137
| ~ spl0_5
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1464,f1403,f25,f1483]) ).
fof(f1486,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,b),equivalent(X0,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_7
| ~ spl0_137 ),
inference(resolution,[],[f1484,f37]) ).
fof(f1501,definition,
( spl0_138
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,b),equivalent(X0,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(X0,a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1502,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,b),equivalent(X0,equivalent(b,equivalent(c,equivalent(e,f))))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1501]) ).
fof(f1503,plain,
( spl0_138
| ~ spl0_7
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1486,f1483,f36,f1501]) ).
fof(f1512,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a)) )
| ~ spl0_5
| ~ spl0_138 ),
inference(resolution,[],[f1502,f26]) ).
fof(f1517,definition,
( spl0_141
<=> ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1518,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a)) )
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1519,plain,
( spl0_141
| ~ spl0_5
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1512,f1501,f25,f1517]) ).
fof(f1520,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c))) )
| ~ spl0_8
| ~ spl0_141 ),
inference(resolution,[],[f1518,f42]) ).
fof(f1524,definition,
( spl0_142
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c))) ) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1525,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(c,equivalent(e,f))),a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(X1,a)) )
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f1524]) ).
fof(f1526,plain,
( spl0_142
| ~ spl0_8
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1520,f1517,f41,f1524]) ).
fof(f1527,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X2,a))
| ~ is_a_theorem(equivalent(X2,equivalent(X0,equivalent(c,equivalent(e,f))))) )
| ~ spl0_8
| ~ spl0_142 ),
inference(resolution,[],[f1525,f42]) ).
fof(f1644,definition,
( spl0_150
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X2,a))
| ~ is_a_theorem(equivalent(X2,equivalent(X0,equivalent(c,equivalent(e,f))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1645,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(X2,equivalent(X0,equivalent(c,equivalent(e,f)))))
| ~ is_a_theorem(equivalent(X2,a))
| ~ is_a_theorem(equivalent(X1,a)) )
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1644]) ).
fof(f1646,plain,
( spl0_150
| ~ spl0_8
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1527,f1524,f41,f1644]) ).
fof(f1659,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,a)) )
| ~ spl0_5
| ~ spl0_150 ),
inference(resolution,[],[f1645,f26]) ).
fof(f1665,definition,
( spl0_153
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1666,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(X1,a)) )
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1667,plain,
( spl0_153
| ~ spl0_5
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1659,f1644,f25,f1665]) ).
fof(f1668,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e)))) )
| ~ spl0_7
| ~ spl0_153 ),
inference(resolution,[],[f1666,f37]) ).
fof(f1677,definition,
( spl0_155
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1678,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X0,equivalent(e,f)),equivalent(f,e))))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f1677]) ).
fof(f1679,plain,
( spl0_155
| ~ spl0_7
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f1668,f1665,f36,f1677]) ).
fof(f1680,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(e,f)))) )
| ~ spl0_7
| ~ spl0_155 ),
inference(resolution,[],[f1678,f37]) ).
fof(f1685,definition,
( spl0_156
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(e,f)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1686,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(e,f))))
| ~ is_a_theorem(equivalent(equivalent(X1,c),a)) )
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1687,plain,
( spl0_156
| ~ spl0_7
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1680,f1677,f36,f1685]) ).
fof(f1691,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) )
| ~ spl0_5
| ~ spl0_156 ),
inference(resolution,[],[f1686,f26]) ).
fof(f1697,definition,
( spl0_157
<=> ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1698,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) )
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f1697]) ).
fof(f1699,plain,
( spl0_157
| ~ spl0_5
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f1691,f1685,f25,f1697]) ).
fof(f1700,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c))) )
| ~ spl0_8
| ~ spl0_157 ),
inference(resolution,[],[f1698,f42]) ).
fof(f1722,definition,
( spl0_159
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c))) ) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1723,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,e),equivalent(f,e)),c)))
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) )
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f1722]) ).
fof(f1724,plain,
( spl0_159
| ~ spl0_8
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f1700,f1697,f41,f1722]) ).
fof(f1725,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,f),c),a))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,e),equivalent(f,e)))) )
| ~ spl0_7
| ~ spl0_159 ),
inference(resolution,[],[f1723,f37]) ).
fof(f1730,definition,
( spl0_160
<=> ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,f),c),a))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,e),equivalent(f,e)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1731,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,e),equivalent(f,e))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X1,f),c),a))
| ~ is_a_theorem(equivalent(equivalent(X0,c),a)) )
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1732,plain,
( spl0_160
| ~ spl0_7
| ~ spl0_159 ),
inference(avatar_split_clause,[],[f1725,f1722,f36,f1730]) ).
fof(f1733,plain,
( ! [X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) )
| ~ spl0_5
| ~ spl0_160 ),
inference(resolution,[],[f1731,f26]) ).
fof(f1738,plain,
( ! [X0] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a))
| ~ spl0_5
| ~ spl0_160 ),
inference(duplicate_literal_removal,[],[f1733]) ).
fof(f1740,definition,
( spl0_161
<=> ! [X0] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a)) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1741,plain,
( ! [X0] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),c),a))
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f1740]) ).
fof(f1742,plain,
( spl0_161
| ~ spl0_5
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f1738,f1730,f25,f1740]) ).
fof(f1745,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),a))) )
| ~ spl0_20
| ~ spl0_161 ),
inference(resolution,[],[f1741,f124]) ).
fof(f1766,definition,
( spl0_164
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),a))) ) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1767,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),a)))
| ~ is_a_theorem(X1) )
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f1766]) ).
fof(f1768,plain,
( spl0_164
| ~ spl0_20
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f1745,f1740,f123,f1766]) ).
fof(f1776,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,f),c))) )
| ~ spl0_7
| ~ spl0_164 ),
inference(resolution,[],[f1767,f37]) ).
fof(f1786,definition,
( spl0_166
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,f),c))) ) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1787,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,f),c)))
| ~ is_a_theorem(X2) )
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1786]) ).
fof(f1788,plain,
( spl0_166
| ~ spl0_7
| ~ spl0_164 ),
inference(avatar_split_clause,[],[f1776,f1766,f36,f1786]) ).
fof(f1811,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,c),a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,f))) )
| ~ spl0_7
| ~ spl0_166 ),
inference(resolution,[],[f1787,f37]) ).
fof(f1832,definition,
( spl0_171
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,c),a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,f))) ) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1833,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,c),a),X2))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,f)))
| ~ is_a_theorem(X2) )
| ~ spl0_171 ),
inference(avatar_component_clause,[],[f1832]) ).
fof(f1834,plain,
( spl0_171
| ~ spl0_7
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f1811,f1786,f36,f1832]) ).
fof(f1888,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7
| ~ spl0_171 ),
inference(resolution,[],[f1833,f37]) ).
fof(f1913,definition,
( spl0_178
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1914,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X2))
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2) )
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f1913]) ).
fof(f1915,plain,
( spl0_178
| ~ spl0_7
| ~ spl0_171 ),
inference(avatar_split_clause,[],[f1888,f1832,f36,f1913]) ).
fof(f2039,plain,
( ! [X0,X4] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X4))
| ~ is_a_theorem(X4) )
| ~ spl0_3
| ~ spl0_178 ),
inference(resolution,[],[f1914,f15]) ).
fof(f2047,definition,
( spl0_187
<=> ! [X4,X0] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X4))
| ~ is_a_theorem(X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f2048,plain,
( ! [X0,X4] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),a),X4))
| ~ is_a_theorem(X4) )
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f2047]) ).
fof(f2049,plain,
( spl0_187
| ~ spl0_3
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f2039,f1913,f14,f2047]) ).
fof(f2052,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),X1),equivalent(a,X1)))
| ~ spl0_5
| ~ spl0_187 ),
inference(resolution,[],[f2048,f26]) ).
fof(f2058,definition,
( spl0_188
<=> ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),X1),equivalent(a,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f2059,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,f),c),X1),equivalent(a,X1)))
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f2058]) ).
fof(f2060,plain,
( spl0_188
| ~ spl0_5
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f2052,f2047,f25,f2058]) ).
fof(f2062,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),X1))) )
| ~ spl0_8
| ~ spl0_188 ),
inference(resolution,[],[f2059,f42]) ).
fof(f2113,definition,
( spl0_198
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f2114,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X2,f),c),X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(a,X1))) )
| ~ spl0_198 ),
inference(avatar_component_clause,[],[f2113]) ).
fof(f2115,plain,
( spl0_198
| ~ spl0_8
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f2062,f2058,f41,f2113]) ).
fof(f2131,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),X1),equivalent(a,equivalent(X1,c))))
| ~ spl0_5
| ~ spl0_198 ),
inference(resolution,[],[f2114,f26]) ).
fof(f2137,definition,
( spl0_200
<=> ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),X1),equivalent(a,equivalent(X1,c)))) ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f2138,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,f),X1),equivalent(a,equivalent(X1,c))))
| ~ spl0_200 ),
inference(avatar_component_clause,[],[f2137]) ).
fof(f2139,plain,
( spl0_200
| ~ spl0_5
| ~ spl0_198 ),
inference(avatar_split_clause,[],[f2131,f2113,f25,f2137]) ).
fof(f2140,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,c))))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X2,f),X1))) )
| ~ spl0_8
| ~ spl0_200 ),
inference(resolution,[],[f2138,f42]) ).
fof(f2203,definition,
( spl0_205
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,c))))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X2,f),X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f2204,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,c))))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X2,f),X1))) )
| ~ spl0_205 ),
inference(avatar_component_clause,[],[f2203]) ).
fof(f2205,plain,
( spl0_205
| ~ spl0_8
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f2140,f2137,f41,f2203]) ).
fof(f2220,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,equivalent(equivalent(X1,f),c))))
| ~ spl0_5
| ~ spl0_205 ),
inference(resolution,[],[f2204,f26]) ).
fof(f2226,definition,
( spl0_208
<=> ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,equivalent(equivalent(X1,f),c)))) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f2227,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,equivalent(equivalent(X1,f),c))))
| ~ spl0_208 ),
inference(avatar_component_clause,[],[f2226]) ).
fof(f2228,plain,
( spl0_208
| ~ spl0_5
| ~ spl0_205 ),
inference(avatar_split_clause,[],[f2220,f2203,f25,f2226]) ).
fof(f2229,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(equivalent(X1,f),c))))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) )
| ~ spl0_8
| ~ spl0_208 ),
inference(resolution,[],[f2227,f42]) ).
fof(f2292,definition,
( spl0_215
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(equivalent(X1,f),c))))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f2293,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(equivalent(X1,f),c))))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) )
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f2292]) ).
fof(f2294,plain,
( spl0_215
| ~ spl0_8
| ~ spl0_208 ),
inference(avatar_split_clause,[],[f2229,f2226,f41,f2292]) ).
fof(f2299,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,f),c)),equivalent(X2,X1)))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_7
| ~ spl0_215 ),
inference(resolution,[],[f2293,f37]) ).
fof(f2335,definition,
( spl0_219
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,f),c)),equivalent(X2,X1)))
| ~ is_a_theorem(equivalent(X0,a)) ) ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f2336,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,f),c)),equivalent(X2,X1)))
| ~ is_a_theorem(equivalent(X0,a)) )
| ~ spl0_219 ),
inference(avatar_component_clause,[],[f2335]) ).
fof(f2337,plain,
( spl0_219
| ~ spl0_7
| ~ spl0_215 ),
inference(avatar_split_clause,[],[f2299,f2292,f36,f2335]) ).
fof(f2338,plain,
( ! [X0] : ~ is_a_theorem(equivalent(X0,a))
| ~ spl0_3
| ~ spl0_219 ),
inference(resolution,[],[f2336,f15]) ).
fof(f2343,plain,
( spl0_122
| ~ spl0_3
| ~ spl0_219 ),
inference(avatar_split_clause,[],[f2338,f2335,f14,f1292]) ).
fof(f2346,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X2,a))) )
| ~ spl0_20
| ~ spl0_122 ),
inference(resolution,[],[f1293,f124]) ).
fof(f2348,definition,
( spl0_220
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X2,a))) ) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f2349,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,a)))
| ~ is_a_theorem(X1) )
| ~ spl0_220 ),
inference(avatar_component_clause,[],[f2348]) ).
fof(f2350,plain,
( spl0_220
| ~ spl0_20
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f2346,f1292,f123,f2348]) ).
fof(f2358,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7
| ~ spl0_220 ),
inference(resolution,[],[f2349,f37]) ).
fof(f2364,definition,
( spl0_221
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f2365,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X2))
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2) )
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f2364]) ).
fof(f2366,plain,
( spl0_221
| ~ spl0_7
| ~ spl0_220 ),
inference(avatar_split_clause,[],[f2358,f2348,f36,f2364]) ).
fof(f2374,plain,
( ! [X0,X4] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X4))
| ~ is_a_theorem(X4) )
| ~ spl0_3
| ~ spl0_221 ),
inference(resolution,[],[f2365,f15]) ).
fof(f2382,definition,
( spl0_222
<=> ! [X4,X0] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X4))
| ~ is_a_theorem(X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f2383,plain,
( ! [X0,X4] :
( ~ is_a_theorem(equivalent(equivalent(X0,a),X4))
| ~ is_a_theorem(X4) )
| ~ spl0_222 ),
inference(avatar_component_clause,[],[f2382]) ).
fof(f2384,plain,
( spl0_222
| ~ spl0_3
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2374,f2364,f14,f2382]) ).
fof(f2387,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,X1)))
| ~ spl0_5
| ~ spl0_222 ),
inference(resolution,[],[f2383,f26]) ).
fof(f2393,definition,
( spl0_223
<=> ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f2394,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(a,X1)))
| ~ spl0_223 ),
inference(avatar_component_clause,[],[f2393]) ).
fof(f2395,plain,
( spl0_223
| ~ spl0_5
| ~ spl0_222 ),
inference(avatar_split_clause,[],[f2387,f2382,f25,f2393]) ).
fof(f2397,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) )
| ~ spl0_8
| ~ spl0_223 ),
inference(resolution,[],[f2394,f42]) ).
fof(f2417,definition,
( spl0_228
<=> ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f2418,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ is_a_theorem(equivalent(X0,equivalent(X2,X1))) )
| ~ spl0_228 ),
inference(avatar_component_clause,[],[f2417]) ).
fof(f2419,plain,
( spl0_228
| ~ spl0_8
| ~ spl0_223 ),
inference(avatar_split_clause,[],[f2397,f2393,f41,f2417]) ).
fof(f2432,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ spl0_228 ),
inference(factoring,[],[f2418]) ).
fof(f2434,definition,
( spl0_229
<=> ! [X0,X1] : ~ is_a_theorem(equivalent(X0,equivalent(a,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f2435,plain,
( ! [X0,X1] : ~ is_a_theorem(equivalent(X0,equivalent(a,X1)))
| ~ spl0_229 ),
inference(avatar_component_clause,[],[f2434]) ).
fof(f2436,plain,
( spl0_229
| ~ spl0_228 ),
inference(avatar_split_clause,[],[f2432,f2417,f2434]) ).
fof(f2437,plain,
( $false
| ~ spl0_3
| ~ spl0_229 ),
inference(resolution,[],[f2435,f15]) ).
fof(f2442,plain,
( ~ spl0_3
| ~ spl0_229 ),
inference(avatar_contradiction_clause,[],[f2437]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f8]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f12]) ).
cnf(s3,plain,
spl0_3,
inference(sat_conversion,[],[f16]) ).
cnf(s4,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f21]) ).
cnf(s5,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f30]) ).
cnf(s6,plain,
( ~ spl0_3
| ~ spl0_6 ),
inference(sat_conversion,[],[f33]) ).
cnf(s7,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_7 ),
inference(sat_conversion,[],[f38]) ).
cnf(s8,plain,
( ~ spl0_2
| ~ spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f43]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f49]) ).
cnf(s10,plain,
( ~ spl0_7
| ~ spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f55]) ).
cnf(s12,plain,
( ~ spl0_8
| ~ spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f74]) ).
cnf(s18,plain,
( ~ spl0_7
| ~ spl0_12
| spl0_18 ),
inference(sat_conversion,[],[f117]) ).
cnf(s20,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_20 ),
inference(sat_conversion,[],[f125]) ).
cnf(s26,plain,
( ~ spl0_7
| ~ spl0_18
| spl0_26 ),
inference(sat_conversion,[],[f177]) ).
cnf(s30,plain,
( ~ spl0_5
| ~ spl0_26
| spl0_31 ),
inference(sat_conversion,[],[f213]) ).
cnf(s50,plain,
( ~ spl0_8
| ~ spl0_31
| spl0_51 ),
inference(sat_conversion,[],[f463]) ).
cnf(s54,plain,
( ~ spl0_5
| ~ spl0_51
| spl0_55 ),
inference(sat_conversion,[],[f494]) ).
cnf(s55,plain,
( ~ spl0_8
| ~ spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f500]) ).
cnf(s129,plain,
( ~ spl0_8
| ~ spl0_56
| spl0_126 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s140,plain,
( ~ spl0_5
| ~ spl0_126
| spl0_137 ),
inference(sat_conversion,[],[f1485]) ).
cnf(s141,plain,
( ~ spl0_7
| ~ spl0_137
| spl0_138 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s144,plain,
( ~ spl0_5
| ~ spl0_138
| spl0_141 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s145,plain,
( ~ spl0_8
| ~ spl0_141
| spl0_142 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s153,plain,
( ~ spl0_8
| ~ spl0_142
| spl0_150 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s156,plain,
( ~ spl0_5
| ~ spl0_150
| spl0_153 ),
inference(sat_conversion,[],[f1667]) ).
cnf(s158,plain,
( ~ spl0_7
| ~ spl0_153
| spl0_155 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s159,plain,
( ~ spl0_7
| ~ spl0_155
| spl0_156 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s160,plain,
( ~ spl0_5
| ~ spl0_156
| spl0_157 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s162,plain,
( ~ spl0_8
| ~ spl0_157
| spl0_159 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s163,plain,
( ~ spl0_7
| ~ spl0_159
| spl0_160 ),
inference(sat_conversion,[],[f1732]) ).
cnf(s164,plain,
( ~ spl0_5
| ~ spl0_160
| spl0_161 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s167,plain,
( ~ spl0_20
| ~ spl0_161
| spl0_164 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s169,plain,
( ~ spl0_7
| ~ spl0_164
| spl0_166 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s174,plain,
( ~ spl0_7
| ~ spl0_166
| spl0_171 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s181,plain,
( ~ spl0_7
| ~ spl0_171
| spl0_178 ),
inference(sat_conversion,[],[f1915]) ).
cnf(s190,plain,
( ~ spl0_3
| ~ spl0_178
| spl0_187 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s191,plain,
( ~ spl0_5
| ~ spl0_187
| spl0_188 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s201,plain,
( ~ spl0_8
| ~ spl0_188
| spl0_198 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s203,plain,
( ~ spl0_5
| ~ spl0_198
| spl0_200 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s208,plain,
( ~ spl0_8
| ~ spl0_200
| spl0_205 ),
inference(sat_conversion,[],[f2205]) ).
cnf(s211,plain,
( ~ spl0_5
| ~ spl0_205
| spl0_208 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s218,plain,
( ~ spl0_8
| ~ spl0_208
| spl0_215 ),
inference(sat_conversion,[],[f2294]) ).
cnf(s222,plain,
( ~ spl0_7
| ~ spl0_215
| spl0_219 ),
inference(sat_conversion,[],[f2337]) ).
cnf(s223,plain,
( ~ spl0_3
| spl0_122
| ~ spl0_219 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s224,plain,
( ~ spl0_20
| ~ spl0_122
| spl0_220 ),
inference(sat_conversion,[],[f2350]) ).
cnf(s225,plain,
( ~ spl0_7
| ~ spl0_220
| spl0_221 ),
inference(sat_conversion,[],[f2366]) ).
cnf(s226,plain,
( ~ spl0_3
| ~ spl0_221
| spl0_222 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s227,plain,
( ~ spl0_5
| ~ spl0_222
| spl0_223 ),
inference(sat_conversion,[],[f2395]) ).
cnf(s232,plain,
( ~ spl0_8
| ~ spl0_223
| spl0_228 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s233,plain,
( ~ spl0_228
| spl0_229 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s234,plain,
( ~ spl0_3
| ~ spl0_229 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s235,plain,
~ spl0_229,
inference(rat,[],[s234,s3]) ).
cnf(s236,plain,
~ spl0_6,
inference(rat,[],[s6,s3]) ).
cnf(s237,plain,
~ spl0_228,
inference(rat,[],[s233,s235]) ).
cnf(s238,plain,
spl0_4,
inference(rat,[],[s4,s3,s2]) ).
cnf(s239,plain,
spl0_5,
inference(rat,[],[s5,s236,s2,s238]) ).
cnf(s240,plain,
spl0_7,
inference(rat,[],[s7,s2,s239]) ).
cnf(s241,plain,
spl0_8,
inference(rat,[],[s8,s2,s240]) ).
cnf(s242,plain,
~ spl0_223,
inference(rat,[],[s232,s237,s241]) ).
cnf(s243,plain,
spl0_20,
inference(rat,[],[s20,s2,s241]) ).
cnf(s244,plain,
~ spl0_222,
inference(rat,[],[s227,s239,s242]) ).
cnf(s246,plain,
~ spl0_221,
inference(rat,[],[s226,s3,s244]) ).
cnf(s247,plain,
~ spl0_220,
inference(rat,[],[s225,s240,s246]) ).
cnf(s248,plain,
~ spl0_122,
inference(rat,[],[s224,s243,s247]) ).
cnf(s249,plain,
~ spl0_219,
inference(rat,[],[s223,s3,s248]) ).
cnf(s251,plain,
~ spl0_215,
inference(rat,[],[s222,s240,s249]) ).
cnf(s252,plain,
~ spl0_208,
inference(rat,[],[s218,s241,s251]) ).
cnf(s253,plain,
~ spl0_205,
inference(rat,[],[s211,s239,s252]) ).
cnf(s254,plain,
~ spl0_200,
inference(rat,[],[s208,s241,s253]) ).
cnf(s255,plain,
~ spl0_198,
inference(rat,[],[s203,s239,s254]) ).
cnf(s256,plain,
~ spl0_188,
inference(rat,[],[s201,s241,s255]) ).
cnf(s257,plain,
~ spl0_187,
inference(rat,[],[s191,s239,s256]) ).
cnf(s258,plain,
~ spl0_178,
inference(rat,[],[s190,s3,s257]) ).
cnf(s259,plain,
~ spl0_171,
inference(rat,[],[s181,s240,s258]) ).
cnf(s260,plain,
~ spl0_166,
inference(rat,[],[s174,s240,s259]) ).
cnf(s261,plain,
~ spl0_164,
inference(rat,[],[s169,s240,s260]) ).
cnf(s262,plain,
~ spl0_161,
inference(rat,[],[s167,s243,s261]) ).
cnf(s263,plain,
~ spl0_160,
inference(rat,[],[s164,s239,s262]) ).
cnf(s264,plain,
~ spl0_159,
inference(rat,[],[s163,s240,s263]) ).
cnf(s265,plain,
~ spl0_157,
inference(rat,[],[s162,s241,s264]) ).
cnf(s266,plain,
~ spl0_156,
inference(rat,[],[s160,s239,s265]) ).
cnf(s267,plain,
~ spl0_155,
inference(rat,[],[s159,s240,s266]) ).
cnf(s268,plain,
~ spl0_153,
inference(rat,[],[s158,s240,s267]) ).
cnf(s269,plain,
~ spl0_150,
inference(rat,[],[s156,s239,s268]) ).
cnf(s270,plain,
~ spl0_142,
inference(rat,[],[s153,s241,s269]) ).
cnf(s271,plain,
~ spl0_141,
inference(rat,[],[s145,s241,s270]) ).
cnf(s272,plain,
~ spl0_138,
inference(rat,[],[s144,s239,s271]) ).
cnf(s273,plain,
~ spl0_137,
inference(rat,[],[s141,s240,s272]) ).
cnf(s274,plain,
~ spl0_126,
inference(rat,[],[s140,s239,s273]) ).
cnf(s275,plain,
~ spl0_56,
inference(rat,[],[s129,s241,s274]) ).
cnf(s276,plain,
~ spl0_55,
inference(rat,[],[s55,s241,s275]) ).
cnf(s277,plain,
~ spl0_51,
inference(rat,[],[s54,s239,s276]) ).
cnf(s278,plain,
~ spl0_31,
inference(rat,[],[s50,s241,s277]) ).
cnf(s279,plain,
~ spl0_26,
inference(rat,[],[s30,s239,s278]) ).
cnf(s280,plain,
~ spl0_18,
inference(rat,[],[s26,s240,s279]) ).
cnf(s281,plain,
~ spl0_12,
inference(rat,[],[s18,s240,s280]) ).
cnf(s282,plain,
~ spl0_10,
inference(rat,[],[s12,s241,s281]) ).
cnf(s283,plain,
~ spl0_9,
inference(rat,[],[s10,s240,s282]) ).
cnf(s284,plain,
spl0_1,
inference(rat,[],[s9,s241,s283]) ).
cnf(s285,plain,
$false,
inference(rat,[],[s1,s284]) ).
fof(f2443,plain,
$false,
inference(avatar_sat_refutation,[],[s285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL124-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.44 % Computer : n016.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 27 15:27:32 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.50 Running first-order theorem proving
% 0.23/0.50 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
% 16.72/3.17 % (2779343)Input is clausal, will run a generic CNF schedule.
% 16.72/3.17 % (2779360)dis-21_1_sil=8000:lcm=predicate:random_seed=3306911823:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 16.72/3.17 % (2779360)Instruction limit reached!
% 16.72/3.17 % (2779360)------------------------------
% 16.72/3.17 % (2779360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.72/3.17 % (2779360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.72/3.17 % (2779360)CaDiCaL version: 2.1.3
% 16.72/3.17 % (2779360)Termination reason: Instruction limit
% 16.72/3.17 % (2779360)Termination phase: Saturation
% 16.72/3.17 % (2779360)Time elapsed: 0.039 s
% 16.72/3.17 % (2779360)Peak memory usage: 88 MB
% 16.72/3.17 % (2779360)Instructions burned: 118 (million)
% 16.72/3.17 % (2779354)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=2983263450:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 16.72/3.17 % (2779359)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1598735548:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 16.72/3.17 % (2779358)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1850542174:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 16.72/3.17 % (2779356)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3319015133:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 16.72/3.17 % (2779355)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=374158101:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 16.72/3.17 % (2779357)lrs+10_1_sil=8000:sp=occurrence:random_seed=1010204738:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 16.72/3.17 % (2779362)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3573725906:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 16.72/3.17 % (2779362)Refutation not found, incomplete strategy
% 16.72/3.17 % (2779362)------------------------------
% 16.72/3.17 % (2779362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.72/3.17 % (2779362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.72/3.17 % (2779362)CaDiCaL version: 2.1.3
% 16.72/3.17 % (2779362)Termination reason: Refutation not found, incomplete strategy
% 16.72/3.17 % (2779362)Time elapsed: 0.0000 s
% 16.72/3.17 % (2779362)Peak memory usage: 87 MB
% 16.72/3.17 % (2779358)Instruction limit reached!
% 16.72/3.17 % (2779358)------------------------------
% 16.72/3.17 % (2779358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.72/3.17 % (2779358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.72/3.17 % (2779358)CaDiCaL version: 2.1.3
% 16.72/3.17 % (2779358)Termination reason: Instruction limit
% 16.72/3.17 % (2779358)Termination phase: Saturation
% 16.72/3.17 % (2779358)Time elapsed: 0.107 s
% 16.72/3.17 % (2779358)Peak memory usage: 88 MB
% 16.72/3.17 % (2779358)Instructions burned: 114 (million)
% 16.72/3.17 % (2779357)Instruction limit reached!
% 16.72/3.17 % (2779357)------------------------------
% 16.72/3.17 % (2779357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.72/3.17 % (2779357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.72/3.17 % (2779357)CaDiCaL version: 2.1.3
% 16.72/3.17 % (2779357)Termination reason: Instruction limit
% 16.72/3.17 % (2779357)Termination phase: Saturation
% 16.72/3.17 % (2779357)Time elapsed: 0.109 s
% 16.72/3.17 % (2779357)Peak memory usage: 88 MB
% 16.72/3.17 % (2779357)Instructions burned: 107 (million)
% 16.72/3.17 % (2779359)Instruction limit reached!
% 16.72/3.17 % (2779359)------------------------------
% 16.72/3.17 % (2779359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.72/3.17 % (2779359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.72/3.17 % (2779359)CaDiCaL version: 2.1.3
% 16.72/3.17 % (2779359)Termination reason: Instruction limit
% 16.72/3.17 % (2779359)Termination phase: Saturation
% 16.72/3.17 % (2779359)Time elapsed: 0.136 s
% 16.72/3.17 % (2779359)Peak memory usage: 89 MB
% 16.72/3.17 % (2779359)Instructions burned: 180 (million)
% 16.72/3.17 % (2779374)lrs+10_64_to=lpo:sil=8000:random_seed=2597296410:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 20.32/3.73 % (2779362)------------------------------
% 20.32/3.73 % (2779362)------------------------------
% 20.32/3.73 % (2779372)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1148216996:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 20.32/3.73 % (2779373)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1284123162:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 20.32/3.73 % (2779373)Refutation not found, incomplete strategy
% 20.32/3.73 % (2779373)------------------------------
% 20.32/3.73 % (2779373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779373)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779373)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.73 % (2779373)Time elapsed: 0.001 s
% 20.32/3.73 % (2779373)Peak memory usage: 87 MB
% 20.32/3.73 % (2779374)Instruction limit reached!
% 20.32/3.73 % (2779374)------------------------------
% 20.32/3.73 % (2779374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779374)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779374)Termination reason: Instruction limit
% 20.32/3.73 % (2779374)Termination phase: Saturation
% 20.32/3.73 % (2779374)Time elapsed: 0.070 s
% 20.32/3.73 % (2779374)Peak memory usage: 88 MB
% 20.32/3.73 % (2779374)Instructions burned: 126 (million)
% 20.32/3.73 % (2779372)Instruction limit reached!
% 20.32/3.73 % (2779372)------------------------------
% 20.32/3.73 % (2779372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779372)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779372)Termination reason: Instruction limit
% 20.32/3.73 % (2779372)Termination phase: Saturation
% 20.32/3.73 % (2779372)Time elapsed: 0.163 s
% 20.32/3.73 % (2779372)Peak memory usage: 87 MB
% 20.32/3.73 % (2779372)Instructions burned: 190 (million)
% 20.32/3.73 % (2779381)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=121995599:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.32/3.73 % (2779378)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3990895958:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.32/3.73 % (2779381)Instruction limit reached!
% 20.32/3.73 % (2779381)------------------------------
% 20.32/3.73 % (2779381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779381)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779381)Termination reason: Instruction limit
% 20.32/3.73 % (2779381)Termination phase: Saturation
% 20.32/3.73 % (2779381)Time elapsed: 0.054 s
% 20.32/3.73 % (2779381)Peak memory usage: 92 MB
% 20.32/3.73 % (2779381)Instructions burned: 157 (million)
% 20.32/3.73 % (2779378)Instruction limit reached!
% 20.32/3.73 % (2779378)------------------------------
% 20.32/3.73 % (2779378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779378)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779378)Termination reason: Instruction limit
% 20.32/3.73 % (2779378)Termination phase: Saturation
% 20.32/3.73 % (2779378)Time elapsed: 0.136 s
% 20.32/3.73 % (2779378)Peak memory usage: 88 MB
% 20.32/3.73 % (2779378)Instructions burned: 195 (million)
% 20.32/3.73 % (2779382)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2173748343:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 20.32/3.73 % (2779387)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=171870986:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 20.32/3.73 % (2779373)------------------------------
% 20.32/3.73 % (2779373)------------------------------
% 20.32/3.73 % (2779387)Instruction limit reached!
% 20.32/3.73 % (2779387)------------------------------
% 20.32/3.73 % (2779387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779387)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779387)Termination reason: Instruction limit
% 20.32/3.73 % (2779387)Termination phase: Saturation
% 20.32/3.73 % (2779387)Time elapsed: 0.043 s
% 20.32/3.73 % (2779387)Peak memory usage: 88 MB
% 20.32/3.73 % (2779387)Instructions burned: 106 (million)
% 20.32/3.73 % (2779388)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3425349326:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 20.32/3.73 % (2779388)Refutation not found, incomplete strategy
% 20.32/3.73 % (2779388)------------------------------
% 20.32/3.73 % (2779388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779388)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779388)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.73 % (2779388)Time elapsed: 0.001 s
% 20.32/3.73 % (2779388)Peak memory usage: 87 MB
% 20.32/3.73 % (2779392)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3620149754:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 20.32/3.73 % (2779391)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=935097722:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 20.32/3.73 % (2779391)Instruction limit reached!
% 20.32/3.73 % (2779391)------------------------------
% 20.32/3.73 % (2779391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779391)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779391)Termination reason: Instruction limit
% 20.32/3.73 % (2779391)Termination phase: Saturation
% 20.32/3.73 % (2779391)Time elapsed: 0.208 s
% 20.32/3.73 % (2779391)Peak memory usage: 90 MB
% 20.32/3.73 % (2779391)Instructions burned: 243 (million)
% 20.32/3.73 % (2779388)------------------------------
% 20.32/3.73 % (2779388)------------------------------
% 20.32/3.73 % (2779396)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1185191148:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 20.32/3.73 % (2779397)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3579597220:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 20.32/3.73 % (2779396)Instruction limit reached!
% 20.32/3.73 % (2779396)------------------------------
% 20.32/3.73 % (2779396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779396)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779396)Termination reason: Instruction limit
% 20.32/3.73 % (2779396)Termination phase: Saturation
% 20.32/3.73 % (2779396)Time elapsed: 0.097 s
% 20.32/3.73 % (2779396)Peak memory usage: 88 MB
% 20.32/3.73 % (2779396)Instructions burned: 135 (million)
% 20.32/3.73 % (2779402)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3386663914:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 20.32/3.73 % (2779397)Instruction limit reached!
% 20.32/3.73 % (2779397)------------------------------
% 20.32/3.73 % (2779397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779397)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779397)Termination reason: Instruction limit
% 20.32/3.73 % (2779397)Termination phase: Saturation
% 20.32/3.73 % (2779397)Time elapsed: 0.443 s
% 20.32/3.73 % (2779397)Peak memory usage: 91 MB
% 20.32/3.73 % (2779397)Instructions burned: 500 (million)
% 20.32/3.73 % (2779402)Instruction limit reached!
% 20.32/3.73 % (2779402)------------------------------
% 20.32/3.73 % (2779402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779402)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779402)Termination reason: Instruction limit
% 20.32/3.73 % (2779402)Termination phase: Saturation
% 20.32/3.73 % (2779402)Time elapsed: 0.198 s
% 20.32/3.73 % (2779402)Peak memory usage: 89 MB
% 20.32/3.73 % (2779402)Instructions burned: 191 (million)
% 20.32/3.73 % (2779404)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2135422419:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 20.32/3.73 % (2779405)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3485233371:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi)
% 20.32/3.73 % (2779404)First to succeed.
% 20.32/3.73 % (2779404)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2779343"
% 20.32/3.73 % (2779405)Instruction limit reached!
% 20.32/3.73 % (2779405)------------------------------
% 20.32/3.73 % (2779405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.73 % (2779405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.73 % (2779405)CaDiCaL version: 2.1.3
% 20.32/3.73 % (2779405)Termination reason: Instruction limit
% 20.32/3.73 % (2779405)Termination phase: Saturation
% 20.32/3.73 % (2779405)Time elapsed: 0.160 s
% 20.32/3.73 % (2779405)Peak memory usage: 89 MB
% 20.32/3.73 % (2779405)Instructions burned: 156 (million)
% 20.32/3.73 % (2779408)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3432238334:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 20.32/3.73 % (2779404)Refutation found. Thanks to Tanya!
% 20.32/3.73 % SZS status Unsatisfiable for theBenchmark
% 20.32/3.73 % SZS output start Proof for theBenchmark
% See solution above
% 21.14/3.94 % (2779404)------------------------------
% 21.14/3.94 % (2779404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.14/3.94 % (2779404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/3.94 % (2779404)CaDiCaL version: 2.1.3
% 21.14/3.94 % (2779404)Termination reason: Refutation
% 21.14/3.94 % (2779404)Time elapsed: 0.141 s
% 21.14/3.94 % (2779404)Peak memory usage: 91 MB
% 21.14/3.94 % (2779404)Instructions burned: 146 (million)
% 21.14/3.94 % (2779404)------------------------------
% 21.14/3.94 % (2779404)------------------------------
% 21.14/3.94 % (2779343)Success in time 2.893 s
% 21.14/3.94 % Vampire exiting
%------------------------------------------------------------------------------