%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PHI044_1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 12:27:24 PM UTC 2026
% Result : Unsatisfiable 8.44s 2.11s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 40
% Syntax : Number of formulae : 406 ( 29 unt; 0 typ; 32 def)
% Number of atoms : 1562 ( 282 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 1978 ( 822 ~; 956 |; 135 &)
% ( 46 <=>; 15 =>; 0 <=; 4 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 40 ( 38 usr; 33 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 361 ( 0 sgn 319 !; 42 ?; 361 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
option: $tType ).
tff(type_def_6,type,
option_set: $tType ).
tff(func_def_0,type,
sK0: ( option_set * option_set ) > option ).
tff(func_def_1,type,
sK1: ( option * option * option_set ) > option ).
tff(func_def_2,type,
sK2: ( option * option_set ) > option ).
tff(func_def_3,type,
sK3: ( option_set * option_set * option ) > option ).
tff(func_def_4,type,
sK4: ( option * option_set ) > option ).
tff(func_def_5,type,
sK5: ( option * option_set ) > option ).
tff(func_def_6,type,
sK6: option ).
tff(func_def_7,type,
sK7: option ).
tff(func_def_8,type,
sK8: option ).
tff(func_def_9,type,
sK9: option_set ).
tff(func_def_10,type,
sK10: option_set ).
tff(func_def_11,type,
sK11: option_set ).
tff(func_def_12,type,
sK12: option_set ).
tff(pred_def_1,type,
subset: ( option_set * option_set ) > $o ).
tff(pred_def_2,type,
member: ( option * option_set ) > $o ).
tff(pred_def_3,type,
weakly_better: ( option_set * option_set ) > $o ).
tff(pred_def_4,type,
better: ( option_set * option_set ) > $o ).
tff(pred_def_5,type,
permitted_preference: ( option * option ) > $o ).
tff(pred_def_6,type,
required_preference: ( option * option ) > $o ).
tff(f1,axiom,
! [X0: option_set,X1: option_set] :
( subset(X0,X1)
<=> ! [X2: option] :
( member(X2,X0)
=> member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subset) ).
tff(f2,axiom,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
<=> ( weakly_better(X0,X1)
& ~ weakly_better(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',better) ).
tff(f3,axiom,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& member(X0,X2)
& member(X1,X2)
& member(X0,X3)
& ! [X4: option] :
( member(X4,X2)
=> ( ( X4 = X0 )
| ( X4 = X1 ) ) )
& ! [X4: option] :
( member(X4,X3)
=> ( X4 = X0 ) ) )
=> better(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',value_of_rational_diversity) ).
tff(f4,axiom,
! [X0: option_set,X1: option_set] :
( ( subset(X0,X1)
& ? [X2: option] :
( member(X2,X0)
& ! [X3: option] :
( ( member(X3,X1)
& ~ member(X3,X0) )
=> required_preference(X2,X3) ) ) )
=> ~ better(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',insignificance_of_dominated_options) ).
tff(f5,axiom,
! [X0: option_set,X1: option_set] :
( subset(X0,X1)
=> weakly_better(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',harmlessness_of_expansions) ).
tff(f6,axiom,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ( ! [X4: option] :
( member(X4,X2)
<=> ( X4 = X0 ) )
& ! [X4: option] :
( member(X4,X3)
<=> ( X4 = X1 ) ) )
=> ~ better(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',parity_of_no_choice_situations) ).
tff(f7,axiom,
! [X0: option_set,X1: option_set,X2: option_set] :
( ( weakly_better(X0,X1)
& weakly_better(X1,X2) )
=> weakly_better(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_weakly_better_freedom_of_choice) ).
tff(f8,axiom,
? [X0: option,X1: option,X2: option,X3: option_set,X4: option_set,X5: option_set,X6: option_set] :
( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& required_preference(X2,X0)
& required_preference(X2,X1)
& member(X0,X3)
& member(X2,X4)
& member(X0,X5)
& member(X1,X5)
& member(X0,X6)
& member(X1,X6)
& member(X2,X6)
& ! [X7: option] :
( member(X7,X3)
<=> ( X7 = X0 ) )
& ! [X7: option] :
( member(X7,X4)
<=> ( X7 = X2 ) )
& ! [X7: option] :
( member(X7,X5)
<=> ( ( X7 = X0 )
| ( X7 = X1 ) ) )
& ! [X7: option] :
( member(X7,X6)
<=> ( ( X7 = X0 )
| ( X7 = X1 )
| ( X7 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_dominated_diversity) ).
tff(f9,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& member(X0,X2)
& member(X1,X2)
& member(X0,X3)
& ! [X4: option] :
( member(X4,X2)
=> ( ( X4 = X0 )
| ( X4 = X1 ) ) )
& ! [X5: option] :
( member(X5,X3)
=> ( X0 = X5 ) ) )
=> better(X2,X3) ),
inference(rectify,[],[f3]) ).
tff(f10,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ( ! [X4: option] :
( member(X4,X2)
<=> ( X4 = X0 ) )
& ! [X5: option] :
( member(X5,X3)
<=> ( X1 = X5 ) ) )
=> ~ better(X2,X3) ),
inference(rectify,[],[f6]) ).
tff(f11,plain,
? [X0: option,X1: option,X2: option,X3: option_set,X4: option_set,X5: option_set,X6: option_set] :
( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& required_preference(X2,X0)
& required_preference(X2,X1)
& member(X0,X3)
& member(X2,X4)
& member(X0,X5)
& member(X1,X5)
& member(X0,X6)
& member(X1,X6)
& member(X2,X6)
& ! [X7: option] :
( member(X7,X3)
<=> ( X7 = X0 ) )
& ! [X8: option] :
( member(X8,X4)
<=> ( X2 = X8 ) )
& ! [X9: option] :
( member(X9,X5)
<=> ( ( X0 = X9 )
| ( X1 = X9 ) ) )
& ! [X10: option] :
( member(X10,X6)
<=> ( ( X0 = X10 )
| ( X1 = X10 )
| ( X2 = X10 ) ) ) ),
inference(rectify,[],[f8]) ).
tff(f12,plain,
! [X0: option_set,X1: option_set] :
( ! [X2: option] :
( member(X2,X0)
=> member(X2,X1) )
=> subset(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
tff(f13,plain,
! [X0: option_set,X1: option_set] :
( subset(X0,X1)
| ? [X2: option] :
( ~ member(X2,X1)
& member(X2,X0) ) ),
inference(ennf_transformation,[],[f12]) ).
tff(f14,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( better(X2,X3)
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ? [X4: option] :
( ( X0 != X4 )
& ( X1 != X4 )
& member(X4,X2) )
| ? [X5: option] :
( ( X0 != X5 )
& member(X5,X3) ) ),
inference(ennf_transformation,[],[f9]) ).
tff(f15,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( better(X2,X3)
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ? [X4: option] :
( ( X0 != X4 )
& ( X1 != X4 )
& member(X4,X2) )
| ? [X5: option] :
( ( X0 != X5 )
& member(X5,X3) ) ),
inference(flattening,[],[f14]) ).
tff(f16,plain,
! [X0: option_set,X1: option_set] :
( ~ better(X1,X0)
| ~ subset(X0,X1)
| ! [X2: option] :
( ~ member(X2,X0)
| ? [X3: option] :
( ~ required_preference(X2,X3)
& member(X3,X1)
& ~ member(X3,X0) ) ) ),
inference(ennf_transformation,[],[f4]) ).
tff(f17,plain,
! [X0: option_set,X1: option_set] :
( ~ better(X1,X0)
| ~ subset(X0,X1)
| ! [X2: option] :
( ~ member(X2,X0)
| ? [X3: option] :
( ~ required_preference(X2,X3)
& member(X3,X1)
& ~ member(X3,X0) ) ) ),
inference(flattening,[],[f16]) ).
tff(f18,plain,
! [X0: option_set,X1: option_set] :
( weakly_better(X1,X0)
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
tff(f19,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ~ better(X2,X3)
| ? [X4: option] :
( member(X4,X2)
<~> ( X4 = X0 ) )
| ? [X5: option] :
( member(X5,X3)
<~> ( X1 = X5 ) ) ),
inference(ennf_transformation,[],[f10]) ).
tff(f20,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ~ better(X2,X3)
| ? [X4: option] :
( member(X4,X2)
<~> ( X4 = X0 ) )
| ? [X5: option] :
( member(X5,X3)
<~> ( X1 = X5 ) ) ),
inference(flattening,[],[f19]) ).
tff(f21,plain,
! [X0: option_set,X1: option_set,X2: option_set] :
( weakly_better(X0,X2)
| ~ weakly_better(X0,X1)
| ~ weakly_better(X1,X2) ),
inference(ennf_transformation,[],[f7]) ).
tff(f22,plain,
! [X0: option_set,X1: option_set,X2: option_set] :
( weakly_better(X0,X2)
| ~ weakly_better(X0,X1)
| ~ weakly_better(X1,X2) ),
inference(flattening,[],[f21]) ).
tff(f23,plain,
! [X0: option_set,X1: option_set] :
( subset(X0,X1)
| ( ~ member(sK0(X0,X1),X1)
& member(sK0(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f13]) ).
tff(f24,plain,
! [X0: option_set,X1: option_set] :
( ( better(X0,X1)
| ~ weakly_better(X0,X1)
| weakly_better(X1,X0) )
& ( ( weakly_better(X0,X1)
& ~ weakly_better(X1,X0) )
| ~ better(X0,X1) ) ),
inference(nnf_transformation,[],[f2]) ).
tff(f25,plain,
! [X0: option_set,X1: option_set] :
( ( better(X0,X1)
| ~ weakly_better(X0,X1)
| weakly_better(X1,X0) )
& ( ( weakly_better(X0,X1)
& ~ weakly_better(X1,X0) )
| ~ better(X0,X1) ) ),
inference(flattening,[],[f24]) ).
tff(f26,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( better(X2,X3)
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ( ( sK1(X0,X1,X2) != X0 )
& ( sK1(X0,X1,X2) != X1 )
& member(sK1(X0,X1,X2),X2) )
| ( ( sK2(X0,X3) != X0 )
& member(sK2(X0,X3),X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X4,sK1(X0,X1,X2)),skolemize(X5,sK2(X0,X3))],[f15]) ).
tff(f27,plain,
! [X0: option_set,X1: option_set] :
( ~ better(X1,X0)
| ~ subset(X0,X1)
| ! [X2: option] :
( ~ member(X2,X0)
| ( ~ required_preference(X2,sK3(X0,X1,X2))
& member(sK3(X0,X1,X2),X1)
& ~ member(sK3(X0,X1,X2),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f17]) ).
tff(f28,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ~ better(X2,X3)
| ? [X4: option] :
( ( ( X0 != X4 )
| ~ member(X4,X2) )
& ( ( X4 = X0 )
| member(X4,X2) ) )
| ? [X5: option] :
( ( ( X1 != X5 )
| ~ member(X5,X3) )
& ( ( X1 = X5 )
| member(X5,X3) ) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f29,plain,
! [X0: option,X1: option,X2: option_set,X3: option_set] :
( ~ better(X2,X3)
| ( ( ( sK4(X0,X2) != X0 )
| ~ member(sK4(X0,X2),X2) )
& ( ( sK4(X0,X2) = X0 )
| member(sK4(X0,X2),X2) ) )
| ( ( ( sK5(X1,X3) != X1 )
| ~ member(sK5(X1,X3),X3) )
& ( ( sK5(X1,X3) = X1 )
| member(sK5(X1,X3),X3) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X4,sK4(X0,X2)),skolemize(X5,sK5(X1,X3))],[f28]) ).
tff(f30,plain,
? [X0: option,X1: option,X2: option,X3: option_set,X4: option_set,X5: option_set,X6: option_set] :
( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& required_preference(X2,X0)
& required_preference(X2,X1)
& member(X0,X3)
& member(X2,X4)
& member(X0,X5)
& member(X1,X5)
& member(X0,X6)
& member(X1,X6)
& member(X2,X6)
& ! [X7: option] :
( ( member(X7,X3)
| ( X0 != X7 ) )
& ( ( X7 = X0 )
| ~ member(X7,X3) ) )
& ! [X8: option] :
( ( member(X8,X4)
| ( X2 != X8 ) )
& ( ( X2 = X8 )
| ~ member(X8,X4) ) )
& ! [X9: option] :
( ( member(X9,X5)
| ( ( X0 != X9 )
& ( X1 != X9 ) ) )
& ( ( X0 = X9 )
| ( X1 = X9 )
| ~ member(X9,X5) ) )
& ! [X10: option] :
( ( member(X10,X6)
| ( ( X0 != X10 )
& ( X1 != X10 )
& ( X2 != X10 ) ) )
& ( ( X0 = X10 )
| ( X1 = X10 )
| ( X2 = X10 )
| ~ member(X10,X6) ) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f31,plain,
? [X0: option,X1: option,X2: option,X3: option_set,X4: option_set,X5: option_set,X6: option_set] :
( permitted_preference(X0,X1)
& permitted_preference(X1,X0)
& required_preference(X2,X0)
& required_preference(X2,X1)
& member(X0,X3)
& member(X2,X4)
& member(X0,X5)
& member(X1,X5)
& member(X0,X6)
& member(X1,X6)
& member(X2,X6)
& ! [X7: option] :
( ( member(X7,X3)
| ( X0 != X7 ) )
& ( ( X7 = X0 )
| ~ member(X7,X3) ) )
& ! [X8: option] :
( ( member(X8,X4)
| ( X2 != X8 ) )
& ( ( X2 = X8 )
| ~ member(X8,X4) ) )
& ! [X9: option] :
( ( member(X9,X5)
| ( ( X0 != X9 )
& ( X1 != X9 ) ) )
& ( ( X0 = X9 )
| ( X1 = X9 )
| ~ member(X9,X5) ) )
& ! [X10: option] :
( ( member(X10,X6)
| ( ( X0 != X10 )
& ( X1 != X10 )
& ( X2 != X10 ) ) )
& ( ( X0 = X10 )
| ( X1 = X10 )
| ( X2 = X10 )
| ~ member(X10,X6) ) ) ),
inference(flattening,[],[f30]) ).
tff(f32,plain,
( permitted_preference(sK6,sK7)
& permitted_preference(sK7,sK6)
& required_preference(sK8,sK6)
& required_preference(sK8,sK7)
& member(sK6,sK9)
& member(sK8,sK10)
& member(sK6,sK11)
& member(sK7,sK11)
& member(sK6,sK12)
& member(sK7,sK12)
& member(sK8,sK12)
& ! [X7: option] :
( ( member(X7,sK9)
| ( sK6 != X7 ) )
& ( ( sK6 = X7 )
| ~ member(X7,sK9) ) )
& ! [X8: option] :
( ( member(X8,sK10)
| ( sK8 != X8 ) )
& ( ( sK8 = X8 )
| ~ member(X8,sK10) ) )
& ! [X9: option] :
( ( member(X9,sK11)
| ( ( sK6 != X9 )
& ( sK7 != X9 ) ) )
& ( ( sK6 = X9 )
| ( sK7 = X9 )
| ~ member(X9,sK11) ) )
& ! [X10: option] :
( ( member(X10,sK12)
| ( ( sK6 != X10 )
& ( sK7 != X10 )
& ( sK8 != X10 ) ) )
& ( ( sK6 = X10 )
| ( sK7 = X10 )
| ( sK8 = X10 )
| ~ member(X10,sK12) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9),skolemize(X4,sK10),skolemize(X5,sK11),skolemize(X6,sK12)],[f31]) ).
tff(f33,plain,
! [X0: option_set,X1: option_set] :
( member(sK0(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tff(f34,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK0(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tff(f35,plain,
! [X0: option_set,X1: option_set] :
( ~ better(X0,X1)
| ~ weakly_better(X1,X0) ),
inference(cnf_transformation,[],[f25]) ).
tff(f37,plain,
! [X0: option_set,X1: option_set] :
( ~ weakly_better(X0,X1)
| better(X0,X1)
| weakly_better(X1,X0) ),
inference(cnf_transformation,[],[f25]) ).
tff(f38,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ permitted_preference(X1,X0)
| ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| member(sK1(X0,X1,X2),X2)
| member(sK2(X0,X3),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f39,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK2(X0,X3) != X0 )
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| member(sK1(X0,X1,X2),X2)
| better(X2,X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f40,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK1(X0,X1,X2) != X1 )
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| better(X2,X3)
| member(sK2(X0,X3),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f41,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK1(X0,X1,X2) != X1 )
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| better(X2,X3)
| ( sK2(X0,X3) != X0 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f42,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK1(X0,X1,X2) != X0 )
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| better(X2,X3)
| member(sK2(X0,X3),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f43,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK1(X0,X1,X2) != X0 )
| ~ permitted_preference(X0,X1)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| better(X2,X3)
| ( sK2(X0,X3) != X0 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f44,plain,
! [X2: option,X0: option_set,X1: option_set] :
( ~ member(sK3(X0,X1,X2),X0)
| ~ subset(X0,X1)
| ~ member(X2,X0)
| ~ better(X1,X0) ),
inference(cnf_transformation,[],[f27]) ).
tff(f45,plain,
! [X2: option,X0: option_set,X1: option_set] :
( member(sK3(X0,X1,X2),X1)
| ~ subset(X0,X1)
| ~ member(X2,X0)
| ~ better(X1,X0) ),
inference(cnf_transformation,[],[f27]) ).
tff(f46,plain,
! [X2: option,X0: option_set,X1: option_set] :
( ~ required_preference(X2,sK3(X0,X1,X2))
| ~ subset(X0,X1)
| ~ member(X2,X0)
| ~ better(X1,X0) ),
inference(cnf_transformation,[],[f27]) ).
tff(f47,plain,
! [X0: option_set,X1: option_set] :
( ~ subset(X0,X1)
| weakly_better(X1,X0) ),
inference(cnf_transformation,[],[f18]) ).
tff(f48,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ better(X2,X3)
| ( sK4(X0,X2) = X0 )
| member(sK4(X0,X2),X2)
| ( sK5(X1,X3) = X1 )
| member(sK5(X1,X3),X3) ),
inference(cnf_transformation,[],[f29]) ).
tff(f49,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK5(X1,X3) != X1 )
| ( sK4(X0,X2) = X0 )
| member(sK4(X0,X2),X2)
| ~ better(X2,X3)
| ~ member(sK5(X1,X3),X3) ),
inference(cnf_transformation,[],[f29]) ).
tff(f50,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK4(X0,X2) != X0 )
| ~ better(X2,X3)
| ~ member(sK4(X0,X2),X2)
| ( sK5(X1,X3) = X1 )
| member(sK5(X1,X3),X3) ),
inference(cnf_transformation,[],[f29]) ).
tff(f51,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ( sK5(X1,X3) != X1 )
| ( sK4(X0,X2) != X0 )
| ~ member(sK4(X0,X2),X2)
| ~ better(X2,X3)
| ~ member(sK5(X1,X3),X3) ),
inference(cnf_transformation,[],[f29]) ).
tff(f52,plain,
! [X2: option_set,X0: option_set,X1: option_set] :
( ~ weakly_better(X1,X2)
| ~ weakly_better(X0,X1)
| weakly_better(X0,X2) ),
inference(cnf_transformation,[],[f22]) ).
tff(f53,plain,
! [X10: option] :
( ~ member(X10,sK12)
| ( sK7 = X10 )
| ( sK8 = X10 )
| ( sK6 = X10 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f54,plain,
! [X10: option] :
( member(X10,sK12)
| ( sK8 != X10 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f55,plain,
! [X10: option] :
( member(X10,sK12)
| ( sK7 != X10 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f56,plain,
! [X10: option] :
( member(X10,sK12)
| ( sK6 != X10 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f57,plain,
! [X9: option] :
( ~ member(X9,sK11)
| ( sK7 = X9 )
| ( sK6 = X9 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f58,plain,
! [X9: option] :
( member(X9,sK11)
| ( sK7 != X9 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f59,plain,
! [X9: option] :
( member(X9,sK11)
| ( sK6 != X9 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f60,plain,
! [X8: option] :
( ~ member(X8,sK10)
| ( sK8 = X8 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f61,plain,
! [X8: option] :
( member(X8,sK10)
| ( sK8 != X8 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f62,plain,
! [X7: option] :
( ~ member(X7,sK9)
| ( sK6 = X7 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f63,plain,
! [X7: option] :
( member(X7,sK9)
| ( sK6 != X7 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f71,plain,
required_preference(sK8,sK7),
inference(cnf_transformation,[],[f32]) ).
tff(f72,plain,
required_preference(sK8,sK6),
inference(cnf_transformation,[],[f32]) ).
tff(f73,plain,
permitted_preference(sK7,sK6),
inference(cnf_transformation,[],[f32]) ).
tff(f74,plain,
permitted_preference(sK6,sK7),
inference(cnf_transformation,[],[f32]) ).
tff(f75,plain,
member(sK6,sK9),
inference(equality_resolution,[],[f63]) ).
tff(f76,plain,
member(sK8,sK10),
inference(equality_resolution,[],[f61]) ).
tff(f77,plain,
member(sK6,sK11),
inference(equality_resolution,[],[f59]) ).
tff(f78,plain,
member(sK7,sK11),
inference(equality_resolution,[],[f58]) ).
tff(f79,plain,
member(sK6,sK12),
inference(equality_resolution,[],[f56]) ).
tff(f80,plain,
member(sK7,sK12),
inference(equality_resolution,[],[f55]) ).
tff(f81,plain,
member(sK8,sK12),
inference(equality_resolution,[],[f54]) ).
tff(f84,plain,
! [X0: option_set] :
( subset(sK9,X0)
| ( sK6 = sK0(sK9,X0) ) ),
inference(resolution,[],[f62,f33]) ).
tff(f85,plain,
! [X0: option_set] :
( subset(sK10,X0)
| ( sK8 = sK0(sK10,X0) ) ),
inference(resolution,[],[f60,f33]) ).
tff(f87,plain,
! [X0: option_set] :
( weakly_better(X0,sK10)
| ( sK8 = sK0(sK10,X0) ) ),
inference(resolution,[],[f47,f85]) ).
tff(f93,plain,
! [X0: option_set,X1: option] :
( ~ better(sK12,X0)
| ~ member(X1,X0)
| ~ subset(X0,sK12)
| ( sK7 = sK3(X0,sK12,X1) )
| ( sK8 = sK3(X0,sK12,X1) )
| ( sK6 = sK3(X0,sK12,X1) ) ),
inference(resolution,[],[f45,f53]) ).
tff(f96,plain,
! [X0: option_set] :
( subset(sK11,X0)
| ( sK6 = sK0(sK11,X0) )
| ( sK7 = sK0(sK11,X0) ) ),
inference(resolution,[],[f57,f33]) ).
tff(f103,plain,
! [X0: option_set] :
( weakly_better(X0,sK11)
| ( sK7 = sK0(sK11,X0) )
| ( sK6 = sK0(sK11,X0) ) ),
inference(resolution,[],[f96,f47]) ).
tff(f111,plain,
! [X0: option_set] :
( weakly_better(sK10,X0)
| better(X0,sK10)
| ( sK8 = sK0(sK10,X0) ) ),
inference(resolution,[],[f87,f37]) ).
tff(f119,plain,
! [X0: option_set,X1: option_set] :
( ~ permitted_preference(sK6,sK7)
| better(X0,X1)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| member(sK1(sK6,sK7,X0),X0)
| member(sK2(sK6,X1),X1) ),
inference(resolution,[],[f38,f73]) ).
tff(f120,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK7,X0)
| ~ member(sK6,X0)
| better(X0,X1)
| ~ member(sK6,X1)
| member(sK1(sK6,sK7,X0),X0)
| member(sK2(sK6,X1),X1) ),
inference(forward_subsumption_resolution,[],[f119,f74]) ).
tff(f123,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| member(sK1(sK6,sK7,sK11),sK11)
| member(sK2(sK6,X0),X0) ),
inference(resolution,[],[f120,f78]) ).
tff(f124,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| member(sK1(sK6,sK7,sK11),sK11)
| member(sK2(sK6,X0),X0) ),
inference(forward_subsumption_resolution,[],[f123,f77]) ).
tff(f127,definition,
( spl13_1
<=> member(sK1(sK6,sK7,sK11),sK11) ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
tff(f129,plain,
( member(sK1(sK6,sK7,sK11),sK11)
| ~ spl13_1 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f131,definition,
( spl13_2
<=> ! [X0: option_set] :
( better(sK11,X0)
| member(sK2(sK6,X0),X0)
| ~ member(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
tff(f132,plain,
( ! [X0: option_set] :
( member(sK2(sK6,X0),X0)
| better(sK11,X0)
| ~ member(sK6,X0) )
| ~ spl13_2 ),
inference(avatar_component_clause,[],[f131]) ).
tff(f133,plain,
( spl13_1
| spl13_2 ),
inference(avatar_split_clause,[],[f124,f131,f127]) ).
tff(f221,plain,
( better(sK11,sK9)
| ~ member(sK6,sK9)
| ( sK6 = sK2(sK6,sK9) )
| ~ spl13_2 ),
inference(resolution,[],[f132,f62]) ).
tff(f240,plain,
( better(sK11,sK9)
| ( sK6 = sK2(sK6,sK9) )
| ~ spl13_2 ),
inference(forward_subsumption_resolution,[],[f221,f75]) ).
tff(f254,definition,
( spl13_18
<=> better(sK11,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
tff(f255,plain,
( ~ better(sK11,sK12)
| spl13_18 ),
inference(avatar_component_clause,[],[f254]) ).
tff(f256,plain,
( better(sK11,sK12)
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f254]) ).
tff(f260,definition,
( spl13_19
<=> ( sK6 = sK2(sK6,sK9) ) ),
introduced(definition,[new_symbols(definition,[spl13_19])],[avatar_definition]) ).
tff(f262,plain,
( ( sK6 = sK2(sK6,sK9) )
| ~ spl13_19 ),
inference(avatar_component_clause,[],[f260]) ).
tff(f264,definition,
( spl13_20
<=> better(sK11,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
tff(f265,plain,
( ~ better(sK11,sK9)
| spl13_20 ),
inference(avatar_component_clause,[],[f264]) ).
tff(f266,plain,
( better(sK11,sK9)
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f264]) ).
tff(f267,plain,
( spl13_19
| spl13_20
| ~ spl13_2 ),
inference(avatar_split_clause,[],[f240,f131,f264,f260]) ).
tff(f278,plain,
( ! [X0: option,X1: option_set] :
( ( sK6 != sK6 )
| ~ permitted_preference(sK6,X0)
| ~ permitted_preference(X0,sK6)
| ~ member(sK6,X1)
| ~ member(X0,X1)
| ~ member(sK6,sK9)
| member(sK1(sK6,X0,X1),X1)
| better(X1,sK9) )
| ~ spl13_19 ),
inference(superposition,[],[f39,f262]) ).
tff(f279,plain,
( ! [X0: option,X1: option_set] :
( ~ permitted_preference(sK6,X0)
| ~ permitted_preference(X0,sK6)
| ~ member(sK6,X1)
| ~ member(X0,X1)
| ~ member(sK6,sK9)
| member(sK1(sK6,X0,X1),X1)
| better(X1,sK9) )
| ~ spl13_19 ),
inference(trivial_inequality_removal,[],[f278]) ).
tff(f280,plain,
( ! [X0: option,X1: option_set] :
( member(sK1(sK6,X0,X1),X1)
| ~ permitted_preference(X0,sK6)
| ~ member(sK6,X1)
| ~ member(X0,X1)
| ~ permitted_preference(sK6,X0)
| better(X1,sK9) )
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f279,f75]) ).
tff(f291,plain,
( ! [X0: option] :
( ~ permitted_preference(X0,sK6)
| ~ member(sK6,sK11)
| ~ member(X0,sK11)
| ~ permitted_preference(sK6,X0)
| better(sK11,sK9)
| ( sK7 = sK1(sK6,X0,sK11) )
| ( sK6 = sK1(sK6,X0,sK11) ) )
| ~ spl13_19 ),
inference(resolution,[],[f280,f57]) ).
tff(f295,plain,
( ! [X0: option] :
( ~ permitted_preference(X0,sK6)
| ~ member(X0,sK11)
| ~ permitted_preference(sK6,X0)
| better(sK11,sK9)
| ( sK7 = sK1(sK6,X0,sK11) )
| ( sK6 = sK1(sK6,X0,sK11) ) )
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f291,f77]) ).
tff(f298,definition,
( spl13_23
<=> better(sK12,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_23])],[avatar_definition]) ).
tff(f299,plain,
( ~ better(sK12,sK9)
| spl13_23 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f300,plain,
( better(sK12,sK9)
| ~ spl13_23 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f306,definition,
( spl13_25
<=> ! [X0: option] :
( ~ permitted_preference(X0,sK6)
| ( sK6 = sK1(sK6,X0,sK11) )
| ( sK7 = sK1(sK6,X0,sK11) )
| ~ permitted_preference(sK6,X0)
| ~ member(X0,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_25])],[avatar_definition]) ).
tff(f307,plain,
( ! [X0: option] :
( ~ permitted_preference(sK6,X0)
| ( sK6 = sK1(sK6,X0,sK11) )
| ( sK7 = sK1(sK6,X0,sK11) )
| ~ permitted_preference(X0,sK6)
| ~ member(X0,sK11) )
| ~ spl13_25 ),
inference(avatar_component_clause,[],[f306]) ).
tff(f308,plain,
( spl13_20
| spl13_25
| ~ spl13_19 ),
inference(avatar_split_clause,[],[f295,f260,f306,f264]) ).
tff(f312,plain,
( ~ weakly_better(sK9,sK11)
| ~ spl13_20 ),
inference(resolution,[],[f266,f35]) ).
tff(f314,definition,
( spl13_26
<=> subset(sK9,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_26])],[avatar_definition]) ).
tff(f315,plain,
( subset(sK9,sK11)
| ~ spl13_26 ),
inference(avatar_component_clause,[],[f314]) ).
tff(f316,plain,
( ~ subset(sK9,sK11)
| spl13_26 ),
inference(avatar_component_clause,[],[f314]) ).
tff(f323,plain,
( ( sK6 = sK0(sK9,sK11) )
| spl13_26 ),
inference(resolution,[],[f316,f84]) ).
tff(f325,plain,
( ~ member(sK6,sK11)
| subset(sK9,sK11)
| spl13_26 ),
inference(superposition,[],[f34,f323]) ).
tff(f326,plain,
( subset(sK9,sK11)
| spl13_26 ),
inference(forward_subsumption_resolution,[],[f325,f77]) ).
tff(f327,plain,
( $false
| spl13_26 ),
inference(forward_subsumption_resolution,[],[f326,f316]) ).
tff(f328,plain,
spl13_26,
inference(avatar_contradiction_clause,[],[f327]) ).
tff(f331,plain,
( ~ weakly_better(sK9,sK12)
| ~ spl13_23 ),
inference(resolution,[],[f300,f35]) ).
tff(f333,definition,
( spl13_28
<=> subset(sK9,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_28])],[avatar_definition]) ).
tff(f334,plain,
( subset(sK9,sK12)
| ~ spl13_28 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f335,plain,
( ~ subset(sK9,sK12)
| spl13_28 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f344,plain,
( weakly_better(sK11,sK9)
| ~ spl13_26 ),
inference(resolution,[],[f315,f47]) ).
tff(f347,plain,
( ( sK6 = sK0(sK9,sK12) )
| spl13_28 ),
inference(resolution,[],[f335,f84]) ).
tff(f349,plain,
( ~ member(sK6,sK12)
| subset(sK9,sK12)
| spl13_28 ),
inference(superposition,[],[f34,f347]) ).
tff(f350,plain,
( subset(sK9,sK12)
| spl13_28 ),
inference(forward_subsumption_resolution,[],[f349,f79]) ).
tff(f351,plain,
( $false
| spl13_28 ),
inference(forward_subsumption_resolution,[],[f350,f335]) ).
tff(f352,plain,
spl13_28,
inference(avatar_contradiction_clause,[],[f351]) ).
tff(f353,plain,
( weakly_better(sK12,sK9)
| ~ spl13_28 ),
inference(resolution,[],[f334,f47]) ).
tff(f354,plain,
( ! [X0: option_set] :
( ~ weakly_better(X0,sK12)
| weakly_better(X0,sK9) )
| ~ spl13_28 ),
inference(resolution,[],[f353,f52]) ).
tff(f355,plain,
( better(sK12,sK9)
| weakly_better(sK9,sK12)
| ~ spl13_28 ),
inference(resolution,[],[f353,f37]) ).
tff(f356,plain,
( weakly_better(sK9,sK12)
| spl13_23
| ~ spl13_28 ),
inference(forward_subsumption_resolution,[],[f355,f299]) ).
tff(f357,plain,
( ! [X0: option_set] :
( ~ weakly_better(X0,sK9)
| weakly_better(X0,sK12) )
| spl13_23
| ~ spl13_28 ),
inference(resolution,[],[f356,f52]) ).
tff(f430,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ( sK7 = sK1(sK6,sK7,sK11) )
| ~ permitted_preference(sK7,sK6)
| ~ member(sK7,sK11)
| ~ spl13_25 ),
inference(resolution,[],[f307,f74]) ).
tff(f431,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ( sK7 = sK1(sK6,sK7,sK11) )
| ~ member(sK7,sK11)
| ~ spl13_25 ),
inference(forward_subsumption_resolution,[],[f430,f73]) ).
tff(f432,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ( sK7 = sK1(sK6,sK7,sK11) )
| ~ spl13_25 ),
inference(forward_subsumption_resolution,[],[f431,f78]) ).
tff(f434,definition,
( spl13_41
<=> ( sK7 = sK1(sK6,sK7,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_41])],[avatar_definition]) ).
tff(f435,plain,
( ( sK7 != sK1(sK6,sK7,sK11) )
| spl13_41 ),
inference(avatar_component_clause,[],[f434]) ).
tff(f436,plain,
( ( sK7 = sK1(sK6,sK7,sK11) )
| ~ spl13_41 ),
inference(avatar_component_clause,[],[f434]) ).
tff(f438,definition,
( spl13_42
<=> ( sK6 = sK1(sK6,sK7,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_42])],[avatar_definition]) ).
tff(f439,plain,
( ( sK6 != sK1(sK6,sK7,sK11) )
| spl13_42 ),
inference(avatar_component_clause,[],[f438]) ).
tff(f440,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ~ spl13_42 ),
inference(avatar_component_clause,[],[f438]) ).
tff(f533,plain,
( ~ weakly_better(sK12,sK11)
| ~ spl13_18 ),
inference(resolution,[],[f256,f35]) ).
tff(f573,definition,
( spl13_57
<=> better(sK12,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_57])],[avatar_definition]) ).
tff(f574,plain,
( ~ better(sK12,sK10)
| spl13_57 ),
inference(avatar_component_clause,[],[f573]) ).
tff(f575,plain,
( better(sK12,sK10)
| ~ spl13_57 ),
inference(avatar_component_clause,[],[f573]) ).
tff(f592,definition,
( spl13_59
<=> subset(sK11,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_59])],[avatar_definition]) ).
tff(f593,plain,
( subset(sK11,sK12)
| ~ spl13_59 ),
inference(avatar_component_clause,[],[f592]) ).
tff(f694,plain,
( ( sK7 = sK0(sK11,sK12) )
| ( sK6 = sK0(sK11,sK12) )
| ~ spl13_18 ),
inference(resolution,[],[f533,f103]) ).
tff(f696,definition,
( spl13_70
<=> ( sK6 = sK0(sK11,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_70])],[avatar_definition]) ).
tff(f698,plain,
( ( sK6 = sK0(sK11,sK12) )
| ~ spl13_70 ),
inference(avatar_component_clause,[],[f696]) ).
tff(f700,definition,
( spl13_71
<=> ( sK7 = sK0(sK11,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_71])],[avatar_definition]) ).
tff(f702,plain,
( ( sK7 = sK0(sK11,sK12) )
| ~ spl13_71 ),
inference(avatar_component_clause,[],[f700]) ).
tff(f703,plain,
( spl13_70
| spl13_71
| ~ spl13_18 ),
inference(avatar_split_clause,[],[f694,f254,f700,f696]) ).
tff(f705,plain,
( ~ member(sK6,sK12)
| subset(sK11,sK12)
| ~ spl13_70 ),
inference(superposition,[],[f34,f698]) ).
tff(f706,plain,
( subset(sK11,sK12)
| ~ spl13_70 ),
inference(forward_subsumption_resolution,[],[f705,f79]) ).
tff(f707,plain,
( spl13_59
| ~ spl13_70 ),
inference(avatar_split_clause,[],[f706,f696,f592]) ).
tff(f709,plain,
( ~ member(sK7,sK12)
| subset(sK11,sK12)
| ~ spl13_71 ),
inference(superposition,[],[f34,f702]) ).
tff(f710,plain,
( subset(sK11,sK12)
| ~ spl13_71 ),
inference(forward_subsumption_resolution,[],[f709,f80]) ).
tff(f711,plain,
( spl13_59
| ~ spl13_71 ),
inference(avatar_split_clause,[],[f710,f700,f592]) ).
tff(f780,plain,
( weakly_better(sK11,sK12)
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(resolution,[],[f357,f344]) ).
tff(f783,plain,
( better(sK11,sK12)
| weakly_better(sK12,sK11)
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(resolution,[],[f780,f37]) ).
tff(f784,plain,
( weakly_better(sK12,sK11)
| spl13_18
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(forward_subsumption_resolution,[],[f783,f255]) ).
tff(f785,plain,
( ! [X0: option_set] :
( ~ weakly_better(X0,sK12)
| weakly_better(X0,sK11) )
| spl13_18
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(resolution,[],[f784,f52]) ).
tff(f807,plain,
( weakly_better(sK9,sK11)
| spl13_18
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(resolution,[],[f785,f356]) ).
tff(f809,plain,
( $false
| spl13_18
| ~ spl13_20
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(forward_subsumption_resolution,[],[f807,f312]) ).
tff(f810,plain,
( spl13_18
| ~ spl13_20
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(avatar_contradiction_clause,[],[f809]) ).
tff(f873,definition,
( spl13_80
<=> ( sK8 = sK0(sK10,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_80])],[avatar_definition]) ).
tff(f874,plain,
( ( sK8 != sK0(sK10,sK12) )
| spl13_80 ),
inference(avatar_component_clause,[],[f873]) ).
tff(f875,plain,
( ( sK8 = sK0(sK10,sK12) )
| ~ spl13_80 ),
inference(avatar_component_clause,[],[f873]) ).
tff(f877,definition,
( spl13_81
<=> weakly_better(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_81])],[avatar_definition]) ).
tff(f879,plain,
( weakly_better(sK10,sK9)
| ~ spl13_81 ),
inference(avatar_component_clause,[],[f877]) ).
tff(f882,plain,
( ~ member(sK8,sK12)
| subset(sK10,sK12)
| ~ spl13_80 ),
inference(superposition,[],[f34,f875]) ).
tff(f883,plain,
( subset(sK10,sK12)
| ~ spl13_80 ),
inference(forward_subsumption_resolution,[],[f882,f81]) ).
tff(f884,plain,
( weakly_better(sK12,sK10)
| ~ spl13_80 ),
inference(resolution,[],[f883,f47]) ).
tff(f886,plain,
( better(sK12,sK10)
| weakly_better(sK10,sK12)
| ~ spl13_80 ),
inference(resolution,[],[f884,f37]) ).
tff(f888,definition,
( spl13_82
<=> weakly_better(sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_82])],[avatar_definition]) ).
tff(f889,plain,
( ~ weakly_better(sK10,sK12)
| spl13_82 ),
inference(avatar_component_clause,[],[f888]) ).
tff(f890,plain,
( weakly_better(sK10,sK12)
| ~ spl13_82 ),
inference(avatar_component_clause,[],[f888]) ).
tff(f891,plain,
( spl13_82
| spl13_57
| ~ spl13_80 ),
inference(avatar_split_clause,[],[f886,f873,f573,f888]) ).
tff(f892,plain,
( weakly_better(sK10,sK9)
| ~ spl13_28
| ~ spl13_82 ),
inference(resolution,[],[f890,f354]) ).
tff(f895,plain,
( spl13_81
| ~ spl13_28
| ~ spl13_82 ),
inference(avatar_split_clause,[],[f892,f888,f333,f877]) ).
tff(f896,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| ~ subset(sK10,sK12)
| ( sK7 = sK3(sK10,sK12,X0) )
| ( sK8 = sK3(sK10,sK12,X0) )
| ( sK6 = sK3(sK10,sK12,X0) ) )
| ~ spl13_57 ),
inference(resolution,[],[f575,f93]) ).
tff(f900,plain,
( better(sK12,sK10)
| ( sK8 = sK0(sK10,sK12) )
| spl13_82 ),
inference(resolution,[],[f889,f111]) ).
tff(f929,definition,
( spl13_86
<=> ( sK6 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_86])],[avatar_definition]) ).
tff(f930,plain,
( ( sK6 != sK3(sK10,sK12,sK8) )
| spl13_86 ),
inference(avatar_component_clause,[],[f929]) ).
tff(f931,plain,
( ( sK6 = sK3(sK10,sK12,sK8) )
| ~ spl13_86 ),
inference(avatar_component_clause,[],[f929]) ).
tff(f933,definition,
( spl13_87
<=> ( sK8 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_87])],[avatar_definition]) ).
tff(f934,plain,
( ( sK8 != sK3(sK10,sK12,sK8) )
| spl13_87 ),
inference(avatar_component_clause,[],[f933]) ).
tff(f935,plain,
( ( sK8 = sK3(sK10,sK12,sK8) )
| ~ spl13_87 ),
inference(avatar_component_clause,[],[f933]) ).
tff(f937,definition,
( spl13_88
<=> ( sK7 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_88])],[avatar_definition]) ).
tff(f938,plain,
( ( sK7 != sK3(sK10,sK12,sK8) )
| spl13_88 ),
inference(avatar_component_clause,[],[f937]) ).
tff(f939,plain,
( ( sK7 = sK3(sK10,sK12,sK8) )
| ~ spl13_88 ),
inference(avatar_component_clause,[],[f937]) ).
tff(f950,plain,
( ~ member(sK8,sK10)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_87 ),
inference(superposition,[],[f44,f935]) ).
tff(f952,plain,
( ~ member(sK8,sK10)
| ~ subset(sK10,sK12)
| ~ better(sK12,sK10)
| ~ spl13_87 ),
inference(duplicate_literal_removal,[],[f950]) ).
tff(f954,plain,
( ~ subset(sK10,sK12)
| ~ better(sK12,sK10)
| ~ spl13_87 ),
inference(forward_subsumption_resolution,[],[f952,f76]) ).
tff(f961,definition,
( spl13_89
<=> subset(sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_89])],[avatar_definition]) ).
tff(f962,plain,
( subset(sK10,sK12)
| ~ spl13_89 ),
inference(avatar_component_clause,[],[f961]) ).
tff(f963,plain,
( ~ subset(sK10,sK12)
| spl13_89 ),
inference(avatar_component_clause,[],[f961]) ).
tff(f965,definition,
( spl13_90
<=> ! [X0: option] :
( ~ member(X0,sK10)
| ( sK6 = sK3(sK10,sK12,X0) )
| ( sK8 = sK3(sK10,sK12,X0) )
| ( sK7 = sK3(sK10,sK12,X0) ) ) ),
introduced(definition,[new_symbols(definition,[spl13_90])],[avatar_definition]) ).
tff(f966,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| ( sK6 = sK3(sK10,sK12,X0) )
| ( sK8 = sK3(sK10,sK12,X0) )
| ( sK7 = sK3(sK10,sK12,X0) ) )
| ~ spl13_90 ),
inference(avatar_component_clause,[],[f965]) ).
tff(f967,plain,
( ~ spl13_89
| spl13_90
| ~ spl13_57 ),
inference(avatar_split_clause,[],[f896,f573,f965,f961]) ).
tff(f969,plain,
( ~ subset(sK10,sK12)
| ~ spl13_57
| ~ spl13_87 ),
inference(forward_subsumption_resolution,[],[f954,f575]) ).
tff(f971,plain,
( ~ spl13_89
| ~ spl13_57
| ~ spl13_87 ),
inference(avatar_split_clause,[],[f969,f933,f573,f961]) ).
tff(f979,plain,
( ( sK8 = sK0(sK10,sK12) )
| spl13_89 ),
inference(resolution,[],[f963,f85]) ).
tff(f980,plain,
( $false
| spl13_80
| spl13_89 ),
inference(forward_subsumption_resolution,[],[f979,f874]) ).
tff(f981,plain,
( spl13_80
| spl13_89 ),
inference(avatar_contradiction_clause,[],[f980]) ).
tff(f982,plain,
( ( sK8 = sK0(sK10,sK12) )
| spl13_57
| spl13_82 ),
inference(forward_subsumption_resolution,[],[f900,f574]) ).
tff(f983,plain,
( $false
| spl13_57
| spl13_80
| spl13_82 ),
inference(forward_subsumption_resolution,[],[f982,f874]) ).
tff(f984,plain,
( spl13_57
| spl13_80
| spl13_82 ),
inference(avatar_contradiction_clause,[],[f983]) ).
tff(f987,plain,
( ! [X0: option_set] :
( ~ weakly_better(X0,sK10)
| weakly_better(X0,sK12) )
| ~ spl13_82 ),
inference(resolution,[],[f890,f52]) ).
tff(f992,plain,
( better(sK10,sK9)
| weakly_better(sK9,sK10)
| ~ spl13_81 ),
inference(resolution,[],[f879,f37]) ).
tff(f994,definition,
( spl13_92
<=> weakly_better(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_92])],[avatar_definition]) ).
tff(f996,plain,
( weakly_better(sK9,sK10)
| ~ spl13_92 ),
inference(avatar_component_clause,[],[f994]) ).
tff(f998,definition,
( spl13_93
<=> better(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_93])],[avatar_definition]) ).
tff(f1000,plain,
( better(sK10,sK9)
| ~ spl13_93 ),
inference(avatar_component_clause,[],[f998]) ).
tff(f1001,plain,
( spl13_92
| spl13_93
| ~ spl13_81 ),
inference(avatar_split_clause,[],[f992,f877,f998,f994]) ).
tff(f1012,plain,
( weakly_better(sK9,sK12)
| ~ spl13_82
| ~ spl13_92 ),
inference(resolution,[],[f987,f996]) ).
tff(f1017,plain,
( $false
| ~ spl13_23
| ~ spl13_82
| ~ spl13_92 ),
inference(forward_subsumption_resolution,[],[f1012,f331]) ).
tff(f1018,plain,
( ~ spl13_23
| ~ spl13_82
| ~ spl13_92 ),
inference(avatar_contradiction_clause,[],[f1017]) ).
tff(f1131,plain,
( ! [X0: option,X1: option] :
( ( sK4(X0,sK10) = X0 )
| member(sK4(X0,sK10),sK10)
| ( sK5(X1,sK9) = X1 )
| member(sK5(X1,sK9),sK9) )
| ~ spl13_93 ),
inference(resolution,[],[f48,f1000]) ).
tff(f1133,definition,
( spl13_101
<=> ! [X1: option] :
( ( sK5(X1,sK9) = X1 )
| member(sK5(X1,sK9),sK9) ) ),
introduced(definition,[new_symbols(definition,[spl13_101])],[avatar_definition]) ).
tff(f1134,plain,
( ! [X1: option] :
( member(sK5(X1,sK9),sK9)
| ( sK5(X1,sK9) = X1 ) )
| ~ spl13_101 ),
inference(avatar_component_clause,[],[f1133]) ).
tff(f1136,definition,
( spl13_102
<=> ! [X0: option] :
( ( sK4(X0,sK10) = X0 )
| member(sK4(X0,sK10),sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_102])],[avatar_definition]) ).
tff(f1137,plain,
( ! [X0: option] :
( member(sK4(X0,sK10),sK10)
| ( sK4(X0,sK10) = X0 ) )
| ~ spl13_102 ),
inference(avatar_component_clause,[],[f1136]) ).
tff(f1138,plain,
( spl13_101
| spl13_102
| ~ spl13_93 ),
inference(avatar_split_clause,[],[f1131,f998,f1136,f1133]) ).
tff(f1152,plain,
( ! [X0: option] :
( ( sK5(X0,sK9) = X0 )
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_101 ),
inference(resolution,[],[f1134,f62]) ).
tff(f1153,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( X0 != X0 )
| ( sK4(X1,X2) = X1 )
| member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_101 ),
inference(superposition,[],[f49,f1152]) ).
tff(f1154,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( X0 != X0 )
| ( sK4(X1,X2) != X1 )
| ~ member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_101 ),
inference(superposition,[],[f51,f1152]) ).
tff(f1160,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( sK4(X1,X2) != X1 )
| ~ member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_101 ),
inference(trivial_inequality_removal,[],[f1154]) ).
tff(f1161,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( sK4(X1,X2) = X1 )
| member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_101 ),
inference(trivial_inequality_removal,[],[f1153]) ).
tff(f1163,definition,
( spl13_105
<=> ! [X0: option] :
( ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) ) ),
introduced(definition,[new_symbols(definition,[spl13_105])],[avatar_definition]) ).
tff(f1164,plain,
( ! [X0: option] :
( ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_105 ),
inference(avatar_component_clause,[],[f1163]) ).
tff(f1166,definition,
( spl13_106
<=> ! [X2: option_set,X1: option] :
( ( sK4(X1,X2) != X1 )
| ~ better(X2,sK9)
| ~ member(sK4(X1,X2),X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_106])],[avatar_definition]) ).
tff(f1167,plain,
( ! [X2: option_set,X1: option] :
( ( sK4(X1,X2) != X1 )
| ~ better(X2,sK9)
| ~ member(sK4(X1,X2),X2) )
| ~ spl13_106 ),
inference(avatar_component_clause,[],[f1166]) ).
tff(f1168,plain,
( spl13_105
| spl13_106
| ~ spl13_101 ),
inference(avatar_split_clause,[],[f1160,f1133,f1166,f1163]) ).
tff(f1170,definition,
( spl13_107
<=> ! [X2: option_set,X1: option] :
( ( sK4(X1,X2) = X1 )
| ~ better(X2,sK9)
| member(sK4(X1,X2),X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_107])],[avatar_definition]) ).
tff(f1171,plain,
( ! [X2: option_set,X1: option] :
( member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ( sK4(X1,X2) = X1 ) )
| ~ spl13_107 ),
inference(avatar_component_clause,[],[f1170]) ).
tff(f1172,plain,
( spl13_105
| spl13_107
| ~ spl13_101 ),
inference(avatar_split_clause,[],[f1161,f1133,f1170,f1163]) ).
tff(f1178,plain,
( ( sK6 = sK5(sK6,sK9) )
| ~ spl13_105 ),
inference(resolution,[],[f1164,f75]) ).
tff(f1181,plain,
( ! [X0: option,X1: option_set] :
( ( sK6 != sK6 )
| ( sK4(X0,X1) = X0 )
| member(sK4(X0,X1),X1)
| ~ better(X1,sK9)
| ~ member(sK6,sK9) )
| ~ spl13_105 ),
inference(superposition,[],[f49,f1178]) ).
tff(f1182,plain,
( ! [X0: option,X1: option_set] :
( ( sK6 != sK6 )
| ( sK4(X0,X1) != X0 )
| ~ member(sK4(X0,X1),X1)
| ~ better(X1,sK9)
| ~ member(sK6,sK9) )
| ~ spl13_105 ),
inference(superposition,[],[f51,f1178]) ).
tff(f1183,plain,
( ! [X0: option,X1: option_set] :
( ( sK4(X0,X1) != X0 )
| ~ member(sK4(X0,X1),X1)
| ~ better(X1,sK9)
| ~ member(sK6,sK9) )
| ~ spl13_105 ),
inference(trivial_inequality_removal,[],[f1182]) ).
tff(f1184,plain,
( ! [X0: option,X1: option_set] :
( ( sK4(X0,X1) = X0 )
| member(sK4(X0,X1),X1)
| ~ better(X1,sK9)
| ~ member(sK6,sK9) )
| ~ spl13_105 ),
inference(trivial_inequality_removal,[],[f1181]) ).
tff(f1185,plain,
( ! [X0: option,X1: option_set] :
( ( sK4(X0,X1) != X0 )
| ~ member(sK4(X0,X1),X1)
| ~ better(X1,sK9) )
| ~ spl13_105 ),
inference(forward_subsumption_resolution,[],[f1183,f75]) ).
tff(f1186,plain,
( ! [X0: option,X1: option_set] :
( ( sK4(X0,X1) = X0 )
| member(sK4(X0,X1),X1)
| ~ better(X1,sK9) )
| ~ spl13_105 ),
inference(forward_subsumption_resolution,[],[f1184,f75]) ).
tff(f1187,plain,
( spl13_106
| ~ spl13_105 ),
inference(avatar_split_clause,[],[f1185,f1163,f1166]) ).
tff(f1188,plain,
( spl13_107
| ~ spl13_105 ),
inference(avatar_split_clause,[],[f1186,f1163,f1170]) ).
tff(f1194,plain,
( ! [X0: option] :
( ~ better(sK10,sK9)
| ( sK4(X0,sK10) = X0 )
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_107 ),
inference(resolution,[],[f1171,f60]) ).
tff(f1199,plain,
( ! [X0: option] :
( ( sK4(X0,sK10) = X0 )
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_93
| ~ spl13_107 ),
inference(forward_subsumption_resolution,[],[f1194,f1000]) ).
tff(f1224,plain,
( ! [X0: option] :
( ( X0 != X0 )
| ~ better(sK10,sK9)
| ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_93
| ~ spl13_106
| ~ spl13_107 ),
inference(superposition,[],[f1167,f1199]) ).
tff(f1232,plain,
( ! [X0: option] :
( ~ better(sK10,sK9)
| ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_93
| ~ spl13_106
| ~ spl13_107 ),
inference(trivial_inequality_removal,[],[f1224]) ).
tff(f1234,definition,
( spl13_114
<=> ! [X0: option] :
( ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) ) ),
introduced(definition,[new_symbols(definition,[spl13_114])],[avatar_definition]) ).
tff(f1235,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_114 ),
inference(avatar_component_clause,[],[f1234]) ).
tff(f1237,definition,
( spl13_115
<=> ! [X2: option,X1: option_set] :
( ~ better(sK10,X1)
| member(sK5(X2,X1),X1)
| ( sK5(X2,X1) = X2 ) ) ),
introduced(definition,[new_symbols(definition,[spl13_115])],[avatar_definition]) ).
tff(f1238,plain,
( ! [X2: option,X1: option_set] :
( member(sK5(X2,X1),X1)
| ~ better(sK10,X1)
| ( sK5(X2,X1) = X2 ) )
| ~ spl13_115 ),
inference(avatar_component_clause,[],[f1237]) ).
tff(f1240,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_93
| ~ spl13_106
| ~ spl13_107 ),
inference(forward_subsumption_resolution,[],[f1232,f1000]) ).
tff(f1241,plain,
( spl13_114
| ~ spl13_93
| ~ spl13_106
| ~ spl13_107 ),
inference(avatar_split_clause,[],[f1240,f1170,f1166,f998,f1234]) ).
tff(f1247,plain,
( ( sK8 = sK4(sK8,sK10) )
| ~ spl13_114 ),
inference(resolution,[],[f1235,f76]) ).
tff(f1249,plain,
( ( sK8 != sK8 )
| ~ better(sK10,sK9)
| ~ member(sK8,sK10)
| ~ spl13_106
| ~ spl13_114 ),
inference(superposition,[],[f1167,f1247]) ).
tff(f1250,plain,
( ! [X0: option_set,X1: option] :
( ( sK8 != sK8 )
| ~ better(sK10,X0)
| ~ member(sK8,sK10)
| ( sK5(X1,X0) = X1 )
| member(sK5(X1,X0),X0) )
| ~ spl13_114 ),
inference(superposition,[],[f50,f1247]) ).
tff(f1251,plain,
( ! [X0: option_set,X1: option] :
( ~ better(sK10,X0)
| ~ member(sK8,sK10)
| ( sK5(X1,X0) = X1 )
| member(sK5(X1,X0),X0) )
| ~ spl13_114 ),
inference(trivial_inequality_removal,[],[f1250]) ).
tff(f1252,plain,
( ~ better(sK10,sK9)
| ~ member(sK8,sK10)
| ~ spl13_106
| ~ spl13_114 ),
inference(trivial_inequality_removal,[],[f1249]) ).
tff(f1253,plain,
( ! [X0: option_set,X1: option] :
( ~ better(sK10,X0)
| ( sK5(X1,X0) = X1 )
| member(sK5(X1,X0),X0) )
| ~ spl13_114 ),
inference(forward_subsumption_resolution,[],[f1251,f76]) ).
tff(f1254,plain,
( ~ member(sK8,sK10)
| ~ spl13_93
| ~ spl13_106
| ~ spl13_114 ),
inference(forward_subsumption_resolution,[],[f1252,f1000]) ).
tff(f1255,plain,
( spl13_115
| ~ spl13_114 ),
inference(avatar_split_clause,[],[f1253,f1234,f1237]) ).
tff(f1256,plain,
( $false
| ~ spl13_93
| ~ spl13_106
| ~ spl13_114 ),
inference(forward_subsumption_resolution,[],[f1254,f76]) ).
tff(f1257,plain,
( ~ spl13_93
| ~ spl13_106
| ~ spl13_114 ),
inference(avatar_contradiction_clause,[],[f1256]) ).
tff(f1281,plain,
( ~ required_preference(sK8,sK7)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_88 ),
inference(superposition,[],[f46,f939]) ).
tff(f1282,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_88 ),
inference(forward_subsumption_resolution,[],[f1281,f71]) ).
tff(f1283,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_88
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1282,f962]) ).
tff(f1284,plain,
( ~ better(sK12,sK10)
| ~ spl13_88
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1283,f76]) ).
tff(f1285,plain,
( $false
| ~ spl13_57
| ~ spl13_88
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1284,f575]) ).
tff(f1286,plain,
( ~ spl13_57
| ~ spl13_88
| ~ spl13_89 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
tff(f1287,plain,
( spl13_89
| ~ spl13_80 ),
inference(avatar_split_clause,[],[f883,f873,f961]) ).
tff(f1300,plain,
( ! [X0: option] :
( ~ better(sK10,sK9)
| ( sK5(X0,sK9) = X0 )
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_115 ),
inference(resolution,[],[f1238,f62]) ).
tff(f1340,plain,
( ( sK6 = sK3(sK10,sK12,sK8) )
| ( sK8 = sK3(sK10,sK12,sK8) )
| ( sK7 = sK3(sK10,sK12,sK8) )
| ~ spl13_90 ),
inference(resolution,[],[f966,f76]) ).
tff(f1341,plain,
( ( sK8 = sK3(sK10,sK12,sK8) )
| ( sK7 = sK3(sK10,sK12,sK8) )
| spl13_86
| ~ spl13_90 ),
inference(forward_subsumption_resolution,[],[f1340,f930]) ).
tff(f1342,plain,
( ( sK7 = sK3(sK10,sK12,sK8) )
| spl13_86
| spl13_87
| ~ spl13_90 ),
inference(forward_subsumption_resolution,[],[f1341,f934]) ).
tff(f1343,plain,
( $false
| spl13_86
| spl13_87
| spl13_88
| ~ spl13_90 ),
inference(forward_subsumption_resolution,[],[f1342,f938]) ).
tff(f1344,plain,
( spl13_86
| spl13_87
| spl13_88
| ~ spl13_90 ),
inference(avatar_contradiction_clause,[],[f1343]) ).
tff(f1347,plain,
( ~ required_preference(sK8,sK6)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_86 ),
inference(superposition,[],[f46,f931]) ).
tff(f1348,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_86 ),
inference(forward_subsumption_resolution,[],[f1347,f72]) ).
tff(f1349,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_86
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1348,f962]) ).
tff(f1350,plain,
( ~ better(sK12,sK10)
| ~ spl13_86
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1349,f76]) ).
tff(f1351,plain,
( $false
| ~ spl13_57
| ~ spl13_86
| ~ spl13_89 ),
inference(forward_subsumption_resolution,[],[f1350,f575]) ).
tff(f1352,plain,
( ~ spl13_57
| ~ spl13_86
| ~ spl13_89 ),
inference(avatar_contradiction_clause,[],[f1351]) ).
tff(f1353,plain,
( spl13_41
| spl13_42
| ~ spl13_25 ),
inference(avatar_split_clause,[],[f432,f306,f438,f434]) ).
tff(f1388,plain,
( ! [X0: option_set] :
( ( sK7 != sK7 )
| ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_41 ),
inference(superposition,[],[f41,f436]) ).
tff(f1390,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_41 ),
inference(trivial_inequality_removal,[],[f1388]) ).
tff(f1392,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1390,f74]) ).
tff(f1393,plain,
( ! [X0: option_set] :
( ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1392,f73]) ).
tff(f1394,plain,
( ! [X0: option_set] :
( ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1393,f77]) ).
tff(f1395,plain,
( ! [X0: option_set] :
( ( sK6 != sK2(sK6,X0) )
| better(sK11,X0)
| ~ member(sK6,X0) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1394,f78]) ).
tff(f1396,plain,
( ( sK6 != sK6 )
| better(sK11,sK9)
| ~ member(sK6,sK9)
| ~ spl13_19
| ~ spl13_41 ),
inference(superposition,[],[f1395,f262]) ).
tff(f1399,plain,
( better(sK11,sK9)
| ~ member(sK6,sK9)
| ~ spl13_19
| ~ spl13_41 ),
inference(trivial_inequality_removal,[],[f1396]) ).
tff(f1400,plain,
( ~ member(sK6,sK9)
| ~ spl13_19
| spl13_20
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1399,f265]) ).
tff(f1401,plain,
( $false
| ~ spl13_19
| spl13_20
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1400,f75]) ).
tff(f1402,plain,
( ~ spl13_19
| spl13_20
| ~ spl13_41 ),
inference(avatar_contradiction_clause,[],[f1401]) ).
tff(f1407,plain,
( ! [X0: option_set] :
( ( sK6 != sK6 )
| ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_42 ),
inference(superposition,[],[f43,f440]) ).
tff(f1408,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_42 ),
inference(trivial_inequality_removal,[],[f1407]) ).
tff(f1410,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1408,f74]) ).
tff(f1411,plain,
( ! [X0: option_set] :
( ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1410,f73]) ).
tff(f1412,plain,
( ! [X0: option_set] :
( ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1411,f77]) ).
tff(f1413,plain,
( ! [X0: option_set] :
( ( sK6 != sK2(sK6,X0) )
| better(sK11,X0)
| ~ member(sK6,X0) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1412,f78]) ).
tff(f1414,plain,
( ( sK6 != sK6 )
| better(sK11,sK9)
| ~ member(sK6,sK9)
| ~ spl13_19
| ~ spl13_42 ),
inference(superposition,[],[f1413,f262]) ).
tff(f1417,plain,
( better(sK11,sK9)
| ~ member(sK6,sK9)
| ~ spl13_19
| ~ spl13_42 ),
inference(trivial_inequality_removal,[],[f1414]) ).
tff(f1418,plain,
( ~ member(sK6,sK9)
| ~ spl13_19
| spl13_20
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1417,f265]) ).
tff(f1419,plain,
( $false
| ~ spl13_19
| spl13_20
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1418,f75]) ).
tff(f1420,plain,
( ~ spl13_19
| spl13_20
| ~ spl13_42 ),
inference(avatar_contradiction_clause,[],[f1419]) ).
tff(f1422,plain,
( ! [X0: option_set] :
( ( sK7 != sK7 )
| ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(superposition,[],[f40,f436]) ).
tff(f1426,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(trivial_inequality_removal,[],[f1422]) ).
tff(f1428,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1426,f74]) ).
tff(f1430,plain,
( ! [X0: option_set] :
( ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1428,f73]) ).
tff(f1432,plain,
( ! [X0: option_set] :
( ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1430,f77]) ).
tff(f1434,plain,
( ! [X0: option_set] :
( ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f1432,f78]) ).
tff(f1435,plain,
( spl13_2
| ~ spl13_41 ),
inference(avatar_split_clause,[],[f1434,f434,f131]) ).
tff(f1436,plain,
( ! [X0: option_set] :
( ( sK6 != sK6 )
| ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(superposition,[],[f42,f440]) ).
tff(f1441,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK6,sK7)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(trivial_inequality_removal,[],[f1436]) ).
tff(f1443,plain,
( ! [X0: option_set] :
( ~ permitted_preference(sK7,sK6)
| ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1441,f74]) ).
tff(f1445,plain,
( ! [X0: option_set] :
( ~ member(sK6,sK11)
| ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1443,f73]) ).
tff(f1447,plain,
( ! [X0: option_set] :
( ~ member(sK7,sK11)
| ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1445,f77]) ).
tff(f1449,plain,
( ! [X0: option_set] :
( ~ member(sK6,X0)
| better(sK11,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_42 ),
inference(forward_subsumption_resolution,[],[f1447,f78]) ).
tff(f1450,plain,
( spl13_2
| ~ spl13_42 ),
inference(avatar_split_clause,[],[f1449,f438,f131]) ).
tff(f1451,plain,
( ( sK7 = sK1(sK6,sK7,sK11) )
| ( sK6 = sK1(sK6,sK7,sK11) )
| ~ spl13_1 ),
inference(resolution,[],[f129,f57]) ).
tff(f1452,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ~ spl13_1
| spl13_41 ),
inference(forward_subsumption_resolution,[],[f1451,f435]) ).
tff(f1453,plain,
( $false
| ~ spl13_1
| spl13_41
| spl13_42 ),
inference(forward_subsumption_resolution,[],[f1452,f439]) ).
tff(f1454,plain,
( ~ spl13_1
| spl13_41
| spl13_42 ),
inference(avatar_contradiction_clause,[],[f1453]) ).
tff(f1457,plain,
( weakly_better(sK12,sK11)
| ~ spl13_59 ),
inference(resolution,[],[f593,f47]) ).
tff(f1458,plain,
( $false
| ~ spl13_18
| ~ spl13_59 ),
inference(forward_subsumption_resolution,[],[f1457,f533]) ).
tff(f1459,plain,
( ~ spl13_18
| ~ spl13_59 ),
inference(avatar_contradiction_clause,[],[f1458]) ).
tff(f1460,plain,
( ! [X0: option] :
( ( sK5(X0,sK9) = X0 )
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_93
| ~ spl13_115 ),
inference(forward_subsumption_resolution,[],[f1300,f1000]) ).
tff(f1572,plain,
( ! [X0: option] :
( ( sK4(X0,sK10) = X0 )
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_102 ),
inference(resolution,[],[f1137,f60]) ).
tff(f1573,plain,
( ! [X0: option] :
( ( X0 != X0 )
| ~ better(sK10,sK9)
| ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_102
| ~ spl13_106 ),
inference(superposition,[],[f1167,f1572]) ).
tff(f1574,plain,
( ! [X2: option,X0: option,X1: option_set] :
( ( X0 != X0 )
| ~ better(sK10,X1)
| ~ member(X0,sK10)
| ( sK5(X2,X1) = X2 )
| member(sK5(X2,X1),X1)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_102 ),
inference(superposition,[],[f50,f1572]) ).
tff(f1580,plain,
( ! [X2: option,X0: option,X1: option_set] :
( ~ better(sK10,X1)
| ~ member(X0,sK10)
| ( sK5(X2,X1) = X2 )
| member(sK5(X2,X1),X1)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_102 ),
inference(trivial_inequality_removal,[],[f1574]) ).
tff(f1581,plain,
( ! [X0: option] :
( ~ better(sK10,sK9)
| ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_102
| ~ spl13_106 ),
inference(trivial_inequality_removal,[],[f1573]) ).
tff(f1582,plain,
( spl13_114
| spl13_115
| ~ spl13_102 ),
inference(avatar_split_clause,[],[f1580,f1136,f1237,f1234]) ).
tff(f1583,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_93
| ~ spl13_102
| ~ spl13_106 ),
inference(forward_subsumption_resolution,[],[f1581,f1000]) ).
tff(f1584,plain,
( spl13_114
| ~ spl13_93
| ~ spl13_102
| ~ spl13_106 ),
inference(avatar_split_clause,[],[f1583,f1166,f1136,f998,f1234]) ).
tff(f1586,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( X0 != X0 )
| ( sK4(X1,X2) != X1 )
| ~ member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_93
| ~ spl13_115 ),
inference(superposition,[],[f51,f1460]) ).
tff(f1591,plain,
( ! [X2: option_set,X0: option,X1: option] :
( ( sK4(X1,X2) != X1 )
| ~ member(sK4(X1,X2),X2)
| ~ better(X2,sK9)
| ~ member(X0,sK9)
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_93
| ~ spl13_115 ),
inference(trivial_inequality_removal,[],[f1586]) ).
tff(f1593,plain,
( spl13_105
| spl13_106
| ~ spl13_93
| ~ spl13_115 ),
inference(avatar_split_clause,[],[f1591,f1237,f998,f1166,f1163]) ).
cnf(s1,plain,
( spl13_1
| spl13_2 ),
inference(sat_conversion,[],[f133]) ).
cnf(s12,plain,
( ~ spl13_2
| spl13_19
| spl13_20 ),
inference(sat_conversion,[],[f267]) ).
cnf(s15,plain,
( ~ spl13_19
| spl13_20
| spl13_25 ),
inference(sat_conversion,[],[f308]) ).
cnf(s17,plain,
spl13_26,
inference(sat_conversion,[],[f328]) ).
cnf(s19,plain,
spl13_28,
inference(sat_conversion,[],[f352]) ).
cnf(s49,plain,
( ~ spl13_18
| spl13_70
| spl13_71 ),
inference(sat_conversion,[],[f703]) ).
cnf(s50,plain,
( spl13_59
| ~ spl13_70 ),
inference(sat_conversion,[],[f707]) ).
cnf(s51,plain,
( spl13_59
| ~ spl13_71 ),
inference(sat_conversion,[],[f711]) ).
cnf(s60,plain,
( spl13_18
| ~ spl13_20
| spl13_23
| ~ spl13_26
| ~ spl13_28 ),
inference(sat_conversion,[],[f810]) ).
cnf(s65,plain,
( spl13_57
| ~ spl13_80
| spl13_82 ),
inference(sat_conversion,[],[f891]) ).
cnf(s66,plain,
( ~ spl13_28
| spl13_81
| ~ spl13_82 ),
inference(sat_conversion,[],[f895]) ).
cnf(s72,plain,
( ~ spl13_57
| ~ spl13_89
| spl13_90 ),
inference(sat_conversion,[],[f967]) ).
cnf(s73,plain,
( ~ spl13_57
| ~ spl13_87
| ~ spl13_89 ),
inference(sat_conversion,[],[f971]) ).
cnf(s75,plain,
( spl13_80
| spl13_89 ),
inference(sat_conversion,[],[f981]) ).
cnf(s76,plain,
( spl13_57
| spl13_80
| spl13_82 ),
inference(sat_conversion,[],[f984]) ).
cnf(s77,plain,
( ~ spl13_81
| spl13_92
| spl13_93 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s78,plain,
( ~ spl13_23
| ~ spl13_82
| ~ spl13_92 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s84,plain,
( ~ spl13_93
| spl13_101
| spl13_102 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s87,plain,
( ~ spl13_101
| spl13_105
| spl13_106 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s88,plain,
( ~ spl13_101
| spl13_105
| spl13_107 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s89,plain,
( ~ spl13_105
| spl13_106 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s90,plain,
( ~ spl13_105
| spl13_107 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s97,plain,
( ~ spl13_93
| ~ spl13_106
| ~ spl13_107
| spl13_114 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s98,plain,
( ~ spl13_114
| spl13_115 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s99,plain,
( ~ spl13_93
| ~ spl13_106
| ~ spl13_114 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s106,plain,
( ~ spl13_57
| ~ spl13_88
| ~ spl13_89 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s107,plain,
( ~ spl13_80
| spl13_89 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s112,plain,
( spl13_86
| spl13_87
| spl13_88
| ~ spl13_90 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s113,plain,
( ~ spl13_57
| ~ spl13_86
| ~ spl13_89 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s114,plain,
( ~ spl13_25
| spl13_41
| spl13_42 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s117,plain,
( ~ spl13_19
| spl13_20
| ~ spl13_41 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s118,plain,
( ~ spl13_19
| spl13_20
| ~ spl13_42 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s119,plain,
( spl13_2
| ~ spl13_41 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s120,plain,
( spl13_2
| ~ spl13_42 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s121,plain,
( ~ spl13_1
| spl13_41
| spl13_42 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s122,plain,
( ~ spl13_18
| ~ spl13_59 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s129,plain,
( ~ spl13_102
| spl13_114
| spl13_115 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s130,plain,
( ~ spl13_93
| ~ spl13_102
| ~ spl13_106
| spl13_114 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s131,plain,
( ~ spl13_93
| spl13_105
| spl13_106
| ~ spl13_115 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s134,plain,
~ spl13_18,
inference(rat,[],[s49,s50,s51,s122]) ).
cnf(s135,plain,
( spl13_115
| ~ spl13_102 ),
inference(rat,[],[s129,s98]) ).
cnf(s136,plain,
( ~ spl13_106
| ~ spl13_102
| ~ spl13_93 ),
inference(rat,[],[s99,s130]) ).
cnf(s137,plain,
( ~ spl13_102
| ~ spl13_93 ),
inference(rat,[],[s131,s89,s136,s135]) ).
cnf(s138,plain,
( spl13_106
| ~ spl13_101 ),
inference(rat,[],[s87,s89]) ).
cnf(s139,plain,
( spl13_102
| ~ spl13_93 ),
inference(rat,[],[s88,s90,s97,s99,s138,s84]) ).
cnf(s140,plain,
~ spl13_93,
inference(rat,[],[s139,s137]) ).
cnf(s141,plain,
( spl13_82
| spl13_57 ),
inference(rat,[],[s65,s76]) ).
cnf(s142,plain,
( ~ spl13_82
| ~ spl13_23 ),
inference(rat,[],[s77,s66,s78,s19,s140]) ).
cnf(s143,plain,
( ~ spl13_89
| ~ spl13_57 ),
inference(rat,[],[s112,s73,s106,s113,s72]) ).
cnf(s144,plain,
spl13_89,
inference(rat,[],[s75,s107]) ).
cnf(s145,plain,
~ spl13_57,
inference(rat,[],[s143,s144]) ).
cnf(s146,plain,
spl13_82,
inference(rat,[],[s141,s145]) ).
cnf(s148,plain,
~ spl13_23,
inference(rat,[],[s142,s146]) ).
cnf(s150,plain,
~ spl13_20,
inference(rat,[],[s60,s19,s17,s134,s148]) ).
cnf(s152,plain,
~ spl13_19,
inference(rat,[],[s114,s15,s117,s118,s150]) ).
cnf(s153,plain,
~ spl13_2,
inference(rat,[],[s12,s150,s152]) ).
cnf(s154,plain,
~ spl13_42,
inference(rat,[],[s120,s153]) ).
cnf(s155,plain,
~ spl13_41,
inference(rat,[],[s119,s153]) ).
cnf(s156,plain,
spl13_1,
inference(rat,[],[s1,s153]) ).
cnf(s157,plain,
$false,
inference(rat,[],[s121,s156,s154,s155]) ).
tff(f1594,plain,
$false,
inference(avatar_sat_refutation,[],[s157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI044_1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 % Computer : n016.cluster.edu
% 0.10/0.41 % Model : x86_64 x86_64
% 0.10/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.41 % Memory : 8046.5625MB
% 0.10/0.41 % OS : Linux 6.8.0-71-generic
% 0.10/0.41 % CPULimit : 300
% 0.10/0.41 % WCLimit : 300
% 0.10/0.41 % DateTime : Sun Sep 27 22:12:47 UTC 2026
% 0.10/0.42 % CPUTime :
% 0.10/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.45 Running first-order theorem proving
% 0.10/0.45 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.44/2.11 % (3042468)Detected formulas, will run a generic FOF schedule.
% 8.44/2.11 % (3042474)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1523645551:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.44/2.11 % (3042478)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2098885413:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.44/2.11 % (3042475)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3041688039:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.44/2.11 % (3042473)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=80357076:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.44/2.11 % (3042476)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3965249688:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.44/2.11 % (3042479)dis-21_1_sil=8000:lcm=predicate:random_seed=1584705119:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.44/2.11 % (3042477)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=838976445:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.44/2.11 % (3042477)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042477)------------------------------
% 8.44/2.11 % (3042477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042477)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042477)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042477)Time elapsed: 0.0000 s
% 8.44/2.11 % (3042476)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042476)------------------------------
% 8.44/2.11 % (3042476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042477)Peak memory usage: 86 MB
% 8.44/2.11 % (3042476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042476)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042476)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042476)Time elapsed: 0.0000 s
% 8.44/2.11 % (3042476)Peak memory usage: 86 MB
% 8.44/2.11 % (3042479)Instruction limit reached!
% 8.44/2.11 % (3042479)------------------------------
% 8.44/2.11 % (3042479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042479)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042479)Termination reason: Instruction limit
% 8.44/2.11 % (3042479)Termination phase: Saturation
% 8.44/2.11 % (3042479)Time elapsed: 0.067 s
% 8.44/2.11 % (3042479)Peak memory usage: 88 MB
% 8.44/2.11 % (3042479)Instructions burned: 129 (million)
% 8.44/2.11 % (3042478)Instruction limit reached!
% 8.44/2.11 % (3042478)------------------------------
% 8.44/2.11 % (3042478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042478)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042478)Termination reason: Instruction limit
% 8.44/2.11 % (3042478)Termination phase: Saturation
% 8.44/2.11 % (3042478)Time elapsed: 0.100 s
% 8.44/2.11 % (3042478)Peak memory usage: 89 MB
% 8.44/2.11 % (3042478)Instructions burned: 140 (million)
% 8.44/2.11 % (3042487)lrs+10_1_sil=8000:sp=occurrence:random_seed=1609446340:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.44/2.11 % (3042487)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042487)------------------------------
% 8.44/2.11 % (3042487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042487)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042487)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042487)Time elapsed: 0.001 s
% 8.44/2.11 % (3042487)Peak memory usage: 86 MB
% 8.44/2.11 % (3042476)------------------------------
% 8.44/2.11 % (3042476)------------------------------
% 8.44/2.11 % (3042477)------------------------------
% 8.44/2.11 % (3042477)------------------------------
% 8.44/2.11 % (3042488)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4032382859:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.44/2.11 % (3042488)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042488)------------------------------
% 8.44/2.11 % (3042488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042488)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042488)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042488)Time elapsed: 0.001 s
% 8.44/2.11 % (3042488)Peak memory usage: 87 MB
% 8.44/2.11 % (3042491)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1953107850:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.44/2.11 % (3042491)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042491)------------------------------
% 8.44/2.11 % (3042491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042491)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042491)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042491)Time elapsed: 0.002 s
% 8.44/2.11 % (3042491)Peak memory usage: 89 MB
% 8.44/2.11 % (3042491)Instructions burned: 3 (million)
% 8.44/2.11 % (3042490)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2213701639:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.44/2.11 % (3042490)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042490)------------------------------
% 8.44/2.11 % (3042490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042490)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042490)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042490)Time elapsed: 0.001 s
% 8.44/2.11 % (3042490)Peak memory usage: 86 MB
% 8.44/2.11 % (3042487)------------------------------
% 8.44/2.11 % (3042487)------------------------------
% 8.44/2.11 % (3042488)------------------------------
% 8.44/2.11 % (3042488)------------------------------
% 8.44/2.11 % (3042491)------------------------------
% 8.44/2.11 % (3042491)------------------------------
% 8.44/2.11 % (3042475)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042475)------------------------------
% 8.44/2.11 % (3042475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042475)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042475)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042475)Time elapsed: 0.571 s
% 8.44/2.11 % (3042475)Peak memory usage: 126 MB
% 8.44/2.11 % (3042475)Instructions burned: 836 (million)
% 8.44/2.11 % (3042495)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=631268986:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 8.44/2.11 % (3042495)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042495)------------------------------
% 8.44/2.11 % (3042495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042495)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042495)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042495)Time elapsed: 0.001 s
% 8.44/2.11 % (3042495)Peak memory usage: 86 MB
% 8.44/2.11 % (3042490)------------------------------
% 8.44/2.11 % (3042490)------------------------------
% 8.44/2.11 % (3042496)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2104595365:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.44/2.11 % (3042497)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1836151487:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 8.44/2.11 % (3042497)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042497)------------------------------
% 8.44/2.11 % (3042497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042497)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042497)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042497)Time elapsed: 0.001 s
% 8.44/2.11 % (3042497)Peak memory usage: 88 MB
% 8.44/2.11 % (3042497)Instructions burned: 1 (million)
% 8.44/2.11 % (3042473)First to succeed.
% 8.44/2.11 % (3042473)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3042468"
% 8.44/2.11 % (3042474)Also succeeded, but the first one will report.
% 8.44/2.11 % (3042475)------------------------------
% 8.44/2.11 % (3042475)------------------------------
% 8.44/2.11 % (3042499)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2942061392:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 8.44/2.11 % (3042499)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042499)------------------------------
% 8.44/2.11 % (3042499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042499)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042499)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042499)Time elapsed: 0.002 s
% 8.44/2.11 % (3042499)Peak memory usage: 88 MB
% 8.44/2.11 % (3042499)Instructions burned: 1 (million)
% 8.44/2.11 % (3042497)------------------------------
% 8.44/2.11 % (3042497)------------------------------
% 8.44/2.11 % (3042495)------------------------------
% 8.44/2.11 % (3042495)------------------------------
% 8.44/2.11 % (3042504)lrs+10_1_sil=8000:sp=occurrence:random_seed=4289484106:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 8.44/2.11 % (3042504)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042504)------------------------------
% 8.44/2.11 % (3042504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042504)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042504)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042504)Time elapsed: 0.0000 s
% 8.44/2.11 % (3042504)Peak memory usage: 86 MB
% 8.44/2.11 % (3042503)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3280318756:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 8.44/2.11 % (3042503)Refutation not found, incomplete strategy
% 8.44/2.11 % (3042503)------------------------------
% 8.44/2.11 % (3042503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.44/2.11 % (3042503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/2.11 % (3042503)CaDiCaL version: 2.1.3
% 8.44/2.11 % (3042503)Termination reason: Refutation not found, incomplete strategy
% 8.44/2.11 % (3042503)Time elapsed: 0.001 s
% 8.44/2.11 % (3042503)Peak memory usage: 87 MB
% 8.44/2.11 % (3042473)Refutation found. Thanks to Tanya!
% 8.44/2.11 % SZS status Unsatisfiable for theBenchmark
% 8.44/2.11 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/2.31 % (3042473)------------------------------
% 0.17/2.31 % (3042473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/2.31 % (3042473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/2.31 % (3042473)CaDiCaL version: 2.1.3
% 0.17/2.31 % (3042473)Termination reason: Refutation
% 0.17/2.31 % (3042473)Time elapsed: 0.777 s
% 0.17/2.31 % (3042473)Peak memory usage: 129 MB
% 0.17/2.31 % (3042473)Instructions burned: 1105 (million)
% 0.17/2.31 % (3042473)------------------------------
% 0.17/2.31 % (3042473)------------------------------
% 0.17/2.31 % (3042468)Success in time 1.218 s
% 0.17/2.31 % Vampire exiting
%------------------------------------------------------------------------------