%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PHI044_1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:32 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.53s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 33
% Syntax : Number of formulae : 346 ( 25 unt; 0 typ; 25 def)
% Number of atoms : 1273 ( 225 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 1552 ( 625 ~; 734 |; 135 &)
% ( 39 <=>; 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 : 33 ( 31 usr; 26 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 307 ( 0 sgn 265 !; 42 ?; 307 :)
% 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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ 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] :
( ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| member(sK1(X0,X1,X2),X2)
| ( sK2(X0,X3) != X0 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f40,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ( sK1(X0,X1,X2) != X1 )
| member(sK2(X0,X3),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f41,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ( sK1(X0,X1,X2) != X1 )
| ( sK2(X0,X3) != X0 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f42,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ( sK1(X0,X1,X2) != X0 )
| member(sK2(X0,X3),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f43,plain,
! [X2: option_set,X3: option_set,X0: option,X1: option] :
( ~ permitted_preference(X0,X1)
| better(X2,X3)
| ~ permitted_preference(X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ member(X0,X3)
| ( sK1(X0,X1,X2) != X0 )
| ( sK2(X0,X3) != X0 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f44,plain,
! [X2: option,X0: option_set,X1: option_set] :
( ~ better(X1,X0)
| ~ subset(X0,X1)
| ~ member(X2,X0)
| ~ member(sK3(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f27]) ).
tff(f45,plain,
! [X2: option,X0: option_set,X1: option_set] :
( ~ better(X1,X0)
| ~ subset(X0,X1)
| ~ member(X2,X0)
| member(sK3(X0,X1,X2),X1) ),
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] :
( ~ 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(f50,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(f51,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(f52,plain,
! [X2: option_set,X0: option_set,X1: option_set] :
( ~ weakly_better(X0,X1)
| weakly_better(X0,X2)
| ~ weakly_better(X1,X2) ),
inference(cnf_transformation,[],[f22]) ).
tff(f53,plain,
! [X10: option] :
( ~ member(X10,sK12)
| ( sK7 = X10 )
| ( sK8 = X10 )
| ( sK6 = X10 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f57,plain,
! [X9: option] :
( ~ member(X9,sK11)
| ( sK7 = X9 )
| ( sK6 = X9 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f60,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(f64,plain,
member(sK8,sK12),
inference(cnf_transformation,[],[f32]) ).
tff(f65,plain,
member(sK7,sK12),
inference(cnf_transformation,[],[f32]) ).
tff(f66,plain,
member(sK6,sK12),
inference(cnf_transformation,[],[f32]) ).
tff(f67,plain,
member(sK7,sK11),
inference(cnf_transformation,[],[f32]) ).
tff(f68,plain,
member(sK6,sK11),
inference(cnf_transformation,[],[f32]) ).
tff(f69,plain,
member(sK8,sK10),
inference(cnf_transformation,[],[f32]) ).
tff(f70,plain,
member(sK6,sK9),
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(f84,plain,
! [X0: option_set] :
( subset(sK10,X0)
| ( sK8 = sK0(sK10,X0) ) ),
inference(resolution,[],[f33,f60]) ).
tff(f85,plain,
! [X0: option_set] :
( subset(sK9,X0)
| ( sK6 = sK0(sK9,X0) ) ),
inference(resolution,[],[f33,f62]) ).
tff(f94,plain,
! [X0: option_set] :
( subset(sK11,X0)
| ( sK6 = sK0(sK11,X0) )
| ( sK7 = sK0(sK11,X0) ) ),
inference(resolution,[],[f57,f33]) ).
tff(f95,plain,
! [X0: option_set] :
( weakly_better(X0,sK10)
| ( sK8 = sK0(sK10,X0) ) ),
inference(resolution,[],[f84,f47]) ).
tff(f102,plain,
! [X0: option_set] :
( better(X0,sK10)
| ( sK8 = sK0(sK10,X0) )
| weakly_better(sK10,X0) ),
inference(resolution,[],[f95,f37]) ).
tff(f121,plain,
! [X0: option_set,X1: option] :
( ( sK8 = sK0(sK10,X0) )
| weakly_better(sK10,X0)
| ~ subset(sK10,X0)
| ~ member(X1,sK10)
| member(sK3(sK10,X0,X1),X0) ),
inference(resolution,[],[f102,f45]) ).
tff(f122,plain,
! [X0: option_set,X1: option] :
( ( sK8 = sK0(sK10,X0) )
| weakly_better(sK10,X0)
| ~ subset(sK10,X0)
| ~ member(X1,sK10)
| ~ member(sK3(sK10,X0,X1),sK10) ),
inference(resolution,[],[f102,f44]) ).
tff(f125,plain,
! [X0: option_set,X1: option] :
( ~ member(sK3(sK10,X0,X1),sK10)
| weakly_better(sK10,X0)
| ~ member(X1,sK10)
| ( sK8 = sK0(sK10,X0) ) ),
inference(forward_subsumption_resolution,[],[f122,f84]) ).
tff(f126,plain,
! [X0: option_set,X1: option] :
( ~ member(X1,sK10)
| weakly_better(sK10,X0)
| ( sK8 = sK0(sK10,X0) )
| member(sK3(sK10,X0,X1),X0) ),
inference(forward_subsumption_resolution,[],[f121,f84]) ).
tff(f148,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| member(sK1(sK6,sK7,X0),X0)
| member(sK2(sK6,X1),X1) ),
inference(resolution,[],[f38,f74]) ).
tff(f149,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,[],[f148,f73]) ).
tff(f158,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| member(sK1(sK6,sK7,X0),X0)
| ( sK6 != sK2(sK6,X1) ) ),
inference(resolution,[],[f39,f74]) ).
tff(f159,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)
| ( sK6 != sK2(sK6,X1) ) ),
inference(forward_subsumption_resolution,[],[f158,f73]) ).
tff(f163,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| ( sK7 != sK1(sK6,sK7,X0) )
| member(sK2(sK6,X1),X1) ),
inference(resolution,[],[f40,f74]) ).
tff(f164,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK7,X0)
| ~ member(sK6,X0)
| better(X0,X1)
| ~ member(sK6,X1)
| ( sK7 != sK1(sK6,sK7,X0) )
| member(sK2(sK6,X1),X1) ),
inference(forward_subsumption_resolution,[],[f163,f73]) ).
tff(f171,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| ( sK7 != sK1(sK6,sK7,X0) )
| ( sK6 != sK2(sK6,X1) ) ),
inference(resolution,[],[f41,f74]) ).
tff(f172,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK7,X0)
| ~ member(sK6,X0)
| better(X0,X1)
| ~ member(sK6,X1)
| ( sK7 != sK1(sK6,sK7,X0) )
| ( sK6 != sK2(sK6,X1) ) ),
inference(forward_subsumption_resolution,[],[f171,f73]) ).
tff(f187,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| ( sK6 != sK1(sK6,sK7,X0) )
| member(sK2(sK6,X1),X1) ),
inference(resolution,[],[f42,f74]) ).
tff(f188,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK7,X0)
| ~ member(sK6,X0)
| better(X0,X1)
| ~ member(sK6,X1)
| ( sK6 != sK1(sK6,sK7,X0) )
| member(sK2(sK6,X1),X1) ),
inference(forward_subsumption_resolution,[],[f187,f73]) ).
tff(f202,plain,
! [X0: option_set,X1: option_set] :
( better(X0,X1)
| ~ permitted_preference(sK7,sK6)
| ~ member(sK6,X0)
| ~ member(sK7,X0)
| ~ member(sK6,X1)
| ( sK6 != sK1(sK6,sK7,X0) )
| ( sK6 != sK2(sK6,X1) ) ),
inference(resolution,[],[f43,f74]) ).
tff(f203,plain,
! [X0: option_set,X1: option_set] :
( ~ member(sK7,X0)
| ~ member(sK6,X0)
| better(X0,X1)
| ~ member(sK6,X1)
| ( sK6 != sK1(sK6,sK7,X0) )
| ( sK6 != sK2(sK6,X1) ) ),
inference(forward_subsumption_resolution,[],[f202,f73]) ).
tff(f205,plain,
! [X0: option_set] :
( weakly_better(X0,sK11)
| ( sK7 = sK0(sK11,X0) )
| ( sK6 = sK0(sK11,X0) ) ),
inference(resolution,[],[f94,f47]) ).
tff(f215,definition,
( spl13_11
<=> ! [X2: option] :
( ( sK5(X2,sK9) != X2 )
| ~ member(sK5(X2,sK9),sK9) ) ),
introduced(definition,[new_symbols(definition,[spl13_11])],[avatar_definition]) ).
tff(f216,plain,
( ! [X2: option] :
( ~ member(sK5(X2,sK9),sK9)
| ( sK5(X2,sK9) != X2 ) )
| ~ spl13_11 ),
inference(avatar_component_clause,[],[f215]) ).
tff(f222,definition,
( spl13_13
<=> ! [X2: option] :
( ( sK5(X2,sK9) = X2 )
| member(sK5(X2,sK9),sK9) ) ),
introduced(definition,[new_symbols(definition,[spl13_13])],[avatar_definition]) ).
tff(f223,plain,
( ! [X2: option] :
( member(sK5(X2,sK9),sK9)
| ( sK5(X2,sK9) = X2 ) )
| ~ spl13_13 ),
inference(avatar_component_clause,[],[f222]) ).
tff(f233,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,[],[f149,f67]) ).
tff(f236,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,[],[f233,f68]) ).
tff(f246,definition,
( spl13_17
<=> member(sK1(sK6,sK7,sK11),sK11) ),
introduced(definition,[new_symbols(definition,[spl13_17])],[avatar_definition]) ).
tff(f247,plain,
( ~ member(sK1(sK6,sK7,sK11),sK11)
| spl13_17 ),
inference(avatar_component_clause,[],[f246]) ).
tff(f248,plain,
( member(sK1(sK6,sK7,sK11),sK11)
| ~ spl13_17 ),
inference(avatar_component_clause,[],[f246]) ).
tff(f250,definition,
( spl13_18
<=> ! [X0: option_set] :
( better(sK11,X0)
| member(sK2(sK6,X0),X0)
| ~ member(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
tff(f251,plain,
( ! [X0: option_set] :
( ~ member(sK6,X0)
| member(sK2(sK6,X0),X0)
| better(sK11,X0) )
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f250]) ).
tff(f252,plain,
( spl13_17
| spl13_18 ),
inference(avatar_split_clause,[],[f236,f250,f246]) ).
tff(f287,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| member(sK1(sK6,sK7,sK11),sK11)
| ( sK6 != sK2(sK6,X0) ) ),
inference(resolution,[],[f159,f67]) ).
tff(f291,plain,
( ( sK7 = sK1(sK6,sK7,sK11) )
| ( sK6 = sK1(sK6,sK7,sK11) )
| ~ spl13_17 ),
inference(resolution,[],[f248,f57]) ).
tff(f293,definition,
( spl13_26
<=> ( sK6 = sK1(sK6,sK7,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_26])],[avatar_definition]) ).
tff(f295,plain,
( ( sK6 = sK1(sK6,sK7,sK11) )
| ~ spl13_26 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f297,definition,
( spl13_27
<=> ( sK7 = sK1(sK6,sK7,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_27])],[avatar_definition]) ).
tff(f299,plain,
( ( sK7 = sK1(sK6,sK7,sK11) )
| ~ spl13_27 ),
inference(avatar_component_clause,[],[f297]) ).
tff(f300,plain,
( spl13_26
| spl13_27
| ~ spl13_17 ),
inference(avatar_split_clause,[],[f291,f246,f297,f293]) ).
tff(f301,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| member(sK1(sK6,sK7,sK11),sK11)
| ( sK6 != sK2(sK6,X0) ) ),
inference(forward_subsumption_resolution,[],[f287,f68]) ).
tff(f305,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| ( sK7 != sK1(sK6,sK7,sK11) )
| member(sK2(sK6,X0),X0) ),
inference(resolution,[],[f164,f67]) ).
tff(f331,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| ( sK7 != sK1(sK6,sK7,sK11) )
| ( sK6 != sK2(sK6,X0) ) ),
inference(resolution,[],[f172,f67]) ).
tff(f337,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK1(sK6,sK7,sK11) )
| member(sK2(sK6,X0),X0) ),
inference(resolution,[],[f188,f67]) ).
tff(f346,plain,
! [X0: option_set] :
( ~ member(sK6,sK11)
| better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK1(sK6,sK7,sK11) )
| ( sK6 != sK2(sK6,X0) ) ),
inference(resolution,[],[f203,f67]) ).
tff(f349,plain,
( ! [X0: option] :
( ( sK5(X0,sK9) = X0 )
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_13 ),
inference(resolution,[],[f223,f62]) ).
tff(f357,plain,
( ! [X0: option] :
( ( sK6 != X0 )
| ( sK6 = sK5(X0,sK9) ) )
| ~ spl13_13 ),
inference(equality_factoring,[],[f349]) ).
tff(f386,definition,
( spl13_37
<=> member(sK2(sK6,sK9),sK9) ),
introduced(definition,[new_symbols(definition,[spl13_37])],[avatar_definition]) ).
tff(f388,plain,
( member(sK2(sK6,sK9),sK9)
| ~ spl13_37 ),
inference(avatar_component_clause,[],[f386]) ).
tff(f409,plain,
( member(sK2(sK6,sK9),sK9)
| better(sK11,sK9)
| ~ spl13_18 ),
inference(resolution,[],[f251,f70]) ).
tff(f423,definition,
( spl13_40
<=> better(sK11,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_40])],[avatar_definition]) ).
tff(f424,plain,
( ~ better(sK11,sK9)
| spl13_40 ),
inference(avatar_component_clause,[],[f423]) ).
tff(f425,plain,
( better(sK11,sK9)
| ~ spl13_40 ),
inference(avatar_component_clause,[],[f423]) ).
tff(f427,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK7 != sK1(sK6,sK7,sK11) )
| member(sK2(sK6,X0),X0) ),
inference(forward_subsumption_resolution,[],[f305,f68]) ).
tff(f428,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK1(sK6,sK7,sK11) )
| member(sK2(sK6,X0),X0) ),
inference(forward_subsumption_resolution,[],[f337,f68]) ).
tff(f429,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK7 != sK1(sK6,sK7,sK11) )
| ( sK6 != sK2(sK6,X0) ) ),
inference(forward_subsumption_resolution,[],[f331,f68]) ).
tff(f430,plain,
! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK1(sK6,sK7,sK11) )
| ( sK6 != sK2(sK6,X0) ) ),
inference(forward_subsumption_resolution,[],[f346,f68]) ).
tff(f431,plain,
( ! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_27 ),
inference(forward_subsumption_resolution,[],[f427,f299]) ).
tff(f435,plain,
( spl13_18
| ~ spl13_27 ),
inference(avatar_split_clause,[],[f431,f297,f250]) ).
tff(f436,plain,
( spl13_40
| spl13_37
| ~ spl13_18 ),
inference(avatar_split_clause,[],[f409,f250,f386,f423]) ).
tff(f470,plain,
( ! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| member(sK2(sK6,X0),X0) )
| ~ spl13_26 ),
inference(forward_subsumption_resolution,[],[f428,f295]) ).
tff(f473,plain,
( spl13_18
| ~ spl13_26 ),
inference(avatar_split_clause,[],[f470,f293,f250]) ).
tff(f476,definition,
( spl13_45
<=> ! [X0: option_set] :
( better(sK11,X0)
| ( sK6 != sK2(sK6,X0) )
| ~ member(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_45])],[avatar_definition]) ).
tff(f477,plain,
( ! [X0: option_set] :
( ~ member(sK6,X0)
| ( sK6 != sK2(sK6,X0) )
| better(sK11,X0) )
| ~ spl13_45 ),
inference(avatar_component_clause,[],[f476]) ).
tff(f478,plain,
( ~ spl13_26
| spl13_45 ),
inference(avatar_split_clause,[],[f430,f476,f293]) ).
tff(f479,plain,
( ! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK2(sK6,X0) ) )
| spl13_17 ),
inference(forward_subsumption_resolution,[],[f301,f247]) ).
tff(f480,plain,
( spl13_45
| spl13_17 ),
inference(avatar_split_clause,[],[f479,f246,f476]) ).
tff(f484,plain,
( ~ weakly_better(sK9,sK11)
| ~ spl13_40 ),
inference(resolution,[],[f425,f35]) ).
tff(f496,definition,
( spl13_47
<=> subset(sK9,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_47])],[avatar_definition]) ).
tff(f497,plain,
( subset(sK9,sK11)
| ~ spl13_47 ),
inference(avatar_component_clause,[],[f496]) ).
tff(f498,plain,
( ~ subset(sK9,sK11)
| spl13_47 ),
inference(avatar_component_clause,[],[f496]) ).
tff(f532,plain,
( ( sK6 = sK0(sK9,sK11) )
| spl13_47 ),
inference(resolution,[],[f498,f85]) ).
tff(f549,plain,
( ( sK6 != sK2(sK6,sK9) )
| better(sK11,sK9)
| ~ spl13_45 ),
inference(resolution,[],[f477,f70]) ).
tff(f713,definition,
( spl13_82
<=> ( sK6 = sK0(sK11,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_82])],[avatar_definition]) ).
tff(f715,plain,
( ( sK6 = sK0(sK11,sK12) )
| ~ spl13_82 ),
inference(avatar_component_clause,[],[f713]) ).
tff(f717,definition,
( spl13_83
<=> ( sK7 = sK0(sK11,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_83])],[avatar_definition]) ).
tff(f719,plain,
( ( sK7 = sK0(sK11,sK12) )
| ~ spl13_83 ),
inference(avatar_component_clause,[],[f717]) ).
tff(f725,definition,
( spl13_85
<=> ( sK8 = sK0(sK10,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_85])],[avatar_definition]) ).
tff(f726,plain,
( ( sK8 != sK0(sK10,sK12) )
| spl13_85 ),
inference(avatar_component_clause,[],[f725]) ).
tff(f727,plain,
( ( sK8 = sK0(sK10,sK12) )
| ~ spl13_85 ),
inference(avatar_component_clause,[],[f725]) ).
tff(f834,plain,
( ~ member(sK8,sK12)
| subset(sK10,sK12)
| ~ spl13_85 ),
inference(superposition,[],[f34,f727]) ).
tff(f836,plain,
( subset(sK10,sK12)
| ~ spl13_85 ),
inference(forward_subsumption_resolution,[],[f834,f64]) ).
tff(f837,plain,
( weakly_better(sK12,sK10)
| ~ spl13_85 ),
inference(resolution,[],[f836,f47]) ).
tff(f853,definition,
( spl13_101
<=> weakly_better(sK12,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_101])],[avatar_definition]) ).
tff(f854,plain,
( ~ weakly_better(sK12,sK11)
| spl13_101 ),
inference(avatar_component_clause,[],[f853]) ).
tff(f855,plain,
( weakly_better(sK12,sK11)
| ~ spl13_101 ),
inference(avatar_component_clause,[],[f853]) ).
tff(f874,plain,
( better(sK12,sK10)
| weakly_better(sK10,sK12)
| ~ spl13_85 ),
inference(resolution,[],[f837,f37]) ).
tff(f876,definition,
( spl13_104
<=> weakly_better(sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_104])],[avatar_definition]) ).
tff(f877,plain,
( ~ weakly_better(sK10,sK12)
| spl13_104 ),
inference(avatar_component_clause,[],[f876]) ).
tff(f878,plain,
( weakly_better(sK10,sK12)
| ~ spl13_104 ),
inference(avatar_component_clause,[],[f876]) ).
tff(f880,definition,
( spl13_105
<=> better(sK12,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_105])],[avatar_definition]) ).
tff(f881,plain,
( ~ better(sK12,sK10)
| spl13_105 ),
inference(avatar_component_clause,[],[f880]) ).
tff(f882,plain,
( better(sK12,sK10)
| ~ spl13_105 ),
inference(avatar_component_clause,[],[f880]) ).
tff(f883,plain,
( spl13_104
| spl13_105
| ~ spl13_85 ),
inference(avatar_split_clause,[],[f874,f725,f880,f876]) ).
tff(f886,plain,
( ! [X0: option_set] :
( ~ weakly_better(sK12,X0)
| weakly_better(sK10,X0) )
| ~ spl13_104 ),
inference(resolution,[],[f878,f52]) ).
tff(f895,plain,
( ~ member(sK6,sK11)
| subset(sK9,sK11)
| spl13_47 ),
inference(superposition,[],[f34,f532]) ).
tff(f897,plain,
( subset(sK9,sK11)
| spl13_47 ),
inference(forward_subsumption_resolution,[],[f895,f68]) ).
tff(f898,plain,
( $false
| spl13_47 ),
inference(forward_subsumption_resolution,[],[f897,f498]) ).
tff(f899,plain,
spl13_47,
inference(avatar_contradiction_clause,[],[f898]) ).
tff(f905,plain,
( ( sK6 != sK2(sK6,sK9) )
| spl13_40
| ~ spl13_45 ),
inference(forward_subsumption_resolution,[],[f549,f424]) ).
tff(f907,plain,
( weakly_better(sK11,sK9)
| ~ spl13_47 ),
inference(resolution,[],[f497,f47]) ).
tff(f908,plain,
( ( sK6 = sK2(sK6,sK9) )
| ~ spl13_37 ),
inference(resolution,[],[f388,f62]) ).
tff(f909,plain,
( $false
| ~ spl13_37
| spl13_40
| ~ spl13_45 ),
inference(forward_subsumption_resolution,[],[f908,f905]) ).
tff(f910,plain,
( ~ spl13_37
| spl13_40
| ~ spl13_45 ),
inference(avatar_contradiction_clause,[],[f909]) ).
tff(f996,plain,
( ( sK7 = sK0(sK11,sK12) )
| ( sK6 = sK0(sK11,sK12) )
| spl13_101 ),
inference(resolution,[],[f854,f205]) ).
tff(f997,plain,
( spl13_82
| spl13_83
| spl13_101 ),
inference(avatar_split_clause,[],[f996,f853,f717,f713]) ).
tff(f998,plain,
( ~ member(sK6,sK12)
| subset(sK11,sK12)
| ~ spl13_82 ),
inference(superposition,[],[f34,f715]) ).
tff(f1000,plain,
( subset(sK11,sK12)
| ~ spl13_82 ),
inference(forward_subsumption_resolution,[],[f998,f66]) ).
tff(f1001,plain,
( weakly_better(sK12,sK11)
| ~ spl13_82 ),
inference(resolution,[],[f1000,f47]) ).
tff(f1002,plain,
( $false
| ~ spl13_82
| spl13_101 ),
inference(forward_subsumption_resolution,[],[f1001,f854]) ).
tff(f1003,plain,
( ~ spl13_82
| spl13_101 ),
inference(avatar_contradiction_clause,[],[f1002]) ).
tff(f1017,plain,
! [X0: option_set] :
( weakly_better(sK10,X0)
| ( sK8 = sK0(sK10,X0) )
| member(sK3(sK10,X0,sK8),X0) ),
inference(resolution,[],[f126,f69]) ).
tff(f1117,plain,
( weakly_better(sK10,sK11)
| ~ spl13_101
| ~ spl13_104 ),
inference(resolution,[],[f886,f855]) ).
tff(f1142,definition,
( spl13_118
<=> weakly_better(sK10,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_118])],[avatar_definition]) ).
tff(f1144,plain,
( weakly_better(sK10,sK11)
| ~ spl13_118 ),
inference(avatar_component_clause,[],[f1142]) ).
tff(f1146,plain,
( spl13_118
| ~ spl13_101
| ~ spl13_104 ),
inference(avatar_split_clause,[],[f1117,f876,f853,f1142]) ).
tff(f1174,plain,
( ! [X0: option] :
( ~ subset(sK10,sK12)
| ~ member(X0,sK10)
| ~ member(sK3(sK10,sK12,X0),sK10) )
| ~ spl13_105 ),
inference(resolution,[],[f882,f44]) ).
tff(f1175,plain,
( ! [X0: option] :
( ~ subset(sK10,sK12)
| ~ member(X0,sK10)
| member(sK3(sK10,sK12,X0),sK12) )
| ~ spl13_105 ),
inference(resolution,[],[f882,f45]) ).
tff(f1188,plain,
( ! [X0: option] :
( ~ member(X0,sK10)
| member(sK3(sK10,sK12,X0),sK12) )
| ~ spl13_85
| ~ spl13_105 ),
inference(forward_subsumption_resolution,[],[f1175,f836]) ).
tff(f1189,plain,
( ! [X0: option] :
( ~ member(sK3(sK10,sK12,X0),sK10)
| ~ member(X0,sK10) )
| ~ spl13_85
| ~ spl13_105 ),
inference(forward_subsumption_resolution,[],[f1174,f836]) ).
tff(f1587,plain,
( ( sK6 = sK5(sK6,sK9) )
| ~ spl13_13 ),
inference(equality_resolution,[],[f357]) ).
tff(f1604,plain,
( ~ member(sK6,sK9)
| ( sK6 != sK6 )
| ~ spl13_11
| ~ spl13_13 ),
inference(superposition,[],[f216,f1587]) ).
tff(f1605,plain,
( ~ member(sK6,sK9)
| ~ spl13_11
| ~ spl13_13 ),
inference(trivial_inequality_removal,[],[f1604]) ).
tff(f1606,plain,
( $false
| ~ spl13_11
| ~ spl13_13 ),
inference(forward_subsumption_resolution,[],[f1605,f70]) ).
tff(f1607,plain,
( ~ spl13_11
| ~ spl13_13 ),
inference(avatar_contradiction_clause,[],[f1606]) ).
tff(f1622,plain,
( member(sK3(sK10,sK12,sK8),sK12)
| ~ spl13_85
| ~ spl13_105 ),
inference(resolution,[],[f1188,f69]) ).
tff(f1631,plain,
( ( sK7 = sK3(sK10,sK12,sK8) )
| ( sK8 = sK3(sK10,sK12,sK8) )
| ( sK6 = sK3(sK10,sK12,sK8) )
| ~ spl13_85
| ~ spl13_105 ),
inference(resolution,[],[f1622,f53]) ).
tff(f1633,definition,
( spl13_139
<=> ( sK6 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_139])],[avatar_definition]) ).
tff(f1635,plain,
( ( sK6 = sK3(sK10,sK12,sK8) )
| ~ spl13_139 ),
inference(avatar_component_clause,[],[f1633]) ).
tff(f1637,definition,
( spl13_140
<=> ( sK8 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_140])],[avatar_definition]) ).
tff(f1638,plain,
( ( sK8 != sK3(sK10,sK12,sK8) )
| spl13_140 ),
inference(avatar_component_clause,[],[f1637]) ).
tff(f1639,plain,
( ( sK8 = sK3(sK10,sK12,sK8) )
| ~ spl13_140 ),
inference(avatar_component_clause,[],[f1637]) ).
tff(f1641,definition,
( spl13_141
<=> ( sK7 = sK3(sK10,sK12,sK8) ) ),
introduced(definition,[new_symbols(definition,[spl13_141])],[avatar_definition]) ).
tff(f1642,plain,
( ( sK7 != sK3(sK10,sK12,sK8) )
| spl13_141 ),
inference(avatar_component_clause,[],[f1641]) ).
tff(f1643,plain,
( ( sK7 = sK3(sK10,sK12,sK8) )
| ~ spl13_141 ),
inference(avatar_component_clause,[],[f1641]) ).
tff(f1644,plain,
( spl13_139
| spl13_140
| spl13_141
| ~ spl13_85
| ~ spl13_105 ),
inference(avatar_split_clause,[],[f1631,f880,f725,f1641,f1637,f1633]) ).
tff(f1676,plain,
( ~ member(sK8,sK10)
| ~ member(sK8,sK10)
| ~ spl13_85
| ~ spl13_105
| ~ spl13_140 ),
inference(superposition,[],[f1189,f1639]) ).
tff(f1677,plain,
( ~ member(sK8,sK10)
| ~ spl13_85
| ~ spl13_105
| ~ spl13_140 ),
inference(duplicate_literal_removal,[],[f1676]) ).
tff(f1678,plain,
( $false
| ~ spl13_85
| ~ spl13_105
| ~ spl13_140 ),
inference(forward_subsumption_resolution,[],[f1677,f69]) ).
tff(f1679,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_140 ),
inference(avatar_contradiction_clause,[],[f1678]) ).
tff(f1713,plain,
( ~ required_preference(sK8,sK7)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_141 ),
inference(superposition,[],[f46,f1643]) ).
tff(f1714,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_141 ),
inference(forward_subsumption_resolution,[],[f1713,f71]) ).
tff(f1715,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_85
| ~ spl13_141 ),
inference(forward_subsumption_resolution,[],[f1714,f836]) ).
tff(f1716,plain,
( ~ better(sK12,sK10)
| ~ spl13_85
| ~ spl13_141 ),
inference(forward_subsumption_resolution,[],[f1715,f69]) ).
tff(f1717,plain,
( $false
| ~ spl13_85
| ~ spl13_105
| ~ spl13_141 ),
inference(forward_subsumption_resolution,[],[f1716,f882]) ).
tff(f1718,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_141 ),
inference(avatar_contradiction_clause,[],[f1717]) ).
tff(f1724,plain,
( ~ required_preference(sK8,sK6)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_139 ),
inference(superposition,[],[f46,f1635]) ).
tff(f1725,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_139 ),
inference(forward_subsumption_resolution,[],[f1724,f72]) ).
tff(f1726,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_85
| ~ spl13_139 ),
inference(forward_subsumption_resolution,[],[f1725,f836]) ).
tff(f1727,plain,
( ~ better(sK12,sK10)
| ~ spl13_85
| ~ spl13_139 ),
inference(forward_subsumption_resolution,[],[f1726,f69]) ).
tff(f1728,plain,
( $false
| ~ spl13_85
| ~ spl13_105
| ~ spl13_139 ),
inference(forward_subsumption_resolution,[],[f1727,f882]) ).
tff(f1729,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_139 ),
inference(avatar_contradiction_clause,[],[f1728]) ).
tff(f1765,plain,
( ( sK8 = sK0(sK10,sK12) )
| weakly_better(sK10,sK12)
| spl13_105 ),
inference(resolution,[],[f881,f102]) ).
tff(f1776,definition,
( spl13_145
<=> weakly_better(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_145])],[avatar_definition]) ).
tff(f1777,plain,
( ~ weakly_better(sK9,sK10)
| spl13_145 ),
inference(avatar_component_clause,[],[f1776]) ).
tff(f1778,plain,
( weakly_better(sK9,sK10)
| ~ spl13_145 ),
inference(avatar_component_clause,[],[f1776]) ).
tff(f1780,definition,
( spl13_146
<=> better(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl13_146])],[avatar_definition]) ).
tff(f1781,plain,
( ~ better(sK10,sK9)
| spl13_146 ),
inference(avatar_component_clause,[],[f1780]) ).
tff(f1782,plain,
( better(sK10,sK9)
| ~ spl13_146 ),
inference(avatar_component_clause,[],[f1780]) ).
tff(f1804,plain,
( ! [X0: option_set] :
( ~ weakly_better(sK11,X0)
| weakly_better(sK10,X0) )
| ~ spl13_118 ),
inference(resolution,[],[f1144,f52]) ).
tff(f1820,plain,
( ! [X0: option,X1: option] :
( ( sK4(X0,sK10) = X0 )
| member(sK4(X0,sK10),sK10)
| ( sK5(X1,sK9) = X1 )
| member(sK5(X1,sK9),sK9) )
| ~ spl13_146 ),
inference(resolution,[],[f1782,f48]) ).
tff(f1822,plain,
( ! [X0: option,X1: option] :
( ( sK4(X0,sK10) != X0 )
| ~ member(sK4(X0,sK10),sK10)
| ( sK5(X1,sK9) = X1 )
| member(sK5(X1,sK9),sK9) )
| ~ spl13_146 ),
inference(resolution,[],[f1782,f50]) ).
tff(f1825,definition,
( spl13_147
<=> ! [X0: option] :
( ( sK4(X0,sK10) != X0 )
| ~ member(sK4(X0,sK10),sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_147])],[avatar_definition]) ).
tff(f1826,plain,
( ! [X0: option] :
( ~ member(sK4(X0,sK10),sK10)
| ( sK4(X0,sK10) != X0 ) )
| ~ spl13_147 ),
inference(avatar_component_clause,[],[f1825]) ).
tff(f1827,plain,
( spl13_13
| spl13_147
| ~ spl13_146 ),
inference(avatar_split_clause,[],[f1822,f1780,f1825,f222]) ).
tff(f1829,definition,
( spl13_148
<=> ! [X0: option] :
( ( sK4(X0,sK10) = X0 )
| member(sK4(X0,sK10),sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_148])],[avatar_definition]) ).
tff(f1830,plain,
( ! [X0: option] :
( member(sK4(X0,sK10),sK10)
| ( sK4(X0,sK10) = X0 ) )
| ~ spl13_148 ),
inference(avatar_component_clause,[],[f1829]) ).
tff(f1831,plain,
( spl13_13
| spl13_148
| ~ spl13_146 ),
inference(avatar_split_clause,[],[f1820,f1780,f1829,f222]) ).
tff(f1949,plain,
( weakly_better(sK10,sK9)
| ~ spl13_47
| ~ spl13_118 ),
inference(resolution,[],[f1804,f907]) ).
tff(f2004,plain,
( ! [X0: option] :
( ( sK4(X0,sK10) = X0 )
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_148 ),
inference(resolution,[],[f1830,f60]) ).
tff(f2024,plain,
( ! [X0: option] :
( ( sK8 != X0 )
| ( sK8 = sK4(X0,sK10) ) )
| ~ spl13_148 ),
inference(equality_factoring,[],[f2004]) ).
tff(f2048,plain,
( ( sK8 = sK4(sK8,sK10) )
| ~ spl13_148 ),
inference(equality_resolution,[],[f2024]) ).
tff(f2058,plain,
( ~ member(sK8,sK10)
| ( sK8 != sK8 )
| ~ spl13_147
| ~ spl13_148 ),
inference(superposition,[],[f1826,f2048]) ).
tff(f2065,plain,
( ~ member(sK8,sK10)
| ~ spl13_147
| ~ spl13_148 ),
inference(trivial_inequality_removal,[],[f2058]) ).
tff(f2066,plain,
( $false
| ~ spl13_147
| ~ spl13_148 ),
inference(forward_subsumption_resolution,[],[f2065,f69]) ).
tff(f2067,plain,
( ~ spl13_147
| ~ spl13_148 ),
inference(avatar_contradiction_clause,[],[f2066]) ).
tff(f2096,plain,
( ! [X0: option_set] :
( ~ weakly_better(sK10,X0)
| weakly_better(sK9,X0) )
| ~ spl13_145 ),
inference(resolution,[],[f1778,f52]) ).
tff(f2241,plain,
( weakly_better(sK9,sK11)
| ~ spl13_118
| ~ spl13_145 ),
inference(resolution,[],[f2096,f1144]) ).
tff(f2264,plain,
( $false
| ~ spl13_40
| ~ spl13_118
| ~ spl13_145 ),
inference(forward_subsumption_resolution,[],[f2241,f484]) ).
tff(f2265,plain,
( ~ spl13_40
| ~ spl13_118
| ~ spl13_145 ),
inference(avatar_contradiction_clause,[],[f2264]) ).
tff(f2289,plain,
( ! [X0: option_set] :
( better(sK11,X0)
| ~ member(sK6,X0)
| ( sK6 != sK2(sK6,X0) ) )
| ~ spl13_27 ),
inference(forward_subsumption_resolution,[],[f429,f299]) ).
tff(f2292,plain,
( spl13_45
| ~ spl13_27 ),
inference(avatar_split_clause,[],[f2289,f297,f476]) ).
tff(f2353,plain,
( ~ member(sK7,sK12)
| subset(sK11,sK12)
| ~ spl13_83 ),
inference(superposition,[],[f34,f719]) ).
tff(f2355,plain,
( subset(sK11,sK12)
| ~ spl13_83 ),
inference(forward_subsumption_resolution,[],[f2353,f65]) ).
tff(f2356,plain,
( weakly_better(sK12,sK11)
| ~ spl13_83 ),
inference(resolution,[],[f2355,f47]) ).
tff(f2357,plain,
( $false
| ~ spl13_83
| spl13_101 ),
inference(forward_subsumption_resolution,[],[f2356,f854]) ).
tff(f2358,plain,
( ~ spl13_83
| spl13_101 ),
inference(avatar_contradiction_clause,[],[f2357]) ).
tff(f2360,plain,
( weakly_better(sK10,sK12)
| spl13_85
| spl13_105 ),
inference(forward_subsumption_resolution,[],[f1765,f726]) ).
tff(f2365,plain,
( $false
| spl13_85
| spl13_104
| spl13_105 ),
inference(forward_subsumption_resolution,[],[f2360,f877]) ).
tff(f2366,plain,
( spl13_85
| spl13_104
| spl13_105 ),
inference(avatar_contradiction_clause,[],[f2365]) ).
tff(f2381,plain,
( ( sK8 = sK0(sK10,sK12) )
| member(sK3(sK10,sK12,sK8),sK12)
| spl13_104 ),
inference(resolution,[],[f877,f1017]) ).
tff(f2387,plain,
( member(sK3(sK10,sK12,sK8),sK12)
| spl13_85
| spl13_104 ),
inference(forward_subsumption_resolution,[],[f2381,f726]) ).
tff(f2401,definition,
( spl13_160
<=> subset(sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_160])],[avatar_definition]) ).
tff(f2402,plain,
( subset(sK10,sK12)
| ~ spl13_160 ),
inference(avatar_component_clause,[],[f2401]) ).
tff(f2403,plain,
( ~ subset(sK10,sK12)
| spl13_160 ),
inference(avatar_component_clause,[],[f2401]) ).
tff(f2411,plain,
( ( sK8 = sK0(sK10,sK12) )
| spl13_160 ),
inference(resolution,[],[f2403,f84]) ).
tff(f2412,plain,
( $false
| spl13_85
| spl13_160 ),
inference(forward_subsumption_resolution,[],[f2411,f726]) ).
tff(f2413,plain,
( spl13_85
| spl13_160 ),
inference(avatar_contradiction_clause,[],[f2412]) ).
tff(f2618,plain,
( better(sK10,sK9)
| weakly_better(sK9,sK10)
| ~ spl13_47
| ~ spl13_118 ),
inference(resolution,[],[f1949,f37]) ).
tff(f2619,plain,
( weakly_better(sK9,sK10)
| ~ spl13_47
| ~ spl13_118
| spl13_146 ),
inference(forward_subsumption_resolution,[],[f2618,f1781]) ).
tff(f2620,plain,
( $false
| ~ spl13_47
| ~ spl13_118
| spl13_145
| spl13_146 ),
inference(forward_subsumption_resolution,[],[f2619,f1777]) ).
tff(f2621,plain,
( ~ spl13_47
| ~ spl13_118
| spl13_145
| spl13_146 ),
inference(avatar_contradiction_clause,[],[f2620]) ).
tff(f2795,plain,
( ( sK7 = sK3(sK10,sK12,sK8) )
| ( sK8 = sK3(sK10,sK12,sK8) )
| ( sK6 = sK3(sK10,sK12,sK8) )
| spl13_85
| spl13_104 ),
inference(resolution,[],[f2387,f53]) ).
tff(f2796,plain,
( ( sK8 = sK3(sK10,sK12,sK8) )
| ( sK6 = sK3(sK10,sK12,sK8) )
| spl13_85
| spl13_104
| spl13_141 ),
inference(forward_subsumption_resolution,[],[f2795,f1642]) ).
tff(f2797,plain,
( ( sK6 = sK3(sK10,sK12,sK8) )
| spl13_85
| spl13_104
| spl13_140
| spl13_141 ),
inference(forward_subsumption_resolution,[],[f2796,f1638]) ).
tff(f2798,plain,
( spl13_139
| spl13_85
| spl13_104
| spl13_140
| spl13_141 ),
inference(avatar_split_clause,[],[f2797,f1641,f1637,f876,f725,f1633]) ).
tff(f2822,plain,
( ~ required_preference(sK8,sK7)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_141 ),
inference(superposition,[],[f46,f1643]) ).
tff(f2823,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_141 ),
inference(forward_subsumption_resolution,[],[f2822,f71]) ).
tff(f2824,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_141
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2823,f2402]) ).
tff(f2825,plain,
( ~ better(sK12,sK10)
| ~ spl13_141
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2824,f69]) ).
tff(f2826,plain,
( $false
| ~ spl13_105
| ~ spl13_141
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2825,f882]) ).
tff(f2827,plain,
( ~ spl13_105
| ~ spl13_141
| ~ spl13_160 ),
inference(avatar_contradiction_clause,[],[f2826]) ).
tff(f2847,plain,
( ~ member(sK8,sK10)
| weakly_better(sK10,sK12)
| ~ member(sK8,sK10)
| ( sK8 = sK0(sK10,sK12) )
| ~ spl13_140 ),
inference(superposition,[],[f125,f1639]) ).
tff(f2849,plain,
( ~ member(sK8,sK10)
| weakly_better(sK10,sK12)
| ( sK8 = sK0(sK10,sK12) )
| ~ spl13_140 ),
inference(duplicate_literal_removal,[],[f2847]) ).
tff(f2851,plain,
( weakly_better(sK10,sK12)
| ( sK8 = sK0(sK10,sK12) )
| ~ spl13_140 ),
inference(forward_subsumption_resolution,[],[f2849,f69]) ).
tff(f2853,plain,
( ( sK8 = sK0(sK10,sK12) )
| spl13_104
| ~ spl13_140 ),
inference(forward_subsumption_resolution,[],[f2851,f877]) ).
tff(f2855,plain,
( $false
| spl13_85
| spl13_104
| ~ spl13_140 ),
inference(forward_subsumption_resolution,[],[f2853,f726]) ).
tff(f2856,plain,
( spl13_85
| spl13_104
| ~ spl13_140 ),
inference(avatar_contradiction_clause,[],[f2855]) ).
tff(f2874,plain,
( ~ required_preference(sK8,sK6)
| ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_139 ),
inference(superposition,[],[f46,f1635]) ).
tff(f2875,plain,
( ~ subset(sK10,sK12)
| ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_139 ),
inference(forward_subsumption_resolution,[],[f2874,f72]) ).
tff(f2876,plain,
( ~ member(sK8,sK10)
| ~ better(sK12,sK10)
| ~ spl13_139
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2875,f2402]) ).
tff(f2877,plain,
( ~ better(sK12,sK10)
| ~ spl13_139
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2876,f69]) ).
tff(f2878,plain,
( $false
| ~ spl13_105
| ~ spl13_139
| ~ spl13_160 ),
inference(forward_subsumption_resolution,[],[f2877,f882]) ).
tff(f2879,plain,
( ~ spl13_105
| ~ spl13_139
| ~ spl13_160 ),
inference(avatar_contradiction_clause,[],[f2878]) ).
tff(f3049,plain,
( ! [X0: option,X1: option] :
( ( sK4(X0,sK10) = X0 )
| member(sK4(X0,sK10),sK10)
| ( sK5(X1,sK9) != X1 )
| ~ member(sK5(X1,sK9),sK9) )
| ~ spl13_146 ),
inference(resolution,[],[f1782,f49]) ).
tff(f3051,plain,
( ! [X0: option,X1: option] :
( ( sK4(X0,sK10) != X0 )
| ~ member(sK4(X0,sK10),sK10)
| ( sK5(X1,sK9) != X1 )
| ~ member(sK5(X1,sK9),sK9) )
| ~ spl13_146 ),
inference(resolution,[],[f1782,f51]) ).
tff(f3052,plain,
( spl13_11
| spl13_147
| ~ spl13_146 ),
inference(avatar_split_clause,[],[f3051,f1780,f1825,f215]) ).
tff(f3053,plain,
( spl13_11
| spl13_148
| ~ spl13_146 ),
inference(avatar_split_clause,[],[f3049,f1780,f1829,f215]) ).
cnf(s14,plain,
( spl13_17
| spl13_18 ),
inference(sat_conversion,[],[f252]) ).
cnf(s18,plain,
( ~ spl13_17
| spl13_26
| spl13_27 ),
inference(sat_conversion,[],[f300]) ).
cnf(s30,plain,
( spl13_18
| ~ spl13_27 ),
inference(sat_conversion,[],[f435]) ).
cnf(s31,plain,
( ~ spl13_18
| spl13_37
| spl13_40 ),
inference(sat_conversion,[],[f436]) ).
cnf(s39,plain,
( spl13_18
| ~ spl13_26 ),
inference(sat_conversion,[],[f473]) ).
cnf(s40,plain,
( ~ spl13_26
| spl13_45 ),
inference(sat_conversion,[],[f478]) ).
cnf(s41,plain,
( spl13_17
| spl13_45 ),
inference(sat_conversion,[],[f480]) ).
cnf(s83,plain,
( ~ spl13_85
| spl13_104
| spl13_105 ),
inference(sat_conversion,[],[f883]) ).
cnf(s86,plain,
spl13_47,
inference(sat_conversion,[],[f899]) ).
cnf(s88,plain,
( ~ spl13_37
| spl13_40
| ~ spl13_45 ),
inference(sat_conversion,[],[f910]) ).
cnf(s97,plain,
( spl13_82
| spl13_83
| spl13_101 ),
inference(sat_conversion,[],[f997]) ).
cnf(s98,plain,
( ~ spl13_82
| spl13_101 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s106,plain,
( ~ spl13_101
| ~ spl13_104
| spl13_118 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s136,plain,
( ~ spl13_11
| ~ spl13_13 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s144,plain,
( ~ spl13_85
| ~ spl13_105
| spl13_139
| spl13_140
| spl13_141 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s147,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_140 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s150,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_141 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s151,plain,
( ~ spl13_85
| ~ spl13_105
| ~ spl13_139 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s155,plain,
( spl13_13
| ~ spl13_146
| spl13_147 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s156,plain,
( spl13_13
| ~ spl13_146
| spl13_148 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s162,plain,
( ~ spl13_147
| ~ spl13_148 ),
inference(sat_conversion,[],[f2067]) ).
cnf(s171,plain,
( ~ spl13_40
| ~ spl13_118
| ~ spl13_145 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s177,plain,
( ~ spl13_27
| spl13_45 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s188,plain,
( ~ spl13_83
| spl13_101 ),
inference(sat_conversion,[],[f2358]) ).
cnf(s190,plain,
( spl13_85
| spl13_104
| spl13_105 ),
inference(sat_conversion,[],[f2366]) ).
cnf(s193,plain,
( spl13_85
| spl13_160 ),
inference(sat_conversion,[],[f2413]) ).
cnf(s200,plain,
( ~ spl13_47
| ~ spl13_118
| spl13_145
| spl13_146 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s217,plain,
( spl13_85
| spl13_104
| spl13_139
| spl13_140
| spl13_141 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s218,plain,
( ~ spl13_105
| ~ spl13_141
| ~ spl13_160 ),
inference(sat_conversion,[],[f2827]) ).
cnf(s221,plain,
( spl13_85
| spl13_104
| ~ spl13_140 ),
inference(sat_conversion,[],[f2856]) ).
cnf(s222,plain,
( ~ spl13_105
| ~ spl13_139
| ~ spl13_160 ),
inference(sat_conversion,[],[f2879]) ).
cnf(s235,plain,
( spl13_11
| ~ spl13_146
| spl13_147 ),
inference(sat_conversion,[],[f3052]) ).
cnf(s236,plain,
( spl13_11
| ~ spl13_146
| spl13_148 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s241,plain,
( spl13_85
| spl13_104 ),
inference(rat,[],[s217,s218,s222,s190,s193,s221]) ).
cnf(s242,plain,
( ~ spl13_105
| ~ spl13_85 ),
inference(rat,[],[s144,s147,s150,s151]) ).
cnf(s243,plain,
( ~ spl13_85
| spl13_104 ),
inference(rat,[],[s242,s83]) ).
cnf(s244,plain,
spl13_104,
inference(rat,[],[s243,s241]) ).
cnf(s247,plain,
spl13_101,
inference(rat,[],[s97,s98,s188]) ).
cnf(s248,plain,
spl13_118,
inference(rat,[],[s106,s244,s247]) ).
cnf(s253,plain,
( ~ spl13_146
| spl13_11 ),
inference(rat,[],[s162,s235,s236]) ).
cnf(s255,plain,
( spl13_17
| spl13_40 ),
inference(rat,[],[s31,s88,s14,s41]) ).
cnf(s256,plain,
( spl13_45
| ~ spl13_17 ),
inference(rat,[],[s18,s40,s177]) ).
cnf(s257,plain,
spl13_40,
inference(rat,[],[s18,s30,s39,s31,s88,s256,s255]) ).
cnf(s264,plain,
~ spl13_145,
inference(rat,[],[s171,s248,s257]) ).
cnf(s267,plain,
spl13_146,
inference(rat,[],[s200,s248,s86,s264]) ).
cnf(s269,plain,
spl13_11,
inference(rat,[],[s253,s267]) ).
cnf(s270,plain,
~ spl13_13,
inference(rat,[],[s136,s269]) ).
cnf(s275,plain,
spl13_148,
inference(rat,[],[s156,s267,s270]) ).
cnf(s276,plain,
spl13_147,
inference(rat,[],[s155,s267,s270]) ).
cnf(s277,plain,
$false,
inference(rat,[],[s162,s275,s276]) ).
tff(f3054,plain,
$false,
inference(avatar_sat_refutation,[],[s277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI044_1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.42 % Computer : n020.cluster.edu
% 0.09/0.42 % Model : x86_64 x86_64
% 0.09/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.42 % Memory : 8046.5625MB
% 0.09/0.42 % OS : Linux 6.8.0-71-generic
% 0.09/0.42 % CPULimit : 300
% 0.09/0.42 % WCLimit : 300
% 0.09/0.42 % DateTime : Sun Sep 27 22:08:50 UTC 2026
% 0.09/0.42 % CPUTime :
% 0.09/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.45 Running first-order model finding
% 0.09/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.53 % (3807614)Will run a generic schedule for satisfiability detection.
% 0.16/0.53 % (3807624)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2798723939:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.53 % (3807620)% WARNING: option uhcvi not known.
% 0.16/0.53 % (3807622)dis+10_1_sil=32000:sp=arity:random_seed=1340050637:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.53 % (3807619)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=48169000_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.53 % (3807625)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=626385862:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.53 % (3807620)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3173414431:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.53 % (3807621)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=274299240:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.53 % (3807623)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=442315236:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.53 % Detected minimum model sizes of [1,1]
% 0.16/0.53 % Detected maximum model sizes of [max,4]
% 0.16/0.53 % TRYING [1,1]
% 0.16/0.53 % TRYING [2,1]
% 0.16/0.53 % TRYING [1,2]
% 0.16/0.53 % TRYING [2,2]
% 0.16/0.53 % TRYING [3,1]
% 0.16/0.53 % TRYING [4,1]
% 0.16/0.53 % TRYING [3,2]
% 0.16/0.53 % TRYING [2,3]
% 0.16/0.53 % TRYING [3,3]
% 0.16/0.53 % TRYING [2,4]
% 0.16/0.53 % TRYING [5,1]
% 0.16/0.53 % TRYING [4,2]
% 0.16/0.53 % TRYING [3,4]
% 0.16/0.53 % TRYING [6,1]
% 0.16/0.53 % TRYING [5,2]
% 0.16/0.53 % (3807624) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3807614-3807624"...
% 0.16/0.53 % TRYING [4,3]
% 0.16/0.53 % (3807624)...printing done.
% 0.16/0.53 % (3807624)Refutation found. Thanks to Tanya!
% 0.16/0.53 % SZS status Unsatisfiable for theBenchmark
% 0.16/0.53 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/0.54 % (3807624)------------------------------
% 0.16/0.54 % (3807624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.54 % (3807624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.54 % (3807624)CaDiCaL version: 2.1.3
% 0.16/0.54 % (3807624)Termination reason: Refutation
% 0.16/0.54 % (3807624)Time elapsed: 0.046 s
% 0.16/0.54 % (3807624)Peak memory usage: 13 MB
% 0.16/0.54 % (3807624)Instructions burned: 132 (million)
% 0.16/0.54 % (3807614)Success in time 0.071 s
% 0.16/0.54 % Vampire exiting
%------------------------------------------------------------------------------