%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE060+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:40:47 AM UTC 2026
% Result : Theorem 214.46s 40.13s
% Output : Refutation 214.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 74
% Syntax : Number of formulae : 436 ( 106 unt; 61 def)
% Number of atoms : 1200 ( 260 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1472 ( 708 ~; 703 |; 0 &)
% ( 61 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 63 ( 61 usr; 62 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 566 ( 0 sgn 564 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f13,axiom,
! [X0] : addition(X0,multiplication(domain(X0),X0)) = multiplication(domain(X0),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain1) ).
fof(f14,axiom,
! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain2) ).
fof(f15,axiom,
! [X0] : addition(domain(X0),one) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain3) ).
fof(f17,axiom,
! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain5) ).
fof(f18,conjecture,
! [X0,X1] : domain(multiplication(domain(X0),X1)) = multiplication(domain(X0),domain(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f19,negated_conjecture,
~ ! [X0,X1] : domain(multiplication(domain(X0),X1)) = multiplication(domain(X0),domain(X1)),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
? [X0,X1] : domain(multiplication(domain(X0),X1)) != multiplication(domain(X0),domain(X1)),
inference(ennf_transformation,[],[f19]) ).
fof(f21,plain,
domain(multiplication(domain(sK0),sK1)) != multiplication(domain(sK0),domain(sK1)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f20]) ).
fof(f22,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f23,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f25,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f26,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f28,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f29,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f33,plain,
! [X0] : multiplication(domain(X0),X0) = addition(X0,multiplication(domain(X0),X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f34,plain,
! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f14]) ).
fof(f35,plain,
! [X0] : one = addition(domain(X0),one),
inference(cnf_transformation,[],[f15]) ).
fof(f37,plain,
! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1)),
inference(cnf_transformation,[],[f17]) ).
fof(f38,plain,
domain(multiplication(domain(sK0),sK1)) != multiplication(domain(sK0),domain(sK1)),
inference(cnf_transformation,[],[f21]) ).
fof(f40,definition,
( spl2_1
<=> domain(multiplication(domain(sK0),sK1)) = multiplication(domain(sK0),domain(sK1)) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f42,plain,
( domain(multiplication(domain(sK0),sK1)) != multiplication(domain(sK0),domain(sK1))
| spl2_1 ),
inference(avatar_component_clause,[],[f40]) ).
fof(f43,plain,
~ spl2_1,
inference(avatar_split_clause,[],[f38,f40]) ).
fof(f45,definition,
( spl2_2
<=> ! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1)) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f46,plain,
( ! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1))
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f47,plain,
spl2_2,
inference(avatar_split_clause,[],[f37,f45]) ).
fof(f54,definition,
( spl2_4
<=> ! [X0] : one = addition(domain(X0),one) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f55,plain,
( ! [X0] : one = addition(domain(X0),one)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f56,plain,
spl2_4,
inference(avatar_split_clause,[],[f35,f54]) ).
fof(f58,definition,
( spl2_5
<=> ! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1))) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f59,plain,
( ! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1)))
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f58]) ).
fof(f60,plain,
spl2_5,
inference(avatar_split_clause,[],[f34,f58]) ).
fof(f62,definition,
( spl2_6
<=> ! [X0] : multiplication(domain(X0),X0) = addition(X0,multiplication(domain(X0),X0)) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f63,plain,
( ! [X0] : multiplication(domain(X0),X0) = addition(X0,multiplication(domain(X0),X0))
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f64,plain,
spl2_6,
inference(avatar_split_clause,[],[f33,f62]) ).
fof(f74,definition,
( spl2_9
<=> ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f75,plain,
( ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f74]) ).
fof(f76,plain,
spl2_9,
inference(avatar_split_clause,[],[f30,f74]) ).
fof(f78,definition,
( spl2_10
<=> ! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f79,plain,
( ! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f78]) ).
fof(f80,plain,
spl2_10,
inference(avatar_split_clause,[],[f29,f78]) ).
fof(f82,definition,
( spl2_11
<=> ! [X0] : multiplication(one,X0) = X0 ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f83,plain,
( ! [X0] : multiplication(one,X0) = X0
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f84,plain,
spl2_11,
inference(avatar_split_clause,[],[f28,f82]) ).
fof(f86,definition,
( spl2_12
<=> ! [X0] : multiplication(X0,one) = X0 ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f87,plain,
( ! [X0] : multiplication(X0,one) = X0
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f88,plain,
spl2_12,
inference(avatar_split_clause,[],[f27,f86]) ).
fof(f90,definition,
( spl2_13
<=> ! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f91,plain,
( ! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2)
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f92,plain,
spl2_13,
inference(avatar_split_clause,[],[f26,f90]) ).
fof(f94,definition,
( spl2_14
<=> ! [X0] : addition(X0,X0) = X0 ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f95,plain,
( ! [X0] : addition(X0,X0) = X0
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f96,plain,
spl2_14,
inference(avatar_split_clause,[],[f25,f94]) ).
fof(f102,definition,
( spl2_16
<=> ! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f103,plain,
( ! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0)
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f104,plain,
spl2_16,
inference(avatar_split_clause,[],[f23,f102]) ).
fof(f106,definition,
( spl2_17
<=> ! [X0,X1] : addition(X0,X1) = addition(X1,X0) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f107,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X1,X0)
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f108,plain,
spl2_17,
inference(avatar_split_clause,[],[f22,f106]) ).
fof(f122,plain,
( ! [X0] : one = addition(one,domain(X0))
| ~ spl2_4
| ~ spl2_17 ),
inference(superposition,[],[f55,f107]) ).
fof(f124,definition,
( spl2_19
<=> ! [X0] : one = addition(one,domain(X0)) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f125,plain,
( ! [X0] : one = addition(one,domain(X0))
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f126,plain,
( spl2_19
| ~ spl2_4
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f122,f106,f54,f124]) ).
fof(f143,plain,
( ! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X1),domain(X0))
| ~ spl2_2
| ~ spl2_17 ),
inference(superposition,[],[f107,f46]) ).
fof(f145,definition,
( spl2_21
<=> ! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X1),domain(X0)) ),
introduced(definition,[new_symbols(definition,[spl2_21])],[avatar_definition]) ).
fof(f146,plain,
( ! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X1),domain(X0))
| ~ spl2_21 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f147,plain,
( spl2_21
| ~ spl2_2
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f143,f106,f45,f145]) ).
fof(f152,plain,
( ! [X0] : domain(multiplication(one,X0)) = domain(domain(X0))
| ~ spl2_5
| ~ spl2_11 ),
inference(superposition,[],[f59,f83]) ).
fof(f153,plain,
( ! [X2,X0,X1] : domain(addition(X2,multiplication(X0,domain(X1)))) = addition(domain(X2),domain(multiplication(X0,X1)))
| ~ spl2_2
| ~ spl2_5 ),
inference(superposition,[],[f46,f59]) ).
fof(f158,plain,
( ! [X2,X0,X1] : domain(addition(X2,multiplication(X0,domain(X1)))) = domain(addition(X2,multiplication(X0,X1)))
| ~ spl2_2
| ~ spl2_5 ),
inference(forward_demodulation,[],[f153,f46]) ).
fof(f159,plain,
( ! [X0] : domain(X0) = domain(domain(X0))
| ~ spl2_5
| ~ spl2_11 ),
inference(forward_demodulation,[],[f152,f83]) ).
fof(f166,definition,
( spl2_23
<=> ! [X2,X0,X1] : domain(addition(X2,multiplication(X0,domain(X1)))) = domain(addition(X2,multiplication(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f167,plain,
( ! [X2,X0,X1] : domain(addition(X2,multiplication(X0,domain(X1)))) = domain(addition(X2,multiplication(X0,X1)))
| ~ spl2_23 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f168,plain,
( spl2_23
| ~ spl2_2
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f158,f58,f45,f166]) ).
fof(f170,definition,
( spl2_24
<=> ! [X0] : domain(X0) = domain(domain(X0)) ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f171,plain,
( ! [X0] : domain(X0) = domain(domain(X0))
| ~ spl2_24 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f172,plain,
( spl2_24
| ~ spl2_5
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f159,f82,f58,f170]) ).
fof(f180,plain,
( ! [X0,X1] : addition(domain(X1),domain(X0)) = domain(addition(X1,domain(X0)))
| ~ spl2_2
| ~ spl2_24 ),
inference(superposition,[],[f46,f171]) ).
fof(f185,plain,
( ! [X0,X1] : domain(addition(X1,X0)) = domain(addition(X1,domain(X0)))
| ~ spl2_2
| ~ spl2_24 ),
inference(forward_demodulation,[],[f180,f46]) ).
fof(f191,definition,
( spl2_27
<=> ! [X0,X1] : domain(addition(X1,X0)) = domain(addition(X1,domain(X0))) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f192,plain,
( ! [X0,X1] : domain(addition(X1,X0)) = domain(addition(X1,domain(X0)))
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( spl2_27
| ~ spl2_2
| ~ spl2_24 ),
inference(avatar_split_clause,[],[f185,f170,f45,f191]) ).
fof(f204,plain,
( ! [X0,X1] : domain(addition(X0,X1)) = domain(addition(X1,X0))
| ~ spl2_2
| ~ spl2_21 ),
inference(superposition,[],[f46,f146]) ).
fof(f209,definition,
( spl2_28
<=> ! [X0,X1] : domain(addition(X0,X1)) = domain(addition(X1,X0)) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f210,plain,
( ! [X0,X1] : domain(addition(X0,X1)) = domain(addition(X1,X0))
| ~ spl2_28 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f211,plain,
( spl2_28
| ~ spl2_2
| ~ spl2_21 ),
inference(avatar_split_clause,[],[f204,f145,f45,f209]) ).
fof(f229,plain,
( ! [X0] : domain(addition(one,domain(X0))) = domain(one)
| ~ spl2_4
| ~ spl2_28 ),
inference(superposition,[],[f210,f55]) ).
fof(f260,plain,
( ! [X0] : domain(one) = domain(addition(one,X0))
| ~ spl2_4
| ~ spl2_27
| ~ spl2_28 ),
inference(forward_demodulation,[],[f229,f192]) ).
fof(f281,definition,
( spl2_32
<=> ! [X0] : domain(one) = domain(addition(one,X0)) ),
introduced(definition,[new_symbols(definition,[spl2_32])],[avatar_definition]) ).
fof(f282,plain,
( ! [X0] : domain(one) = domain(addition(one,X0))
| ~ spl2_32 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( spl2_32
| ~ spl2_4
| ~ spl2_27
| ~ spl2_28 ),
inference(avatar_split_clause,[],[f260,f209,f191,f54,f281]) ).
fof(f309,plain,
( ! [X0,X1] : domain(multiplication(X0,addition(one,X1))) = domain(multiplication(X0,domain(one)))
| ~ spl2_5
| ~ spl2_32 ),
inference(superposition,[],[f59,f282]) ).
fof(f316,plain,
( ! [X0,X1] : domain(multiplication(X0,addition(one,X1))) = domain(multiplication(X0,one))
| ~ spl2_5
| ~ spl2_32 ),
inference(forward_demodulation,[],[f309,f59]) ).
fof(f326,plain,
( ! [X0,X1] : domain(X0) = domain(multiplication(X0,addition(one,X1)))
| ~ spl2_5
| ~ spl2_12
| ~ spl2_32 ),
inference(forward_demodulation,[],[f316,f87]) ).
fof(f338,definition,
( spl2_39
<=> ! [X0,X1] : domain(X0) = domain(multiplication(X0,addition(one,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f339,plain,
( ! [X0,X1] : domain(X0) = domain(multiplication(X0,addition(one,X1)))
| ~ spl2_39 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f340,plain,
( spl2_39
| ~ spl2_5
| ~ spl2_12
| ~ spl2_32 ),
inference(avatar_split_clause,[],[f326,f281,f86,f58,f338]) ).
fof(f1132,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1))
| ~ spl2_14
| ~ spl2_16 ),
inference(superposition,[],[f103,f95]) ).
fof(f1134,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2))
| ~ spl2_16
| ~ spl2_17 ),
inference(superposition,[],[f103,f107]) ).
fof(f1141,plain,
( ! [X0,X1] : addition(one,X1) = addition(domain(X0),addition(one,X1))
| ~ spl2_4
| ~ spl2_16 ),
inference(superposition,[],[f103,f55]) ).
fof(f1153,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1))
| ~ spl2_16
| ~ spl2_17 ),
inference(superposition,[],[f107,f103]) ).
fof(f1173,definition,
( spl2_87
<=> ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_87])],[avatar_definition]) ).
fof(f1174,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1))
| ~ spl2_87 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1175,plain,
( spl2_87
| ~ spl2_16
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f1153,f106,f102,f1173]) ).
fof(f1189,definition,
( spl2_91
<=> ! [X0,X1] : addition(one,X1) = addition(domain(X0),addition(one,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_91])],[avatar_definition]) ).
fof(f1190,plain,
( ! [X0,X1] : addition(one,X1) = addition(domain(X0),addition(one,X1))
| ~ spl2_91 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1191,plain,
( spl2_91
| ~ spl2_4
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f1141,f102,f54,f1189]) ).
fof(f1202,definition,
( spl2_94
<=> ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)) ),
introduced(definition,[new_symbols(definition,[spl2_94])],[avatar_definition]) ).
fof(f1203,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2))
| ~ spl2_94 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1204,plain,
( spl2_94
| ~ spl2_16
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f1134,f106,f102,f1202]) ).
fof(f1206,definition,
( spl2_95
<=> ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_95])],[avatar_definition]) ).
fof(f1207,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1))
| ~ spl2_95 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1208,plain,
( spl2_95
| ~ spl2_14
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f1132,f102,f94,f1206]) ).
fof(f1210,plain,
( ! [X0,X1] : addition(one,X1) = addition(one,addition(X1,domain(X0)))
| ~ spl2_87
| ~ spl2_91 ),
inference(forward_demodulation,[],[f1190,f1174]) ).
fof(f1212,definition,
( spl2_96
<=> ! [X0,X1] : addition(one,X1) = addition(one,addition(X1,domain(X0))) ),
introduced(definition,[new_symbols(definition,[spl2_96])],[avatar_definition]) ).
fof(f1213,plain,
( ! [X0,X1] : addition(one,X1) = addition(one,addition(X1,domain(X0)))
| ~ spl2_96 ),
inference(avatar_component_clause,[],[f1212]) ).
fof(f1214,plain,
( spl2_96
| ~ spl2_87
| ~ spl2_91 ),
inference(avatar_split_clause,[],[f1210,f1189,f1173,f1212]) ).
fof(f1217,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X1,addition(X0,X1))
| ~ spl2_17
| ~ spl2_95 ),
inference(superposition,[],[f1207,f107]) ).
fof(f1221,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),addition(X0,addition(X1,X2)))
| ~ spl2_16
| ~ spl2_95 ),
inference(superposition,[],[f1207,f103]) ).
fof(f1245,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(addition(X1,X2),addition(X0,X1)))
| ~ spl2_16
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1221,f1174]) ).
fof(f1247,definition,
( spl2_97
<=> ! [X0,X1] : addition(X0,X1) = addition(X1,addition(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_97])],[avatar_definition]) ).
fof(f1248,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X1,addition(X0,X1))
| ~ spl2_97 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1249,plain,
( spl2_97
| ~ spl2_17
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1217,f1206,f106,f1247]) ).
fof(f1260,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X1,addition(addition(X1,X2),X0)))
| ~ spl2_16
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1245,f1174]) ).
fof(f1266,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X1,addition(X1,addition(X2,X0))))
| ~ spl2_16
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1260,f103]) ).
fof(f1268,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X1,addition(X2,X0)))
| ~ spl2_16
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1266,f1207]) ).
fof(f1270,definition,
( spl2_101
<=> ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X1,addition(X2,X0))) ),
introduced(definition,[new_symbols(definition,[spl2_101])],[avatar_definition]) ).
fof(f1271,plain,
( ! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X1,addition(X2,X0)))
| ~ spl2_101 ),
inference(avatar_component_clause,[],[f1270]) ).
fof(f1272,plain,
( spl2_101
| ~ spl2_16
| ~ spl2_87
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1268,f1206,f1173,f102,f1270]) ).
fof(f1459,plain,
( ! [X0,X1] : addition(X1,one) = addition(one,addition(domain(X0),X1))
| ~ spl2_19
| ~ spl2_87 ),
inference(superposition,[],[f1174,f125]) ).
fof(f1464,plain,
( ! [X2,X0,X1] : addition(X2,domain(addition(X0,X1))) = addition(domain(X0),addition(domain(X1),X2))
| ~ spl2_2
| ~ spl2_87 ),
inference(superposition,[],[f1174,f46]) ).
fof(f1498,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,X0))
| ~ spl2_87
| ~ spl2_95 ),
inference(superposition,[],[f1207,f1174]) ).
fof(f1525,definition,
( spl2_108
<=> ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,X0)) ),
introduced(definition,[new_symbols(definition,[spl2_108])],[avatar_definition]) ).
fof(f1526,plain,
( ! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,X0))
| ~ spl2_108 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1527,plain,
( spl2_108
| ~ spl2_87
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1498,f1206,f1173,f1525]) ).
fof(f1556,definition,
( spl2_113
<=> ! [X2,X0,X1] : addition(X2,domain(addition(X0,X1))) = addition(domain(X0),addition(domain(X1),X2)) ),
introduced(definition,[new_symbols(definition,[spl2_113])],[avatar_definition]) ).
fof(f1557,plain,
( ! [X2,X0,X1] : addition(X2,domain(addition(X0,X1))) = addition(domain(X0),addition(domain(X1),X2))
| ~ spl2_113 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1558,plain,
( spl2_113
| ~ spl2_2
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f1464,f1173,f45,f1556]) ).
fof(f1567,definition,
( spl2_115
<=> ! [X0,X1] : addition(X1,one) = addition(one,addition(domain(X0),X1)) ),
introduced(definition,[new_symbols(definition,[spl2_115])],[avatar_definition]) ).
fof(f1568,plain,
( ! [X0,X1] : addition(X1,one) = addition(one,addition(domain(X0),X1))
| ~ spl2_115 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1569,plain,
( spl2_115
| ~ spl2_19
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f1459,f1173,f124,f1567]) ).
fof(f2214,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(addition(X1,X0),addition(X0,X2))
| ~ spl2_94
| ~ spl2_108 ),
inference(superposition,[],[f1203,f1526]) ).
fof(f2336,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X0,addition(X2,addition(X1,X0)))
| ~ spl2_87
| ~ spl2_94
| ~ spl2_108 ),
inference(forward_demodulation,[],[f2214,f1174]) ).
fof(f2371,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X0,addition(X2,X1))
| ~ spl2_87
| ~ spl2_94
| ~ spl2_101
| ~ spl2_108 ),
inference(forward_demodulation,[],[f2336,f1271]) ).
fof(f2387,definition,
( spl2_138
<=> ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X0,addition(X2,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_138])],[avatar_definition]) ).
fof(f2388,plain,
( ! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X0,addition(X2,X1))
| ~ spl2_138 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2389,plain,
( spl2_138
| ~ spl2_87
| ~ spl2_94
| ~ spl2_101
| ~ spl2_108 ),
inference(avatar_split_clause,[],[f2371,f1525,f1270,f1202,f1173,f2387]) ).
fof(f6838,plain,
( ! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0))
| ~ spl2_9
| ~ spl2_11 ),
inference(superposition,[],[f75,f83]) ).
fof(f6859,plain,
( ! [X2,X0,X1] : addition(multiplication(X1,X2),multiplication(X0,X2)) = addition(multiplication(X1,X2),multiplication(addition(X0,X1),X2))
| ~ spl2_9
| ~ spl2_108 ),
inference(superposition,[],[f1526,f75]) ).
fof(f6896,plain,
( ! [X2,X0,X1] : addition(multiplication(X1,X2),multiplication(X0,X2)) = multiplication(addition(X1,addition(X0,X1)),X2)
| ~ spl2_9
| ~ spl2_108 ),
inference(forward_demodulation,[],[f6859,f75]) ).
fof(f6915,definition,
( spl2_201
<=> ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)) ),
introduced(definition,[new_symbols(definition,[spl2_201])],[avatar_definition]) ).
fof(f6916,plain,
( ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2))
| ~ spl2_201 ),
inference(avatar_component_clause,[],[f6915]) ).
fof(f6931,definition,
( spl2_204
<=> ! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)) ),
introduced(definition,[new_symbols(definition,[spl2_204])],[avatar_definition]) ).
fof(f6932,plain,
( ! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0))
| ~ spl2_204 ),
inference(avatar_component_clause,[],[f6931]) ).
fof(f6933,plain,
( spl2_204
| ~ spl2_9
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f6838,f82,f74,f6931]) ).
fof(f6955,plain,
( ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2))
| ~ spl2_9
| ~ spl2_97
| ~ spl2_108 ),
inference(forward_demodulation,[],[f6896,f1248]) ).
fof(f6968,plain,
( spl2_201
| ~ spl2_9
| ~ spl2_97
| ~ spl2_108 ),
inference(avatar_split_clause,[],[f6955,f1525,f1247,f74,f6915]) ).
fof(f6980,plain,
( ! [X0] : multiplication(domain(X0),X0) = multiplication(addition(one,domain(X0)),X0)
| ~ spl2_6
| ~ spl2_204 ),
inference(superposition,[],[f63,f6932]) ).
fof(f6995,plain,
( ! [X2,X0,X1] : addition(multiplication(addition(one,X0),X1),X2) = addition(X1,addition(X2,multiplication(X0,X1)))
| ~ spl2_138
| ~ spl2_204 ),
inference(superposition,[],[f2388,f6932]) ).
fof(f7013,plain,
( ! [X0,X1] : addition(multiplication(X0,domain(X1)),one) = addition(one,multiplication(addition(one,X0),domain(X1)))
| ~ spl2_115
| ~ spl2_204 ),
inference(superposition,[],[f1568,f6932]) ).
fof(f7020,definition,
( spl2_211
<=> ! [X0,X1] : addition(one,multiplication(addition(one,X0),domain(X1))) = addition(one,multiplication(X0,domain(X1))) ),
introduced(definition,[new_symbols(definition,[spl2_211])],[avatar_definition]) ).
fof(f7021,plain,
( ! [X0,X1] : addition(one,multiplication(addition(one,X0),domain(X1))) = addition(one,multiplication(X0,domain(X1)))
| ~ spl2_211 ),
inference(avatar_component_clause,[],[f7020]) ).
fof(f7023,plain,
( ! [X0,X1] : addition(one,multiplication(addition(one,X0),domain(X1))) = addition(one,multiplication(X0,domain(X1)))
| ~ spl2_17
| ~ spl2_115
| ~ spl2_204 ),
inference(forward_demodulation,[],[f7013,f107]) ).
fof(f7048,definition,
( spl2_214
<=> ! [X2,X0,X1] : addition(multiplication(addition(one,X0),X1),X2) = addition(X1,addition(X2,multiplication(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_214])],[avatar_definition]) ).
fof(f7049,plain,
( ! [X2,X0,X1] : addition(multiplication(addition(one,X0),X1),X2) = addition(X1,addition(X2,multiplication(X0,X1)))
| ~ spl2_214 ),
inference(avatar_component_clause,[],[f7048]) ).
fof(f7050,plain,
( spl2_214
| ~ spl2_138
| ~ spl2_204 ),
inference(avatar_split_clause,[],[f6995,f6931,f2387,f7048]) ).
fof(f7073,plain,
( ! [X0] : multiplication(one,X0) = multiplication(domain(X0),X0)
| ~ spl2_6
| ~ spl2_19
| ~ spl2_204 ),
inference(forward_demodulation,[],[f6980,f125]) ).
fof(f7087,plain,
( spl2_211
| ~ spl2_17
| ~ spl2_115
| ~ spl2_204 ),
inference(avatar_split_clause,[],[f7023,f6931,f1567,f106,f7020]) ).
fof(f7099,plain,
( ! [X0] : multiplication(domain(X0),X0) = X0
| ~ spl2_6
| ~ spl2_11
| ~ spl2_19
| ~ spl2_204 ),
inference(forward_demodulation,[],[f7073,f83]) ).
fof(f7109,definition,
( spl2_219
<=> ! [X0] : multiplication(domain(X0),X0) = X0 ),
introduced(definition,[new_symbols(definition,[spl2_219])],[avatar_definition]) ).
fof(f7110,plain,
( ! [X0] : multiplication(domain(X0),X0) = X0
| ~ spl2_219 ),
inference(avatar_component_clause,[],[f7109]) ).
fof(f7111,plain,
( spl2_219
| ~ spl2_6
| ~ spl2_11
| ~ spl2_19
| ~ spl2_204 ),
inference(avatar_split_clause,[],[f7099,f6931,f124,f82,f62,f7109]) ).
fof(f7114,plain,
( ! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1))
| ~ spl2_10
| ~ spl2_12 ),
inference(superposition,[],[f79,f87]) ).
fof(f7119,plain,
( ! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0)
| ~ spl2_10
| ~ spl2_12 ),
inference(superposition,[],[f79,f87]) ).
fof(f7142,plain,
( ! [X2,X0,X1] : addition(multiplication(X0,X2),multiplication(X0,X1)) = addition(multiplication(X0,X2),multiplication(X0,addition(X1,X2)))
| ~ spl2_10
| ~ spl2_108 ),
inference(superposition,[],[f1526,f79]) ).
fof(f7179,plain,
( ! [X2,X0,X1] : addition(multiplication(X0,X2),multiplication(X0,X1)) = multiplication(X0,addition(X2,addition(X1,X2)))
| ~ spl2_10
| ~ spl2_108 ),
inference(forward_demodulation,[],[f7142,f79]) ).
fof(f7198,definition,
( spl2_227
<=> ! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_227])],[avatar_definition]) ).
fof(f7199,plain,
( ! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1))
| ~ spl2_227 ),
inference(avatar_component_clause,[],[f7198]) ).
fof(f7212,plain,
( ! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1))
| ~ spl2_10
| ~ spl2_12
| ~ spl2_17 ),
inference(forward_demodulation,[],[f7119,f107]) ).
fof(f7218,definition,
( spl2_229
<=> ! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_229])],[avatar_definition]) ).
fof(f7219,plain,
( ! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1))
| ~ spl2_229 ),
inference(avatar_component_clause,[],[f7218]) ).
fof(f7220,plain,
( spl2_229
| ~ spl2_10
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f7114,f86,f78,f7218]) ).
fof(f7236,plain,
( ! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1))
| ~ spl2_10
| ~ spl2_97
| ~ spl2_108 ),
inference(forward_demodulation,[],[f7179,f1248]) ).
fof(f7245,definition,
( spl2_234
<=> ! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_234])],[avatar_definition]) ).
fof(f7246,plain,
( ! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1))
| ~ spl2_234 ),
inference(avatar_component_clause,[],[f7245]) ).
fof(f7247,plain,
( spl2_234
| ~ spl2_10
| ~ spl2_12
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f7212,f106,f86,f78,f7245]) ).
fof(f7251,plain,
( spl2_227
| ~ spl2_10
| ~ spl2_97
| ~ spl2_108 ),
inference(avatar_split_clause,[],[f7236,f1525,f1247,f78,f7198]) ).
fof(f7281,plain,
( ! [X0] : domain(X0) = multiplication(domain(X0),domain(X0))
| ~ spl2_24
| ~ spl2_219 ),
inference(superposition,[],[f7110,f171]) ).
fof(f7288,plain,
( ! [X0,X1] : addition(X0,multiplication(X1,X0)) = multiplication(addition(domain(X0),X1),X0)
| ~ spl2_9
| ~ spl2_219 ),
inference(superposition,[],[f75,f7110]) ).
fof(f7301,plain,
( ! [X0,X1] : multiplication(addition(one,X1),X0) = multiplication(addition(domain(X0),X1),X0)
| ~ spl2_9
| ~ spl2_204
| ~ spl2_219 ),
inference(forward_demodulation,[],[f7288,f6932]) ).
fof(f7310,definition,
( spl2_237
<=> ! [X0] : domain(X0) = multiplication(domain(X0),domain(X0)) ),
introduced(definition,[new_symbols(definition,[spl2_237])],[avatar_definition]) ).
fof(f7311,plain,
( ! [X0] : domain(X0) = multiplication(domain(X0),domain(X0))
| ~ spl2_237 ),
inference(avatar_component_clause,[],[f7310]) ).
fof(f7312,plain,
( spl2_237
| ~ spl2_24
| ~ spl2_219 ),
inference(avatar_split_clause,[],[f7281,f7109,f170,f7310]) ).
fof(f7360,definition,
( spl2_248
<=> ! [X0,X1] : multiplication(addition(one,X1),X0) = multiplication(addition(domain(X0),X1),X0) ),
introduced(definition,[new_symbols(definition,[spl2_248])],[avatar_definition]) ).
fof(f7361,plain,
( ! [X0,X1] : multiplication(addition(one,X1),X0) = multiplication(addition(domain(X0),X1),X0)
| ~ spl2_248 ),
inference(avatar_component_clause,[],[f7360]) ).
fof(f7362,plain,
( spl2_248
| ~ spl2_9
| ~ spl2_204
| ~ spl2_219 ),
inference(avatar_split_clause,[],[f7301,f7109,f6931,f74,f7360]) ).
fof(f7403,plain,
( ! [X0,X1] : multiplication(domain(X0),addition(domain(X0),X1)) = addition(domain(X0),multiplication(domain(X0),X1))
| ~ spl2_10
| ~ spl2_237 ),
inference(superposition,[],[f79,f7311]) ).
fof(f7406,plain,
( ! [X0,X1] : multiplication(addition(domain(X0),X1),domain(X0)) = addition(domain(X0),multiplication(X1,domain(X0)))
| ~ spl2_9
| ~ spl2_237 ),
inference(superposition,[],[f75,f7311]) ).
fof(f7412,plain,
( ! [X0,X1] : multiplication(addition(domain(X0),X1),domain(X0)) = multiplication(addition(one,X1),domain(X0))
| ~ spl2_9
| ~ spl2_204
| ~ spl2_237 ),
inference(forward_demodulation,[],[f7406,f6932]) ).
fof(f7415,plain,
( ! [X0,X1] : multiplication(domain(X0),addition(domain(X0),X1)) = multiplication(domain(X0),addition(one,X1))
| ~ spl2_10
| ~ spl2_229
| ~ spl2_237 ),
inference(forward_demodulation,[],[f7403,f7219]) ).
fof(f7419,definition,
( spl2_252
<=> ! [X0,X1] : multiplication(addition(domain(X0),X1),domain(X0)) = multiplication(addition(one,X1),domain(X0)) ),
introduced(definition,[new_symbols(definition,[spl2_252])],[avatar_definition]) ).
fof(f7420,plain,
( ! [X0,X1] : multiplication(addition(domain(X0),X1),domain(X0)) = multiplication(addition(one,X1),domain(X0))
| ~ spl2_252 ),
inference(avatar_component_clause,[],[f7419]) ).
fof(f7421,plain,
( spl2_252
| ~ spl2_9
| ~ spl2_204
| ~ spl2_237 ),
inference(avatar_split_clause,[],[f7412,f7310,f6931,f74,f7419]) ).
fof(f7425,definition,
( spl2_253
<=> ! [X0,X1] : multiplication(domain(X0),addition(domain(X0),X1)) = multiplication(domain(X0),addition(one,X1)) ),
introduced(definition,[new_symbols(definition,[spl2_253])],[avatar_definition]) ).
fof(f7426,plain,
( ! [X0,X1] : multiplication(domain(X0),addition(domain(X0),X1)) = multiplication(domain(X0),addition(one,X1))
| ~ spl2_253 ),
inference(avatar_component_clause,[],[f7425]) ).
fof(f7427,plain,
( spl2_253
| ~ spl2_10
| ~ spl2_229
| ~ spl2_237 ),
inference(avatar_split_clause,[],[f7415,f7310,f7218,f78,f7425]) ).
fof(f7722,plain,
( ! [X0] : addition(domain(X0),X0) = multiplication(domain(X0),addition(one,X0))
| ~ spl2_219
| ~ spl2_229 ),
inference(superposition,[],[f7219,f7110]) ).
fof(f7845,plain,
( ! [X0] : addition(X0,domain(X0)) = multiplication(domain(X0),addition(one,X0))
| ~ spl2_17
| ~ spl2_219
| ~ spl2_229 ),
inference(forward_demodulation,[],[f7722,f107]) ).
fof(f7868,definition,
( spl2_286
<=> ! [X0] : addition(X0,domain(X0)) = multiplication(domain(X0),addition(one,X0)) ),
introduced(definition,[new_symbols(definition,[spl2_286])],[avatar_definition]) ).
fof(f7869,plain,
( ! [X0] : addition(X0,domain(X0)) = multiplication(domain(X0),addition(one,X0))
| ~ spl2_286 ),
inference(avatar_component_clause,[],[f7868]) ).
fof(f7870,plain,
( spl2_286
| ~ spl2_17
| ~ spl2_219
| ~ spl2_229 ),
inference(avatar_split_clause,[],[f7845,f7218,f7109,f106,f7868]) ).
fof(f8452,plain,
( ! [X0,X1] : multiplication(X0,addition(one,X1)) = multiplication(X0,addition(X1,one))
| ~ spl2_229
| ~ spl2_234 ),
inference(superposition,[],[f7219,f7246]) ).
fof(f8550,definition,
( spl2_342
<=> ! [X0,X1] : multiplication(X0,addition(one,X1)) = multiplication(X0,addition(X1,one)) ),
introduced(definition,[new_symbols(definition,[spl2_342])],[avatar_definition]) ).
fof(f8551,plain,
( ! [X0,X1] : multiplication(X0,addition(one,X1)) = multiplication(X0,addition(X1,one))
| ~ spl2_342 ),
inference(avatar_component_clause,[],[f8550]) ).
fof(f8552,plain,
( spl2_342
| ~ spl2_229
| ~ spl2_234 ),
inference(avatar_split_clause,[],[f8452,f7245,f7218,f8550]) ).
fof(f9562,plain,
( ! [X0,X1] : multiplication(domain(X0),multiplication(addition(one,X0),X1)) = multiplication(addition(X0,domain(X0)),X1)
| ~ spl2_13
| ~ spl2_286 ),
inference(superposition,[],[f91,f7869]) ).
fof(f9574,definition,
( spl2_404
<=> ! [X0,X1] : multiplication(domain(X0),multiplication(addition(one,X0),X1)) = multiplication(addition(X0,domain(X0)),X1) ),
introduced(definition,[new_symbols(definition,[spl2_404])],[avatar_definition]) ).
fof(f9575,plain,
( ! [X0,X1] : multiplication(domain(X0),multiplication(addition(one,X0),X1)) = multiplication(addition(X0,domain(X0)),X1)
| ~ spl2_404 ),
inference(avatar_component_clause,[],[f9574]) ).
fof(f9576,plain,
( spl2_404
| ~ spl2_13
| ~ spl2_286 ),
inference(avatar_split_clause,[],[f9562,f7868,f90,f9574]) ).
fof(f10442,plain,
( ! [X0,X1] : multiplication(addition(one,domain(X1)),X0) = multiplication(domain(addition(X0,X1)),X0)
| ~ spl2_2
| ~ spl2_248 ),
inference(superposition,[],[f7361,f46]) ).
fof(f10548,plain,
( ! [X0,X1] : multiplication(one,X0) = multiplication(domain(addition(X0,X1)),X0)
| ~ spl2_2
| ~ spl2_19
| ~ spl2_248 ),
inference(forward_demodulation,[],[f10442,f125]) ).
fof(f10622,plain,
( ! [X0,X1] : multiplication(domain(addition(X0,X1)),X0) = X0
| ~ spl2_2
| ~ spl2_11
| ~ spl2_19
| ~ spl2_248 ),
inference(forward_demodulation,[],[f10548,f83]) ).
fof(f10642,definition,
( spl2_462
<=> ! [X0,X1] : multiplication(domain(addition(X0,X1)),X0) = X0 ),
introduced(definition,[new_symbols(definition,[spl2_462])],[avatar_definition]) ).
fof(f10643,plain,
( ! [X0,X1] : multiplication(domain(addition(X0,X1)),X0) = X0
| ~ spl2_462 ),
inference(avatar_component_clause,[],[f10642]) ).
fof(f10644,plain,
( spl2_462
| ~ spl2_2
| ~ spl2_11
| ~ spl2_19
| ~ spl2_248 ),
inference(avatar_split_clause,[],[f10622,f7360,f124,f82,f45,f10642]) ).
fof(f10700,plain,
( ! [X0,X1] : domain(X1) = multiplication(domain(domain(addition(X0,X1))),domain(X1))
| ~ spl2_21
| ~ spl2_462 ),
inference(superposition,[],[f10643,f146]) ).
fof(f10769,definition,
( spl2_466
<=> ! [X0,X1] : domain(X1) = multiplication(domain(addition(X0,X1)),domain(X1)) ),
introduced(definition,[new_symbols(definition,[spl2_466])],[avatar_definition]) ).
fof(f10770,plain,
( ! [X0,X1] : domain(X1) = multiplication(domain(addition(X0,X1)),domain(X1))
| ~ spl2_466 ),
inference(avatar_component_clause,[],[f10769]) ).
fof(f10782,plain,
( ! [X0,X1] : domain(X1) = multiplication(domain(addition(X0,X1)),domain(X1))
| ~ spl2_21
| ~ spl2_24
| ~ spl2_462 ),
inference(forward_demodulation,[],[f10700,f171]) ).
fof(f10862,plain,
( spl2_466
| ~ spl2_21
| ~ spl2_24
| ~ spl2_462 ),
inference(avatar_split_clause,[],[f10782,f10642,f170,f145,f10769]) ).
fof(f11069,plain,
( ! [X0,X1] : domain(multiplication(X0,X1)) = multiplication(domain(multiplication(X0,addition(one,X1))),domain(multiplication(X0,X1)))
| ~ spl2_229
| ~ spl2_466 ),
inference(superposition,[],[f10770,f7219]) ).
fof(f11230,plain,
( ! [X0,X1] : domain(multiplication(X0,X1)) = multiplication(domain(X0),domain(multiplication(X0,X1)))
| ~ spl2_39
| ~ spl2_229
| ~ spl2_466 ),
inference(forward_demodulation,[],[f11069,f339]) ).
fof(f11290,definition,
( spl2_507
<=> ! [X0,X1] : domain(multiplication(X0,X1)) = multiplication(domain(X0),domain(multiplication(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_507])],[avatar_definition]) ).
fof(f11291,plain,
( ! [X0,X1] : domain(multiplication(X0,X1)) = multiplication(domain(X0),domain(multiplication(X0,X1)))
| ~ spl2_507 ),
inference(avatar_component_clause,[],[f11290]) ).
fof(f11292,plain,
( spl2_507
| ~ spl2_39
| ~ spl2_229
| ~ spl2_466 ),
inference(avatar_split_clause,[],[f11230,f10769,f7218,f338,f11290]) ).
fof(f15345,plain,
( ! [X0,X1] : domain(multiplication(domain(X0),X1)) = multiplication(domain(X0),domain(multiplication(domain(X0),X1)))
| ~ spl2_24
| ~ spl2_507 ),
inference(superposition,[],[f11291,f171]) ).
fof(f15461,definition,
( spl2_797
<=> ! [X0,X1] : domain(multiplication(domain(X0),X1)) = multiplication(domain(X0),domain(multiplication(domain(X0),X1))) ),
introduced(definition,[new_symbols(definition,[spl2_797])],[avatar_definition]) ).
fof(f15462,plain,
( ! [X0,X1] : domain(multiplication(domain(X0),X1)) = multiplication(domain(X0),domain(multiplication(domain(X0),X1)))
| ~ spl2_797 ),
inference(avatar_component_clause,[],[f15461]) ).
fof(f15463,plain,
( spl2_797
| ~ spl2_24
| ~ spl2_507 ),
inference(avatar_split_clause,[],[f15345,f11290,f170,f15461]) ).
fof(f19090,plain,
( ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2)
| ~ spl2_9
| ~ spl2_201 ),
inference(superposition,[],[f75,f6916]) ).
fof(f19163,definition,
( spl2_999
<=> ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2) ),
introduced(definition,[new_symbols(definition,[spl2_999])],[avatar_definition]) ).
fof(f19164,plain,
( ! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2)
| ~ spl2_999 ),
inference(avatar_component_clause,[],[f19163]) ).
fof(f19165,plain,
( spl2_999
| ~ spl2_9
| ~ spl2_201 ),
inference(avatar_split_clause,[],[f19090,f6915,f74,f19163]) ).
fof(f19433,plain,
( ! [X2,X3,X0,X1] : multiplication(addition(multiplication(X0,X2),multiplication(X0,X1)),X3) = multiplication(multiplication(X0,addition(X1,X2)),X3)
| ~ spl2_10
| ~ spl2_999 ),
inference(superposition,[],[f19164,f79]) ).
fof(f19595,plain,
( ! [X2,X3,X0,X1] : multiplication(addition(multiplication(X0,X2),multiplication(X0,X1)),X3) = multiplication(X0,multiplication(addition(X1,X2),X3))
| ~ spl2_10
| ~ spl2_13
| ~ spl2_999 ),
inference(forward_demodulation,[],[f19433,f91]) ).
fof(f19657,plain,
( ! [X2,X3,X0,X1] : multiplication(X0,multiplication(addition(X1,X2),X3)) = multiplication(multiplication(X0,addition(X2,X1)),X3)
| ~ spl2_10
| ~ spl2_13
| ~ spl2_999 ),
inference(forward_demodulation,[],[f19595,f79]) ).
fof(f19672,plain,
( ! [X2,X3,X0,X1] : multiplication(X0,multiplication(addition(X1,X2),X3)) = multiplication(X0,multiplication(addition(X2,X1),X3))
| ~ spl2_10
| ~ spl2_13
| ~ spl2_999 ),
inference(forward_demodulation,[],[f19657,f91]) ).
fof(f19679,definition,
( spl2_1026
<=> ! [X0,X3,X2,X1] : multiplication(X0,multiplication(addition(X1,X2),X3)) = multiplication(X0,multiplication(addition(X2,X1),X3)) ),
introduced(definition,[new_symbols(definition,[spl2_1026])],[avatar_definition]) ).
fof(f19680,plain,
( ! [X2,X3,X0,X1] : multiplication(X0,multiplication(addition(X1,X2),X3)) = multiplication(X0,multiplication(addition(X2,X1),X3))
| ~ spl2_1026 ),
inference(avatar_component_clause,[],[f19679]) ).
fof(f19681,plain,
( spl2_1026
| ~ spl2_10
| ~ spl2_13
| ~ spl2_999 ),
inference(avatar_split_clause,[],[f19672,f19163,f90,f78,f19679]) ).
fof(f113566,plain,
( ! [X0,X1] : addition(addition(domain(X1),X0),multiplication(addition(one,X0),domain(X1))) = multiplication(addition(domain(X1),X0),addition(domain(X1),one))
| ~ spl2_234
| ~ spl2_252 ),
inference(superposition,[],[f7246,f7420]) ).
fof(f113589,plain,
( ! [X0,X1] : multiplication(addition(domain(X1),X0),addition(one,domain(X1))) = addition(addition(domain(X1),X0),multiplication(addition(one,X0),domain(X1)))
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113566,f8551]) ).
fof(f113710,plain,
( ! [X0,X1] : multiplication(addition(domain(X1),X0),addition(one,domain(X1))) = addition(domain(X1),addition(X0,multiplication(addition(one,X0),domain(X1))))
| ~ spl2_16
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113589,f103]) ).
fof(f113776,plain,
( ! [X0,X1] : multiplication(addition(domain(X1),X0),addition(one,domain(X1))) = addition(multiplication(addition(one,addition(one,X0)),domain(X1)),X0)
| ~ spl2_16
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113710,f7049]) ).
fof(f113796,plain,
( ! [X0,X1] : multiplication(addition(domain(X1),X0),addition(one,domain(X1))) = addition(X0,multiplication(addition(one,addition(one,X0)),domain(X1)))
| ~ spl2_16
| ~ spl2_17
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113776,f107]) ).
fof(f113807,plain,
( ! [X0,X1] : multiplication(addition(domain(X1),X0),addition(one,domain(X1))) = addition(X0,multiplication(addition(one,X0),domain(X1)))
| ~ spl2_16
| ~ spl2_17
| ~ spl2_95
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113796,f1207]) ).
fof(f113815,plain,
( ! [X0,X1] : addition(X0,multiplication(addition(one,X0),domain(X1))) = multiplication(addition(domain(X1),X0),one)
| ~ spl2_16
| ~ spl2_17
| ~ spl2_19
| ~ spl2_95
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113807,f125]) ).
fof(f113823,plain,
( ! [X0,X1] : addition(domain(X1),X0) = addition(X0,multiplication(addition(one,X0),domain(X1)))
| ~ spl2_12
| ~ spl2_16
| ~ spl2_17
| ~ spl2_19
| ~ spl2_95
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(forward_demodulation,[],[f113815,f87]) ).
fof(f113825,definition,
( spl2_4275
<=> ! [X0,X1] : addition(domain(X1),X0) = addition(X0,multiplication(addition(one,X0),domain(X1))) ),
introduced(definition,[new_symbols(definition,[spl2_4275])],[avatar_definition]) ).
fof(f113826,plain,
( ! [X0,X1] : addition(domain(X1),X0) = addition(X0,multiplication(addition(one,X0),domain(X1)))
| ~ spl2_4275 ),
inference(avatar_component_clause,[],[f113825]) ).
fof(f113832,plain,
( spl2_4275
| ~ spl2_12
| ~ spl2_16
| ~ spl2_17
| ~ spl2_19
| ~ spl2_95
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342 ),
inference(avatar_split_clause,[],[f113823,f8550,f7419,f7245,f7048,f1206,f124,f106,f102,f86,f113825]) ).
fof(f114165,plain,
( ! [X0,X1] : addition(one,addition(domain(X0),domain(X1))) = addition(multiplication(addition(one,domain(X1)),domain(X0)),one)
| ~ spl2_115
| ~ spl2_4275 ),
inference(superposition,[],[f1568,f113826]) ).
fof(f114193,plain,
( ! [X0,X1] : addition(one,addition(domain(X0),domain(X1))) = addition(one,multiplication(addition(one,domain(X1)),domain(X0)))
| ~ spl2_17
| ~ spl2_115
| ~ spl2_4275 ),
inference(forward_demodulation,[],[f114165,f107]) ).
fof(f114412,plain,
( ! [X0,X1] : addition(one,addition(domain(X0),domain(X1))) = addition(one,multiplication(domain(X1),domain(X0)))
| ~ spl2_17
| ~ spl2_115
| ~ spl2_211
| ~ spl2_4275 ),
inference(forward_demodulation,[],[f114193,f7021]) ).
fof(f114634,plain,
( ! [X0,X1] : addition(one,domain(X0)) = addition(one,multiplication(domain(X1),domain(X0)))
| ~ spl2_17
| ~ spl2_96
| ~ spl2_115
| ~ spl2_211
| ~ spl2_4275 ),
inference(forward_demodulation,[],[f114412,f1213]) ).
fof(f114785,plain,
( ! [X0,X1] : one = addition(one,multiplication(domain(X1),domain(X0)))
| ~ spl2_17
| ~ spl2_19
| ~ spl2_96
| ~ spl2_115
| ~ spl2_211
| ~ spl2_4275 ),
inference(forward_demodulation,[],[f114634,f125]) ).
fof(f114792,definition,
( spl2_4307
<=> ! [X0,X1] : one = addition(one,multiplication(domain(X1),domain(X0))) ),
introduced(definition,[new_symbols(definition,[spl2_4307])],[avatar_definition]) ).
fof(f114793,plain,
( ! [X0,X1] : one = addition(one,multiplication(domain(X1),domain(X0)))
| ~ spl2_4307 ),
inference(avatar_component_clause,[],[f114792]) ).
fof(f114923,plain,
( spl2_4307
| ~ spl2_17
| ~ spl2_19
| ~ spl2_96
| ~ spl2_115
| ~ spl2_211
| ~ spl2_4275 ),
inference(avatar_split_clause,[],[f114785,f113825,f7020,f1567,f1212,f124,f106,f114792]) ).
fof(f121923,plain,
( ! [X0,X1] : multiplication(domain(X0),domain(addition(X0,X1))) = multiplication(domain(X0),addition(one,domain(X1)))
| ~ spl2_2
| ~ spl2_253 ),
inference(superposition,[],[f7426,f46]) ).
fof(f122150,plain,
( ! [X0,X1] : multiplication(domain(X0),one) = multiplication(domain(X0),domain(addition(X0,X1)))
| ~ spl2_2
| ~ spl2_19
| ~ spl2_253 ),
inference(forward_demodulation,[],[f121923,f125]) ).
fof(f122213,plain,
( ! [X0,X1] : domain(X0) = multiplication(domain(X0),domain(addition(X0,X1)))
| ~ spl2_2
| ~ spl2_12
| ~ spl2_19
| ~ spl2_253 ),
inference(forward_demodulation,[],[f122150,f87]) ).
fof(f122256,definition,
( spl2_4414
<=> ! [X0,X1] : domain(X0) = multiplication(domain(X0),domain(addition(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_4414])],[avatar_definition]) ).
fof(f122257,plain,
( ! [X0,X1] : domain(X0) = multiplication(domain(X0),domain(addition(X0,X1)))
| ~ spl2_4414 ),
inference(avatar_component_clause,[],[f122256]) ).
fof(f122258,plain,
( spl2_4414
| ~ spl2_2
| ~ spl2_12
| ~ spl2_19
| ~ spl2_253 ),
inference(avatar_split_clause,[],[f122213,f7425,f124,f86,f45,f122256]) ).
fof(f237943,plain,
( ! [X2,X0,X1] : multiplication(domain(X0),addition(domain(multiplication(domain(X0),X1)),X2)) = addition(multiplication(domain(X0),X2),domain(multiplication(domain(X0),X1)))
| ~ spl2_227
| ~ spl2_797 ),
inference(superposition,[],[f7199,f15462]) ).
fof(f237994,definition,
( spl2_9742
<=> ! [X2,X0,X1] : multiplication(domain(X0),addition(domain(multiplication(domain(X0),X1)),X2)) = addition(multiplication(domain(X0),X2),domain(multiplication(domain(X0),X1))) ),
introduced(definition,[new_symbols(definition,[spl2_9742])],[avatar_definition]) ).
fof(f237995,plain,
( ! [X2,X0,X1] : multiplication(domain(X0),addition(domain(multiplication(domain(X0),X1)),X2)) = addition(multiplication(domain(X0),X2),domain(multiplication(domain(X0),X1)))
| ~ spl2_9742 ),
inference(avatar_component_clause,[],[f237994]) ).
fof(f237996,plain,
( spl2_9742
| ~ spl2_227
| ~ spl2_797 ),
inference(avatar_split_clause,[],[f237943,f15461,f7198,f237994]) ).
fof(f457151,plain,
( ! [X2,X0,X1] : addition(multiplication(one,X1),X2) = addition(X1,addition(X2,multiplication(domain(X0),X1)))
| ~ spl2_19
| ~ spl2_214 ),
inference(superposition,[],[f7049,f125]) ).
fof(f461398,plain,
( ! [X2,X0,X1] : addition(X1,X2) = addition(X1,addition(X2,multiplication(domain(X0),X1)))
| ~ spl2_11
| ~ spl2_19
| ~ spl2_214 ),
inference(forward_demodulation,[],[f457151,f83]) ).
fof(f462564,definition,
( spl2_19617
<=> ! [X2,X0,X1] : addition(X1,X2) = addition(X1,addition(X2,multiplication(domain(X0),X1))) ),
introduced(definition,[new_symbols(definition,[spl2_19617])],[avatar_definition]) ).
fof(f462565,plain,
( ! [X2,X0,X1] : addition(X1,X2) = addition(X1,addition(X2,multiplication(domain(X0),X1)))
| ~ spl2_19617 ),
inference(avatar_component_clause,[],[f462564]) ).
fof(f462566,plain,
( spl2_19617
| ~ spl2_11
| ~ spl2_19
| ~ spl2_214 ),
inference(avatar_split_clause,[],[f461398,f7048,f124,f82,f462564]) ).
fof(f464655,plain,
( ! [X2,X0,X1] : addition(domain(X0),domain(X1)) = addition(multiplication(domain(X2),domain(X0)),domain(addition(X0,X1)))
| ~ spl2_113
| ~ spl2_19617 ),
inference(superposition,[],[f1557,f462565]) ).
fof(f464734,plain,
( ! [X2,X0,X1] : domain(addition(X0,X1)) = addition(multiplication(domain(X2),domain(X0)),domain(addition(X0,X1)))
| ~ spl2_2
| ~ spl2_113
| ~ spl2_19617 ),
inference(forward_demodulation,[],[f464655,f46]) ).
fof(f465388,definition,
( spl2_19762
<=> ! [X2,X0,X1] : domain(addition(X0,X1)) = addition(multiplication(domain(X2),domain(X0)),domain(addition(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_19762])],[avatar_definition]) ).
fof(f465389,plain,
( ! [X2,X0,X1] : domain(addition(X0,X1)) = addition(multiplication(domain(X2),domain(X0)),domain(addition(X0,X1)))
| ~ spl2_19762 ),
inference(avatar_component_clause,[],[f465388]) ).
fof(f465390,plain,
( spl2_19762
| ~ spl2_2
| ~ spl2_113
| ~ spl2_19617 ),
inference(avatar_split_clause,[],[f464734,f462564,f1556,f45,f465388]) ).
fof(f695000,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(addition(multiplication(domain(X0),domain(X1)),domain(multiplication(domain(X0),domain(X1)))),X2)
| ~ spl2_404
| ~ spl2_4307 ),
inference(superposition,[],[f9575,f114793]) ).
fof(f695826,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(multiplication(domain(X0),addition(domain(multiplication(domain(X0),domain(X1))),domain(X1))),X2)
| ~ spl2_404
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f695000,f237995]) ).
fof(f696322,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(addition(domain(multiplication(domain(X0),domain(X1))),domain(X1)),X2))
| ~ spl2_13
| ~ spl2_404
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f695826,f91]) ).
fof(f696784,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(addition(domain(X1),domain(multiplication(domain(X0),domain(X1)))),X2))
| ~ spl2_13
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f696322,f19680]) ).
fof(f697078,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(domain(addition(X1,multiplication(domain(X0),domain(X1)))),X2))
| ~ spl2_2
| ~ spl2_13
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f696784,f46]) ).
fof(f697346,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(domain(addition(X1,multiplication(domain(X0),X1))),X2))
| ~ spl2_2
| ~ spl2_13
| ~ spl2_23
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697078,f167]) ).
fof(f697505,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(domain(multiplication(addition(one,domain(X0)),X1)),X2))
| ~ spl2_2
| ~ spl2_13
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697346,f6932]) ).
fof(f697651,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2)) = multiplication(domain(X0),multiplication(domain(multiplication(one,X1)),X2))
| ~ spl2_2
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697505,f125]) ).
fof(f697706,plain,
( ! [X2,X0,X1] : multiplication(domain(X0),multiplication(domain(X1),X2)) = multiplication(domain(multiplication(domain(X0),domain(X1))),multiplication(one,X2))
| ~ spl2_2
| ~ spl2_11
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697651,f83]) ).
fof(f697731,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),domain(X1))),X2) = multiplication(domain(X0),multiplication(domain(X1),X2))
| ~ spl2_2
| ~ spl2_11
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697706,f83]) ).
fof(f697741,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),X1)),X2) = multiplication(domain(X0),multiplication(domain(X1),X2))
| ~ spl2_2
| ~ spl2_5
| ~ spl2_11
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(forward_demodulation,[],[f697731,f59]) ).
fof(f697745,definition,
( spl2_28239
<=> ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),X1)),X2) = multiplication(domain(X0),multiplication(domain(X1),X2)) ),
introduced(definition,[new_symbols(definition,[spl2_28239])],[avatar_definition]) ).
fof(f697746,plain,
( ! [X2,X0,X1] : multiplication(domain(multiplication(domain(X0),X1)),X2) = multiplication(domain(X0),multiplication(domain(X1),X2))
| ~ spl2_28239 ),
inference(avatar_component_clause,[],[f697745]) ).
fof(f697747,plain,
( spl2_28239
| ~ spl2_2
| ~ spl2_5
| ~ spl2_11
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742 ),
inference(avatar_split_clause,[],[f697741,f237994,f114792,f19679,f9574,f6931,f166,f124,f90,f82,f58,f45,f697745]) ).
fof(f726552,plain,
( ! [X2,X0,X1] : domain(multiplication(domain(X2),domain(X0))) = multiplication(domain(multiplication(domain(X2),domain(X0))),domain(domain(addition(X0,X1))))
| ~ spl2_4414
| ~ spl2_19762 ),
inference(superposition,[],[f122257,f465389]) ).
fof(f726622,plain,
( ! [X2,X0,X1] : domain(multiplication(domain(X2),domain(X0))) = multiplication(domain(X2),multiplication(domain(domain(X0)),domain(domain(addition(X0,X1)))))
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(forward_demodulation,[],[f726552,f697746]) ).
fof(f727577,plain,
( ! [X2,X0,X1] : domain(multiplication(domain(X2),domain(X0))) = multiplication(domain(X2),multiplication(domain(domain(X0)),domain(addition(X0,X1))))
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(forward_demodulation,[],[f726622,f171]) ).
fof(f728102,plain,
( ! [X2,X0,X1] : domain(multiplication(domain(X2),domain(X0))) = multiplication(domain(X2),multiplication(domain(X0),domain(addition(X0,X1))))
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(forward_demodulation,[],[f727577,f171]) ).
fof(f728493,plain,
( ! [X2,X0] : multiplication(domain(X2),domain(X0)) = domain(multiplication(domain(X2),domain(X0)))
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(forward_demodulation,[],[f728102,f122257]) ).
fof(f728757,plain,
( ! [X2,X0] : multiplication(domain(X2),domain(X0)) = domain(multiplication(domain(X2),X0))
| ~ spl2_5
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(forward_demodulation,[],[f728493,f59]) ).
fof(f728868,definition,
( spl2_29270
<=> ! [X2,X0] : multiplication(domain(X2),domain(X0)) = domain(multiplication(domain(X2),X0)) ),
introduced(definition,[new_symbols(definition,[spl2_29270])],[avatar_definition]) ).
fof(f728869,plain,
( ! [X2,X0] : multiplication(domain(X2),domain(X0)) = domain(multiplication(domain(X2),X0))
| ~ spl2_29270 ),
inference(avatar_component_clause,[],[f728868]) ).
fof(f728874,plain,
( spl2_29270
| ~ spl2_5
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239 ),
inference(avatar_split_clause,[],[f728757,f697745,f465388,f122256,f170,f58,f728868]) ).
fof(f729006,plain,
( $false
| spl2_1
| ~ spl2_29270 ),
inference(backward_subsumption_resolution,[],[f42,f728869]) ).
fof(f729007,plain,
( spl2_1
| ~ spl2_29270 ),
inference(avatar_contradiction_clause,[],[f729006]) ).
cnf(s1,plain,
~ spl2_1,
inference(sat_conversion,[],[f43]) ).
cnf(s2,plain,
spl2_2,
inference(sat_conversion,[],[f47]) ).
cnf(s4,plain,
spl2_4,
inference(sat_conversion,[],[f56]) ).
cnf(s5,plain,
spl2_5,
inference(sat_conversion,[],[f60]) ).
cnf(s6,plain,
spl2_6,
inference(sat_conversion,[],[f64]) ).
cnf(s9,plain,
spl2_9,
inference(sat_conversion,[],[f76]) ).
cnf(s10,plain,
spl2_10,
inference(sat_conversion,[],[f80]) ).
cnf(s11,plain,
spl2_11,
inference(sat_conversion,[],[f84]) ).
cnf(s12,plain,
spl2_12,
inference(sat_conversion,[],[f88]) ).
cnf(s13,plain,
spl2_13,
inference(sat_conversion,[],[f92]) ).
cnf(s14,plain,
spl2_14,
inference(sat_conversion,[],[f96]) ).
cnf(s16,plain,
spl2_16,
inference(sat_conversion,[],[f104]) ).
cnf(s17,plain,
spl2_17,
inference(sat_conversion,[],[f108]) ).
cnf(s19,plain,
( ~ spl2_4
| ~ spl2_17
| spl2_19 ),
inference(sat_conversion,[],[f126]) ).
cnf(s27,plain,
( ~ spl2_2
| ~ spl2_17
| spl2_21 ),
inference(sat_conversion,[],[f147]) ).
cnf(s32,plain,
( ~ spl2_2
| ~ spl2_5
| spl2_23 ),
inference(sat_conversion,[],[f168]) ).
cnf(s33,plain,
( ~ spl2_5
| ~ spl2_11
| spl2_24 ),
inference(sat_conversion,[],[f172]) ).
cnf(s36,plain,
( ~ spl2_2
| ~ spl2_24
| spl2_27 ),
inference(sat_conversion,[],[f193]) ).
cnf(s37,plain,
( ~ spl2_2
| ~ spl2_21
| spl2_28 ),
inference(sat_conversion,[],[f211]) ).
cnf(s44,plain,
( ~ spl2_4
| ~ spl2_27
| ~ spl2_28
| spl2_32 ),
inference(sat_conversion,[],[f283]) ).
cnf(s62,plain,
( ~ spl2_5
| ~ spl2_12
| ~ spl2_32
| spl2_39 ),
inference(sat_conversion,[],[f340]) ).
cnf(s124,plain,
( ~ spl2_16
| ~ spl2_17
| spl2_87 ),
inference(sat_conversion,[],[f1175]) ).
cnf(s133,plain,
( ~ spl2_4
| ~ spl2_16
| spl2_91 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s136,plain,
( ~ spl2_16
| ~ spl2_17
| spl2_94 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s138,plain,
( ~ spl2_14
| ~ spl2_16
| spl2_95 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s139,plain,
( ~ spl2_87
| ~ spl2_91
| spl2_96 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s140,plain,
( ~ spl2_17
| ~ spl2_95
| spl2_97 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s147,plain,
( ~ spl2_16
| ~ spl2_87
| ~ spl2_95
| spl2_101 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s155,plain,
( ~ spl2_87
| ~ spl2_95
| spl2_108 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s163,plain,
( ~ spl2_2
| ~ spl2_87
| spl2_113 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s165,plain,
( ~ spl2_19
| ~ spl2_87
| spl2_115 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s208,plain,
( ~ spl2_87
| ~ spl2_94
| ~ spl2_101
| ~ spl2_108
| spl2_138 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s374,plain,
( ~ spl2_9
| ~ spl2_11
| spl2_204 ),
inference(sat_conversion,[],[f6933]) ).
cnf(s386,plain,
( ~ spl2_9
| ~ spl2_97
| ~ spl2_108
| spl2_201 ),
inference(sat_conversion,[],[f6968]) ).
cnf(s390,plain,
( ~ spl2_138
| ~ spl2_204
| spl2_214 ),
inference(sat_conversion,[],[f7050]) ).
cnf(s398,plain,
( ~ spl2_17
| ~ spl2_115
| ~ spl2_204
| spl2_211 ),
inference(sat_conversion,[],[f7087]) ).
cnf(s409,plain,
( ~ spl2_6
| ~ spl2_11
| ~ spl2_19
| ~ spl2_204
| spl2_219 ),
inference(sat_conversion,[],[f7111]) ).
cnf(s425,plain,
( ~ spl2_10
| ~ spl2_12
| spl2_229 ),
inference(sat_conversion,[],[f7220]) ).
cnf(s434,plain,
( ~ spl2_10
| ~ spl2_12
| ~ spl2_17
| spl2_234 ),
inference(sat_conversion,[],[f7247]) ).
cnf(s436,plain,
( ~ spl2_10
| ~ spl2_97
| ~ spl2_108
| spl2_227 ),
inference(sat_conversion,[],[f7251]) ).
cnf(s439,plain,
( ~ spl2_24
| ~ spl2_219
| spl2_237 ),
inference(sat_conversion,[],[f7312]) ).
cnf(s451,plain,
( ~ spl2_9
| ~ spl2_204
| ~ spl2_219
| spl2_248 ),
inference(sat_conversion,[],[f7362]) ).
cnf(s455,plain,
( ~ spl2_9
| ~ spl2_204
| ~ spl2_237
| spl2_252 ),
inference(sat_conversion,[],[f7421]) ).
cnf(s456,plain,
( ~ spl2_10
| ~ spl2_229
| ~ spl2_237
| spl2_253 ),
inference(sat_conversion,[],[f7427]) ).
cnf(s522,plain,
( ~ spl2_17
| ~ spl2_219
| ~ spl2_229
| spl2_286 ),
inference(sat_conversion,[],[f7870]) ).
cnf(s604,plain,
( ~ spl2_229
| ~ spl2_234
| spl2_342 ),
inference(sat_conversion,[],[f8552]) ).
cnf(s697,plain,
( ~ spl2_13
| ~ spl2_286
| spl2_404 ),
inference(sat_conversion,[],[f9576]) ).
cnf(s791,plain,
( ~ spl2_2
| ~ spl2_11
| ~ spl2_19
| ~ spl2_248
| spl2_462 ),
inference(sat_conversion,[],[f10644]) ).
cnf(s817,plain,
( ~ spl2_21
| ~ spl2_24
| ~ spl2_462
| spl2_466 ),
inference(sat_conversion,[],[f10862]) ).
cnf(s851,plain,
( ~ spl2_39
| ~ spl2_229
| ~ spl2_466
| spl2_507 ),
inference(sat_conversion,[],[f11292]) ).
cnf(s1211,plain,
( ~ spl2_24
| ~ spl2_507
| spl2_797 ),
inference(sat_conversion,[],[f15463]) ).
cnf(s1466,plain,
( ~ spl2_9
| ~ spl2_201
| spl2_999 ),
inference(sat_conversion,[],[f19165]) ).
cnf(s1538,plain,
( ~ spl2_10
| ~ spl2_13
| ~ spl2_999
| spl2_1026 ),
inference(sat_conversion,[],[f19681]) ).
cnf(s6870,plain,
( ~ spl2_12
| ~ spl2_16
| ~ spl2_17
| ~ spl2_19
| ~ spl2_95
| ~ spl2_214
| ~ spl2_234
| ~ spl2_252
| ~ spl2_342
| spl2_4275 ),
inference(sat_conversion,[],[f113832]) ).
cnf(s6950,plain,
( ~ spl2_17
| ~ spl2_19
| ~ spl2_96
| ~ spl2_115
| ~ spl2_211
| ~ spl2_4275
| spl2_4307 ),
inference(sat_conversion,[],[f114923]) ).
cnf(s7132,plain,
( ~ spl2_2
| ~ spl2_12
| ~ spl2_19
| ~ spl2_253
| spl2_4414 ),
inference(sat_conversion,[],[f122258]) ).
cnf(s14887,plain,
( ~ spl2_227
| ~ spl2_797
| spl2_9742 ),
inference(sat_conversion,[],[f237996]) ).
cnf(s34530,plain,
( ~ spl2_11
| ~ spl2_19
| ~ spl2_214
| spl2_19617 ),
inference(sat_conversion,[],[f462566]) ).
cnf(s34857,plain,
( ~ spl2_2
| ~ spl2_113
| ~ spl2_19617
| spl2_19762 ),
inference(sat_conversion,[],[f465390]) ).
cnf(s48200,plain,
( ~ spl2_2
| ~ spl2_5
| ~ spl2_11
| ~ spl2_13
| ~ spl2_19
| ~ spl2_23
| ~ spl2_204
| ~ spl2_404
| ~ spl2_1026
| ~ spl2_4307
| ~ spl2_9742
| spl2_28239 ),
inference(sat_conversion,[],[f697747]) ).
cnf(s49962,plain,
( ~ spl2_5
| ~ spl2_24
| ~ spl2_4414
| ~ spl2_19762
| ~ spl2_28239
| spl2_29270 ),
inference(sat_conversion,[],[f728874]) ).
cnf(s49965,plain,
( spl2_1
| ~ spl2_29270 ),
inference(sat_conversion,[],[f729007]) ).
cnf(s49966,plain,
spl2_94,
inference(rat,[],[s136,s17,s16]) ).
cnf(s49967,plain,
spl2_87,
inference(rat,[],[s124,s17,s16]) ).
cnf(s50350,plain,
spl2_95,
inference(rat,[],[s138,s16,s14]) ).
cnf(s50353,plain,
spl2_108,
inference(rat,[],[s155,s49967,s50350]) ).
cnf(s50355,plain,
spl2_97,
inference(rat,[],[s140,s17,s50350]) ).
cnf(s50356,plain,
spl2_101,
inference(rat,[],[s147,s49967,s16,s50350]) ).
cnf(s50396,plain,
spl2_138,
inference(rat,[],[s208,s50353,s49967,s49966,s50356]) ).
cnf(s50533,plain,
spl2_227,
inference(rat,[],[s436,s50355,s50353,s10]) ).
cnf(s50534,plain,
spl2_234,
inference(rat,[],[s434,s12,s17,s10]) ).
cnf(s50538,plain,
spl2_229,
inference(rat,[],[s425,s12,s10]) ).
cnf(s50651,plain,
spl2_342,
inference(rat,[],[s604,s50534,s50538]) ).
cnf(s51613,plain,
spl2_201,
inference(rat,[],[s386,s50355,s50353,s9]) ).
cnf(s51619,plain,
spl2_204,
inference(rat,[],[s374,s11,s9]) ).
cnf(s51661,plain,
spl2_999,
inference(rat,[],[s1466,s9,s51613]) ).
cnf(s51957,plain,
spl2_214,
inference(rat,[],[s390,s50396,s51619]) ).
cnf(s52141,plain,
spl2_1026,
inference(rat,[],[s1538,s10,s13,s51661]) ).
cnf(s54755,plain,
spl2_24,
inference(rat,[],[s33,s11,s5]) ).
cnf(s54764,plain,
spl2_91,
inference(rat,[],[s133,s16,s4]) ).
cnf(s54765,plain,
spl2_19,
inference(rat,[],[s19,s17,s4]) ).
cnf(s54784,plain,
spl2_96,
inference(rat,[],[s139,s49967,s54764]) ).
cnf(s54790,plain,
spl2_19617,
inference(rat,[],[s34530,s51957,s11,s54765]) ).
cnf(s54797,plain,
spl2_115,
inference(rat,[],[s165,s49967,s54765]) ).
cnf(s54801,plain,
spl2_219,
inference(rat,[],[s409,s6,s51619,s11,s54765]) ).
cnf(s55065,plain,
spl2_211,
inference(rat,[],[s398,s51619,s17,s54797]) ).
cnf(s55091,plain,
spl2_286,
inference(rat,[],[s522,s50538,s17,s54801]) ).
cnf(s55093,plain,
spl2_237,
inference(rat,[],[s439,s54755,s54801]) ).
cnf(s55103,plain,
spl2_248,
inference(rat,[],[s451,s51619,s9,s54801]) ).
cnf(s55827,plain,
spl2_404,
inference(rat,[],[s697,s13,s55091]) ).
cnf(s55870,plain,
spl2_253,
inference(rat,[],[s456,s50538,s10,s55093]) ).
cnf(s55874,plain,
spl2_252,
inference(rat,[],[s455,s51619,s9,s55093]) ).
cnf(s56354,plain,
spl2_4275,
inference(rat,[],[s6870,s54765,s50651,s51957,s50534,s12,s50350,s16,s17,s55874]) ).
cnf(s56895,plain,
spl2_4307,
inference(rat,[],[s6950,s55065,s54797,s54784,s54765,s17,s56354]) ).
cnf(s57231,plain,
spl2_4414,
inference(rat,[],[s7132,s55870,s54765,s12,s2]) ).
cnf(s57235,plain,
spl2_462,
inference(rat,[],[s791,s55103,s54765,s11,s2]) ).
cnf(s57240,plain,
spl2_113,
inference(rat,[],[s163,s49967,s2]) ).
cnf(s57242,plain,
spl2_27,
inference(rat,[],[s36,s54755,s2]) ).
cnf(s57244,plain,
spl2_23,
inference(rat,[],[s32,s5,s2]) ).
cnf(s57246,plain,
spl2_21,
inference(rat,[],[s27,s17,s2]) ).
cnf(s57714,plain,
spl2_19762,
inference(rat,[],[s34857,s2,s54790,s57240]) ).
cnf(s58002,plain,
spl2_466,
inference(rat,[],[s817,s57235,s54755,s57246]) ).
cnf(s58008,plain,
spl2_28,
inference(rat,[],[s37,s2,s57246]) ).
cnf(s60112,plain,
spl2_32,
inference(rat,[],[s44,s57242,s4,s58008]) ).
cnf(s62751,plain,
spl2_39,
inference(rat,[],[s62,s5,s12,s60112]) ).
cnf(s65504,plain,
spl2_507,
inference(rat,[],[s851,s58002,s50538,s62751]) ).
cnf(s68880,plain,
spl2_797,
inference(rat,[],[s1211,s54755,s65504]) ).
cnf(s70195,plain,
spl2_9742,
inference(rat,[],[s14887,s50533,s68880]) ).
cnf(s72657,plain,
spl2_28239,
inference(rat,[],[s48200,s57244,s2,s56895,s52141,s55827,s51619,s54765,s5,s13,s11,s70195]) ).
cnf(s76270,plain,
spl2_29270,
inference(rat,[],[s49962,s57714,s57231,s54755,s5,s72657]) ).
cnf(s78852,plain,
spl2_1,
inference(rat,[],[s49965,s76270]) ).
cnf(s79222,plain,
$false,
inference(rat,[],[s1,s78852]) ).
fof(f729008,plain,
$false,
inference(avatar_sat_refutation,[],[s79222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE060+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 13:08:05 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 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
% 7.76/1.55 % (2374055)Will run a generic schedule for satisfiability detection.
% 7.76/1.55 % (2374061)% WARNING: option uhcvi not known.
% 7.76/1.55 % (2374064)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=35826599:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.76/1.55 % (2374065)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2652695615:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.76/1.55 % (2374060)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3372663845_2999 on theBenchmark for (2999ds/0Mi)
% 7.76/1.55 % (2374063)dis+10_1_sil=32000:sp=arity:random_seed=3350742351:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.76/1.55 % (2374061)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2503118068:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.76/1.55 % (2374062)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=285233726:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.76/1.55 % (2374066)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=735567811:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.76/1.55 % TRYING [1]
% 7.76/1.55 % TRYING [2]
% 7.76/1.55 % TRYING [3]
% 7.76/1.55 % TRYING [4]
% 7.76/1.55 % TRYING [5]
% 7.76/1.55 % (2374063)Instruction limit reached!
% 7.76/1.55 % (2374063)------------------------------
% 7.76/1.55 % (2374063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.55 % (2374063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.55 % (2374063)CaDiCaL version: 2.1.3
% 7.76/1.55 % (2374063)Termination reason: Instruction limit
% 7.76/1.55 % (2374063)Termination phase: Saturation
% 7.76/1.55 % (2374063)Time elapsed: 0.032 s
% 7.76/1.55 % (2374063)Peak memory usage: 12 MB
% 7.76/1.55 % (2374063)Instructions burned: 105 (million)
% 7.76/1.55 % (2374064)Instruction limit reached!
% 7.76/1.55 % (2374064)------------------------------
% 7.76/1.55 % (2374064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.55 % (2374064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.55 % (2374064)CaDiCaL version: 2.1.3
% 7.76/1.55 % (2374064)Termination reason: Instruction limit
% 7.76/1.55 % (2374064)Termination phase: Saturation
% 7.76/1.55 % (2374064)Time elapsed: 0.037 s
% 7.76/1.55 % (2374064)Peak memory usage: 12 MB
% 7.76/1.55 % (2374064)Instructions burned: 118 (million)
% 7.76/1.55 % (2374065)Instruction limit reached!
% 7.76/1.55 % (2374065)------------------------------
% 7.76/1.55 % (2374065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.55 % (2374065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.55 % (2374065)CaDiCaL version: 2.1.3
% 7.76/1.55 % (2374065)Termination reason: Instruction limit
% 7.76/1.55 % (2374065)Termination phase: Saturation
% 7.76/1.55 % (2374065)Time elapsed: 0.039 s
% 7.76/1.55 % (2374065)Peak memory usage: 12 MB
% 7.76/1.55 % (2374065)Instructions burned: 134 (million)
% 7.76/1.55 % (2374074)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4253342080:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.76/1.55 % TRYING [1]
% 7.76/1.55 % TRYING [2]
% 7.76/1.55 % TRYING [3]
% 7.76/1.55 % (2374075)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4135228908:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.76/1.55 % TRYING [6]
% 7.76/1.55 % (2374076)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3485338482:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.76/1.55 % TRYING [4]
% 7.76/1.55 % (2374066)Instruction limit reached!
% 7.76/1.55 % (2374066)------------------------------
% 7.76/1.55 % (2374066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.55 % (2374066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.55 % (2374066)CaDiCaL version: 2.1.3
% 7.76/1.55 % (2374066)Termination reason: Instruction limit
% 7.76/1.55 % (2374066)Termination phase: Saturation
% 7.76/1.55 % (2374066)Time elapsed: 0.051 s
% 7.76/1.55 % (2374066)Peak memory usage: 12 MB
% 7.76/1.55 % (2374066)Instructions burned: 159 (million)
% 7.76/1.55 % TRYING [5]
% 7.76/1.55 % (2374080)ott-21_1_sil=16000:fs=off:random_seed=207427292:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.76/1.55 % (2374075)Instruction limit reached!
% 7.76/1.55 % (2374075)------------------------------
% 7.76/1.55 % (2374075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374075)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374075)Termination reason: Instruction limit
% 25.88/4.07 % (2374075)Termination phase: Saturation
% 25.88/4.07 % (2374075)Time elapsed: 0.045 s
% 25.88/4.07 % (2374075)Peak memory usage: 13 MB
% 25.88/4.07 % (2374075)Instructions burned: 134 (million)
% 25.88/4.07 % TRYING [6]
% 25.88/4.07 % (2374082)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1160150619:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 25.88/4.07 % (2374080)Instruction limit reached!
% 25.88/4.07 % (2374080)------------------------------
% 25.88/4.07 % (2374080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374080)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374080)Termination reason: Instruction limit
% 25.88/4.07 % (2374080)Termination phase: Saturation
% 25.88/4.07 % (2374080)Time elapsed: 0.041 s
% 25.88/4.07 % (2374080)Peak memory usage: 12 MB
% 25.88/4.07 % (2374080)Instructions burned: 182 (million)
% 25.88/4.07 % (2374084)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2006007664:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 25.88/4.07 % TRYING [1]
% 25.88/4.07 % TRYING [2]
% 25.88/4.07 % TRYING [3]
% 25.88/4.07 % TRYING [4]
% 25.88/4.07 % TRYING [5]
% 25.88/4.07 % TRYING [7]
% 25.88/4.07 % TRYING [6]
% 25.88/4.07 % TRYING [7]
% 25.88/4.07 % (2374074)Instruction limit reached!
% 25.88/4.07 % (2374074)------------------------------
% 25.88/4.07 % (2374074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374074)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374074)Termination reason: Instruction limit
% 25.88/4.07 % (2374074)Termination phase: Finite model building constraint generation
% 25.88/4.07 % (2374074)Time elapsed: 0.179 s
% 25.88/4.07 % (2374074)Peak memory usage: 31 MB
% 25.88/4.07 % (2374074)Instructions burned: 717 (million)
% 25.88/4.07 % (2374076)Instruction limit reached!
% 25.88/4.07 % (2374076)------------------------------
% 25.88/4.07 % (2374076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374076)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374076)Termination reason: Instruction limit
% 25.88/4.07 % (2374076)Termination phase: Saturation
% 25.88/4.07 % (2374076)Time elapsed: 0.184 s
% 25.88/4.07 % (2374076)Peak memory usage: 17 MB
% 25.88/4.07 % (2374076)Instructions burned: 688 (million)
% 25.88/4.07 % (2374086)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1683572400:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 25.88/4.07 % (2374082)Instruction limit reached!
% 25.88/4.07 % (2374082)------------------------------
% 25.88/4.07 % (2374082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374082)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374082)Termination reason: Instruction limit
% 25.88/4.07 % (2374082)Termination phase: Saturation
% 25.88/4.07 % (2374082)Time elapsed: 0.134 s
% 25.88/4.07 % (2374082)Peak memory usage: 15 MB
% 25.88/4.07 % (2374082)Instructions burned: 477 (million)
% 25.88/4.07 % (2374087)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1759432900:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 25.88/4.07 % (2374089)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=691592891:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 25.88/4.07 % (2374084)Instruction limit reached!
% 25.88/4.07 % (2374084)------------------------------
% 25.88/4.07 % (2374084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.88/4.07 % (2374084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.88/4.07 % (2374084)CaDiCaL version: 2.1.3
% 25.88/4.07 % (2374084)Termination reason: Instruction limit
% 25.88/4.07 % (2374084)Termination phase: Finite model building SAT solving
% 25.88/4.07 % (2374084)Time elapsed: 0.197 s
% 25.88/4.07 % (2374084)Peak memory usage: 25 MB
% 25.88/4.07 % (2374084)Instructions burned: 868 (million)
% 25.88/4.07 % TRYING [14]
% 25.88/4.07 % (2374092)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3321303986:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 51.85/7.78 % TRYING [8]
% 51.85/7.78 % (2374087)Instruction limit reached!
% 51.85/7.78 % (2374087)------------------------------
% 51.85/7.78 % (2374087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374087)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374087)Termination reason: Instruction limit
% 51.85/7.78 % (2374087)Termination phase: Finite model building constraint generation
% 51.85/7.78 % (2374087)Time elapsed: 0.191 s
% 51.85/7.78 % (2374087)Peak memory usage: 81 MB
% 51.85/7.78 % (2374087)Instructions burned: 889 (million)
% 51.85/7.78 % (2374094)fmb+10_1_sil=64000:random_seed=398779698:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 51.85/7.78 % TRYING [1]
% 51.85/7.78 % TRYING [2]
% 51.85/7.78 % TRYING [3]
% 51.85/7.78 % TRYING [4]
% 51.85/7.78 % (2374089)Instruction limit reached!
% 51.85/7.78 % (2374089)------------------------------
% 51.85/7.78 % (2374089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374089)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374089)Termination reason: Instruction limit
% 51.85/7.78 % (2374089)Termination phase: Saturation
% 51.85/7.78 % (2374089)Time elapsed: 0.215 s
% 51.85/7.78 % (2374089)Peak memory usage: 18 MB
% 51.85/7.78 % (2374089)Instructions burned: 693 (million)
% 51.85/7.78 % (2374096)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2234622363:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 51.85/7.78 % TRYING [20]
% 51.85/7.78 % TRYING [5]
% 51.85/7.78 % TRYING [6]
% 51.85/7.78 % (2374086)Instruction limit reached!
% 51.85/7.78 % (2374086)------------------------------
% 51.85/7.78 % (2374086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374086)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374086)Termination reason: Instruction limit
% 51.85/7.78 % (2374086)Termination phase: Saturation
% 51.85/7.78 % (2374086)Time elapsed: 0.329 s
% 51.85/7.78 % (2374086)Peak memory usage: 19 MB
% 51.85/7.78 % (2374086)Instructions burned: 1180 (million)
% 51.85/7.78 % (2374098)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3037958890:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 51.85/7.78 % (2374092)Instruction limit reached!
% 51.85/7.78 % (2374092)------------------------------
% 51.85/7.78 % (2374092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374092)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374092)Termination reason: Instruction limit
% 51.85/7.78 % (2374092)Termination phase: Saturation
% 51.85/7.78 % (2374092)Time elapsed: 0.252 s
% 51.85/7.78 % (2374092)Peak memory usage: 17 MB
% 51.85/7.78 % (2374092)Instructions burned: 880 (million)
% 51.85/7.78 % TRYING [8]
% 51.85/7.78 % (2374100)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2046617198:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 51.85/7.78 % TRYING [7]
% 51.85/7.78 % (2374098)Instruction limit reached!
% 51.85/7.78 % (2374098)------------------------------
% 51.85/7.78 % (2374098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374098)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374098)Termination reason: Instruction limit
% 51.85/7.78 % (2374098)Termination phase: Finite model building constraint generation
% 51.85/7.78 % (2374098)Time elapsed: 0.197 s
% 51.85/7.78 % (2374098)Peak memory usage: 66 MB
% 51.85/7.78 % (2374098)Instructions burned: 923 (million)
% 51.85/7.78 % (2374102)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1476512861:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 51.85/7.78 % TRYING [9]
% 51.85/7.78 % TRYING [8]
% 51.85/7.78 % (2374102)Instruction limit reached!
% 51.85/7.78 % (2374102)------------------------------
% 51.85/7.78 % (2374102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.85/7.78 % (2374102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.85/7.78 % (2374102)CaDiCaL version: 2.1.3
% 51.85/7.78 % (2374102)Termination reason: Instruction limit
% 51.85/7.78 % (2374102)Termination phase: Saturation
% 51.85/7.78 % (2374102)Time elapsed: 0.387 s
% 51.85/7.78 % (2374102)Peak memory usage: 26 MB
% 51.85/7.78 % (2374102)Instructions burned: 1473 (million)
% 51.85/7.78 % (2374104)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3506236179:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 147.76/21.38 % TRYING [77]
% 147.76/21.38 % TRYING [9]
% 147.76/21.38 % (2374100)Instruction limit reached!
% 147.76/21.38 % (2374100)------------------------------
% 147.76/21.38 % (2374100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374100)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374100)Termination reason: Instruction limit
% 147.76/21.38 % (2374100)Termination phase: Saturation
% 147.76/21.38 % (2374100)Time elapsed: 1.473 s
% 147.76/21.38 % (2374100)Peak memory usage: 46 MB
% 147.76/21.38 % (2374100)Instructions burned: 5134 (million)
% 147.76/21.38 % (2374106)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2192571588:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 147.76/21.38 % TRYING [16]
% 147.76/21.38 % TRYING [10]
% 147.76/21.38 % (2374096)Instruction limit reached!
% 147.76/21.38 % (2374096)------------------------------
% 147.76/21.38 % (2374096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374096)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374096)Termination reason: Instruction limit
% 147.76/21.38 % (2374096)Termination phase: Finite model building constraint generation
% 147.76/21.38 % (2374096)Time elapsed: 1.914 s
% 147.76/21.38 % (2374096)Peak memory usage: 668 MB
% 147.76/21.38 % (2374096)Instructions burned: 9518 (million)
% 147.76/21.38 % (2374108)ott-2_1_sil=16000:newcnf=on:random_seed=1065919819:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 147.76/21.38 % (2374104)Instruction limit reached!
% 147.76/21.38 % (2374104)------------------------------
% 147.76/21.38 % (2374104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374104)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374104)Termination reason: Instruction limit
% 147.76/21.38 % (2374104)Termination phase: Finite model building constraint generation
% 147.76/21.38 % (2374104)Time elapsed: 1.293 s
% 147.76/21.38 % (2374104)Peak memory usage: 515 MB
% 147.76/21.38 % (2374104)Instructions burned: 6325 (million)
% 147.76/21.38 % (2374106)Instruction limit reached!
% 147.76/21.38 % (2374106)------------------------------
% 147.76/21.38 % (2374106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374106)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374106)Termination reason: Instruction limit
% 147.76/21.38 % (2374106)Termination phase: Finite model building constraint generation
% 147.76/21.38 % (2374106)Time elapsed: 0.407 s
% 147.76/21.38 % (2374106)Peak memory usage: 135 MB
% 147.76/21.38 % (2374106)Instructions burned: 2179 (million)
% 147.76/21.38 % (2374110)ott+10_1_sil=32000:tgt=ground:random_seed=1287665555:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 147.76/21.38 % (2374112)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1276524465:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 147.76/21.38 % TRYING [1]
% 147.76/21.38 % TRYING [2]
% 147.76/21.38 % TRYING [3]
% 147.76/21.38 % TRYING [4]
% 147.76/21.38 % TRYING [5]
% 147.76/21.38 % TRYING [6]
% 147.76/21.38 % TRYING [7]
% 147.76/21.38 % (2374108)Instruction limit reached!
% 147.76/21.38 % (2374108)------------------------------
% 147.76/21.38 % (2374108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374108)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374108)Termination reason: Instruction limit
% 147.76/21.38 % (2374108)Termination phase: Saturation
% 147.76/21.38 % (2374108)Time elapsed: 0.269 s
% 147.76/21.38 % (2374108)Peak memory usage: 18 MB
% 147.76/21.38 % (2374108)Instructions burned: 870 (million)
% 147.76/21.38 % (2374114)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1125450224:i=3512:aac=none_2972 on theBenchmark for (2972ds/3512Mi)
% 147.76/21.38 % TRYING [8]
% 147.76/21.38 % TRYING [11]
% 147.76/21.38 % TRYING [9]
% 147.76/21.38 % TRYING [10]
% 147.76/21.38 % (2374114)Instruction limit reached!
% 147.76/21.38 % (2374114)------------------------------
% 147.76/21.38 % (2374114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.76/21.38 % (2374114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.76/21.38 % (2374114)CaDiCaL version: 2.1.3
% 147.76/21.38 % (2374114)Termination reason: Instruction limit
% 147.76/21.38 % (2374114)Termination phase: Saturation
% 147.76/21.38 % (2374114)Time elapsed: 0.978 s
% 197.14/28.35 % (2374114)Peak memory usage: 35 MB
% 197.14/28.35 % (2374114)Instructions burned: 3512 (million)
% 197.14/28.35 % (2374116)dis+21_1_sil=32000:sas=cadical:random_seed=2575704427:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 197.14/28.35 % (2374110)Instruction limit reached!
% 197.14/28.35 % (2374110)------------------------------
% 197.14/28.35 % (2374110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374110)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374110)Termination reason: Instruction limit
% 197.14/28.35 % (2374110)Termination phase: Saturation
% 197.14/28.35 % (2374110)Time elapsed: 1.614 s
% 197.14/28.35 % (2374110)Peak memory usage: 47 MB
% 197.14/28.35 % (2374110)Instructions burned: 5115 (million)
% 197.14/28.35 % (2374118)ott+11_1_sil=16000:gs=on:random_seed=925669257:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2958 on theBenchmark for (2958ds/2251Mi)
% 197.14/28.35 % TRYING [10]
% 197.14/28.35 % (2374116)Instruction limit reached!
% 197.14/28.35 % (2374116)------------------------------
% 197.14/28.35 % (2374116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374116)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374116)Termination reason: Instruction limit
% 197.14/28.35 % (2374116)Termination phase: Saturation
% 197.14/28.35 % (2374116)Time elapsed: 1.049 s
% 197.14/28.35 % (2374116)Peak memory usage: 36 MB
% 197.14/28.35 % (2374116)Instructions burned: 3774 (million)
% 197.14/28.35 % (2374120)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1908864042:fmbsr=1.6:i=67534_2951 on theBenchmark for (2951ds/67534Mi)
% 197.14/28.35 % TRYING [7]
% 197.14/28.35 % (2374118)Instruction limit reached!
% 197.14/28.35 % (2374118)------------------------------
% 197.14/28.35 % (2374118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374118)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374118)Termination reason: Instruction limit
% 197.14/28.35 % (2374118)Termination phase: Saturation
% 197.14/28.35 % (2374118)Time elapsed: 0.673 s
% 197.14/28.35 % (2374118)Peak memory usage: 23 MB
% 197.14/28.35 % (2374118)Instructions burned: 2251 (million)
% 197.14/28.35 % (2374122)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2648716510:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2951 on theBenchmark for (2951ds/4591Mi)
% 197.14/28.35 % TRYING [12]
% 197.14/28.35 % TRYING [8]
% 197.14/28.35 % (2374094)Instruction limit reached!
% 197.14/28.35 % (2374094)------------------------------
% 197.14/28.35 % (2374094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374094)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374094)Termination reason: Instruction limit
% 197.14/28.35 % (2374094)Termination phase: Finite model building SAT solving
% 197.14/28.35 % (2374094)Time elapsed: 5.273 s
% 197.14/28.35 % (2374094)Peak memory usage: 186 MB
% 197.14/28.35 % (2374094)Instructions burned: 22063 (million)
% 197.14/28.35 % (2374124)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=635588104:i=29340_2942 on theBenchmark for (2942ds/29340Mi)
% 197.14/28.35 % TRYING [11]
% 197.14/28.35 % (2374122)Instruction limit reached!
% 197.14/28.35 % (2374122)------------------------------
% 197.14/28.35 % (2374122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374122)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374122)Termination reason: Instruction limit
% 197.14/28.35 % (2374122)Termination phase: Saturation
% 197.14/28.35 % (2374122)Time elapsed: 1.117 s
% 197.14/28.35 % (2374122)Peak memory usage: 32 MB
% 197.14/28.35 % (2374122)Instructions burned: 4595 (million)
% 197.14/28.35 % (2374126)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=518350383:i=5211_2940 on theBenchmark for (2940ds/5211Mi)
% 197.14/28.35 % TRYING [9]
% 197.14/28.35 % (2374126)Instruction limit reached!
% 197.14/28.35 % (2374126)------------------------------
% 197.14/28.35 % (2374126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.14/28.35 % (2374126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.14/28.35 % (2374126)CaDiCaL version: 2.1.3
% 197.14/28.35 % (2374126)Termination reason: Instruction limit
% 197.14/28.35 % (2374126)Termination phase: Saturation
% 257.76/36.94 % (2374126)Time elapsed: 1.471 s
% 257.76/36.94 % (2374126)Peak memory usage: 44 MB
% 257.76/36.94 % (2374126)Instructions burned: 5213 (million)
% 257.76/36.94 % (2374128)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1842363791:i=5497:nm=2_2925 on theBenchmark for (2925ds/5497Mi)
% 257.76/36.94 % TRYING [17]
% 257.76/36.94 % TRYING [12]
% 257.76/36.94 % (2374128)Instruction limit reached!
% 257.76/36.94 % (2374128)------------------------------
% 257.76/36.94 % (2374128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374128)CaDiCaL version: 2.1.3
% 257.76/36.94 % (2374128)Termination reason: Instruction limit
% 257.76/36.94 % (2374128)Termination phase: Finite model building constraint generation
% 257.76/36.94 % (2374128)Time elapsed: 1.104 s
% 257.76/36.94 % (2374128)Peak memory usage: 390 MB
% 257.76/36.94 % (2374128)Instructions burned: 5497 (million)
% 257.76/36.94 % (2374130)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4281697197:fmbsr=2:i=46332_2914 on theBenchmark for (2914ds/46332Mi)
% 257.76/36.94 % TRYING [15]
% 257.76/36.94 % TRYING [13]
% 257.76/36.94 % TRYING [10]
% 257.76/36.94 % TRYING [13]
% 257.76/36.94 % (2374124)Instruction limit reached!
% 257.76/36.94 % (2374124)------------------------------
% 257.76/36.94 % (2374124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374124)CaDiCaL version: 2.1.3
% 257.76/36.94 % (2374124)Termination reason: Instruction limit
% 257.76/36.94 % (2374124)Termination phase: Saturation
% 257.76/36.94 % (2374124)Time elapsed: 8.068 s
% 257.76/36.94 % (2374124)Peak memory usage: 124 MB
% 257.76/36.94 % (2374124)Instructions burned: 29342 (million)
% 257.76/36.94 % (2374132)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2805853896:i=14071_2861 on theBenchmark for (2861ds/14071Mi)
% 257.76/36.94 % TRYING [12]
% 257.76/36.94 % TRYING [11]
% 257.76/36.94 % (2374062)Instruction limit reached!
% 257.76/36.94 % (2374062)------------------------------
% 257.76/36.94 % (2374062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374062)CaDiCaL version: 2.1.3
% 257.76/36.94 % (2374062)Termination reason: Instruction limit
% 257.76/36.94 % (2374062)Termination phase: Saturation
% 257.76/36.94 % (2374062)Time elapsed: 15.872 s
% 257.76/36.94 % (2374062)Peak memory usage: 178 MB
% 257.76/36.94 % (2374062)Instructions burned: 88028 (million)
% 257.76/36.94 % (2374134)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=280105872:i=22565:add=on:rawr=on_2840 on theBenchmark for (2840ds/22565Mi)
% 257.76/36.94 % TRYING [14]
% 257.76/36.94 % TRYING [13]
% 257.76/36.94 % (2374132)Instruction limit reached!
% 257.76/36.94 % (2374132)------------------------------
% 257.76/36.94 % (2374132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374132)CaDiCaL version: 2.1.3
% 257.76/36.94 % (2374132)Termination reason: Instruction limit
% 257.76/36.94 % (2374132)Termination phase: Finite model building constraint generation
% 257.76/36.94 % (2374132)Time elapsed: 5.493 s
% 257.76/36.94 % (2374132)Peak memory usage: 614 MB
% 257.76/36.94 % (2374132)Instructions burned: 14071 (million)
% 257.76/36.94 % (2374136)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2807031496:i=8173:av=off_2806 on theBenchmark for (2806ds/8173Mi)
% 257.76/36.94 % TRYING [14]
% 257.76/36.94 % TRYING [12]
% 257.76/36.94 % (2374134)Instruction limit reached!
% 257.76/36.94 % (2374134)------------------------------
% 257.76/36.94 % (2374134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374134)CaDiCaL version: 2.1.3
% 257.76/36.94 % (2374134)Termination reason: Instruction limit
% 257.76/36.94 % (2374134)Termination phase: Saturation
% 257.76/36.94 % (2374134)Time elapsed: 4.724 s
% 257.76/36.94 % (2374134)Peak memory usage: 85 MB
% 257.76/36.94 % (2374134)Instructions burned: 22569 (million)
% 257.76/36.94 % (2374138)dis+10_16:1_sil=16000:random_seed=2461893533:i=9155:fsr=off_2793 on theBenchmark for (2793ds/9155Mi)
% 257.76/36.94 % (2374112)Instruction limit reached!
% 257.76/36.94 % (2374112)------------------------------
% 257.76/36.94 % (2374112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.76/36.94 % (2374112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.76/36.94 % (2374112)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374112)Termination reason: Instruction limit
% 214.46/40.13 % (2374112)Termination phase: Finite model building constraint generation
% 214.46/40.13 % (2374112)Time elapsed: 18.496 s
% 214.46/40.13 % (2374112)Peak memory usage: 871 MB
% 214.46/40.13 % (2374112)Instructions burned: 54289 (million)
% 214.46/40.13 % (2374140)ott-3_8_sil=64000:random_seed=1337235876:i=20139:bs=on_2788 on theBenchmark for (2788ds/20139Mi)
% 214.46/40.13 % (2374136)Instruction limit reached!
% 214.46/40.13 % (2374136)------------------------------
% 214.46/40.13 % (2374136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374136)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374136)Termination reason: Instruction limit
% 214.46/40.13 % (2374136)Termination phase: Saturation
% 214.46/40.13 % (2374136)Time elapsed: 2.431 s
% 214.46/40.13 % (2374136)Peak memory usage: 59 MB
% 214.46/40.13 % (2374136)Instructions burned: 8174 (million)
% 214.46/40.13 % (2374142)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=895761639:fmbsr=2:i=32576_2781 on theBenchmark for (2781ds/32576Mi)
% 214.46/40.13 % TRYING [9]
% 214.46/40.13 % TRYING [16]
% 214.46/40.13 % TRYING [10]
% 214.46/40.13 % (2374138)Instruction limit reached!
% 214.46/40.13 % (2374138)------------------------------
% 214.46/40.13 % (2374138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374138)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374138)Termination reason: Instruction limit
% 214.46/40.13 % (2374138)Termination phase: Saturation
% 214.46/40.13 % (2374138)Time elapsed: 2.655 s
% 214.46/40.13 % (2374138)Peak memory usage: 66 MB
% 214.46/40.13 % (2374138)Instructions burned: 9156 (million)
% 214.46/40.13 % (2374145)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1079144911:i=11404_2766 on theBenchmark for (2766ds/11404Mi)
% 214.46/40.13 % TRYING [11]
% 214.46/40.13 % (2374130)Instruction limit reached!
% 214.46/40.13 % (2374130)------------------------------
% 214.46/40.13 % (2374130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374130)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374130)Termination reason: Instruction limit
% 214.46/40.13 % (2374130)Termination phase: Finite model building constraint generation
% 214.46/40.13 % (2374130)Time elapsed: 15.271 s
% 214.46/40.13 % (2374130)Peak memory usage: 1707 MB
% 214.46/40.13 % (2374130)Instructions burned: 46332 (million)
% 214.46/40.13 % (2374120)Instruction limit reached!
% 214.46/40.13 % (2374120)------------------------------
% 214.46/40.13 % (2374120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374120)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374120)Termination reason: Instruction limit
% 214.46/40.13 % (2374120)Termination phase: Finite model building SAT solving
% 214.46/40.13 % (2374120)Time elapsed: 19.141 s
% 214.46/40.13 % (2374120)Peak memory usage: 390 MB
% 214.46/40.13 % (2374120)Instructions burned: 67537 (million)
% 214.46/40.13 % (2374147)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1065599100:i=14134_2760 on theBenchmark for (2760ds/14134Mi)
% 214.46/40.13 % (2374149)dis+33_16_sil=32000:sac=on:random_seed=2662799284:i=15851:nm=0_2759 on theBenchmark for (2759ds/15851Mi)
% 214.46/40.13 % TRYING [12]
% 214.46/40.13 % (2374145)Instruction limit reached!
% 214.46/40.13 % (2374145)------------------------------
% 214.46/40.13 % (2374145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374145)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374145)Termination reason: Instruction limit
% 214.46/40.13 % (2374145)Termination phase: Saturation
% 214.46/40.13 % (2374145)Time elapsed: 3.458 s
% 214.46/40.13 % (2374145)Peak memory usage: 65 MB
% 214.46/40.13 % (2374145)Instructions burned: 11404 (million)
% 214.46/40.13 % (2374151)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4149244960:avsq=on:i=17627:add=on:amm=off_2731 on theBenchmark for (2731ds/17627Mi)
% 214.46/40.13 % TRYING [15]
% 214.46/40.13 % (2374140)Instruction limit reached!
% 214.46/40.13 % (2374140)------------------------------
% 214.46/40.13 % (2374140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374140)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374140)Termination reason: Instruction limit
% 214.46/40.13 % (2374140)Termination phase: Saturation
% 214.46/40.13 % (2374140)Time elapsed: 6.888 s
% 214.46/40.13 % (2374140)Peak memory usage: 135 MB
% 214.46/40.13 % (2374140)Instructions burned: 20140 (million)
% 214.46/40.13 % (2374153)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4229009531:s2a=on:i=53295_2719 on theBenchmark for (2719ds/53295Mi)
% 214.46/40.13 % (2374149)Instruction limit reached!
% 214.46/40.13 % (2374149)------------------------------
% 214.46/40.13 % (2374149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374149)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374149)Termination reason: Instruction limit
% 214.46/40.13 % (2374149)Termination phase: Saturation
% 214.46/40.13 % (2374149)Time elapsed: 4.593 s
% 214.46/40.13 % (2374149)Peak memory usage: 113 MB
% 214.46/40.13 % (2374149)Instructions burned: 15855 (million)
% 214.46/40.13 % (2374155)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2864298423:i=26857:ins=20_2713 on theBenchmark for (2713ds/26857Mi)
% 214.46/40.13 % TRYING [16]
% 214.46/40.13 % (2374147)Instruction limit reached!
% 214.46/40.13 % (2374147)------------------------------
% 214.46/40.13 % (2374147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374147)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374147)Termination reason: Instruction limit
% 214.46/40.13 % (2374147)Termination phase: Saturation
% 214.46/40.13 % (2374147)Time elapsed: 4.662 s
% 214.46/40.13 % (2374147)Peak memory usage: 106 MB
% 214.46/40.13 % (2374147)Instructions burned: 14135 (million)
% 214.46/40.13 % (2374157)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1770955621:i=28120:bs=on:fsr=off_2713 on theBenchmark for (2713ds/28120Mi)
% 214.46/40.13 % TRYING [13]
% 214.46/40.13 % (2374151)Instruction limit reached!
% 214.46/40.13 % (2374151)------------------------------
% 214.46/40.13 % (2374151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374151)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374151)Termination reason: Instruction limit
% 214.46/40.13 % (2374151)Termination phase: Saturation
% 214.46/40.13 % (2374151)Time elapsed: 3.923 s
% 214.46/40.13 % (2374151)Peak memory usage: 81 MB
% 214.46/40.13 % (2374151)Instructions burned: 17630 (million)
% 214.46/40.13 % (2374311)fmb+10_1_sil=256000:fmbss=7:random_seed=569005877:fmbsr=1.6:i=182295_2692 on theBenchmark for (2692ds/182295Mi)
% 214.46/40.13 % TRYING [7]
% 214.46/40.13 % (2374142)Instruction limit reached!
% 214.46/40.13 % (2374142)------------------------------
% 214.46/40.13 % (2374142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374142)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374142)Termination reason: Instruction limit
% 214.46/40.13 % (2374142)Termination phase: Finite model building constraint generation
% 214.46/40.13 % (2374142)Time elapsed: 9.141 s
% 214.46/40.13 % (2374142)Peak memory usage: 616 MB
% 214.46/40.13 % (2374142)Instructions burned: 32576 (million)
% 214.46/40.13 % (2374313)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=199198359:i=44625:gsp=on_2689 on theBenchmark for (2689ds/44625Mi)
% 214.46/40.13 % TRYING [8]
% 214.46/40.13 % TRYING [21]
% 214.46/40.13 % TRYING [9]
% 214.46/40.13 % TRYING [10]
% 214.46/40.13 % TRYING [16]
% 214.46/40.13 % (2374155)Instruction limit reached!
% 214.46/40.13 % (2374155)------------------------------
% 214.46/40.13 % (2374155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374155)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374155)Termination reason: Instruction limit
% 214.46/40.13 % (2374155)Termination phase: Finite model building constraint generation
% 214.46/40.13 % (2374155)Time elapsed: 6.489 s
% 214.46/40.13 % (2374155)Peak memory usage: 1556 MB
% 214.46/40.13 % (2374155)Instructions burned: 26858 (million)
% 214.46/40.13 % (2374315)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1612276042:i=160505_2647 on theBenchmark for (2647ds/160505Mi)
% 214.46/40.13 % TRYING [15]
% 214.46/40.13 % TRYING [11]
% 214.46/40.13 % (2374157)Instruction limit reached!
% 214.46/40.13 % (2374157)------------------------------
% 214.46/40.13 % (2374157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.13 % (2374157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.13 % (2374157)CaDiCaL version: 2.1.3
% 214.46/40.13 % (2374157)Termination reason: Instruction limit
% 214.46/40.13 % (2374157)Termination phase: Saturation
% 214.46/40.13 % (2374157)Time elapsed: 7.927 s
% 214.46/40.13 % (2374157)Peak memory usage: 106 MB
% 214.46/40.13 % (2374157)Instructions burned: 28122 (million)
% 214.46/40.13 % (2374317)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2177331446:fmbsr=1.3:i=225729_2633 on theBenchmark for (2633ds/225729Mi)
% 214.46/40.13 % TRYING [10]
% 214.46/40.13 % (2374153) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2374055-2374153"...
% 214.46/40.13 % (2374153)...printing done.
% 214.46/40.13 % (2374153)Refutation found. Thanks to Tanya!
% 214.46/40.13 % SZS status Theorem for theBenchmark
% 214.46/40.13 % SZS output start Proof for theBenchmark
% See solution above
% 214.46/40.14 % (2374153)------------------------------
% 214.46/40.14 % (2374153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.46/40.14 % (2374153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.46/40.14 % (2374153)CaDiCaL version: 2.1.3
% 214.46/40.14 % (2374153)Termination reason: Refutation
% 214.46/40.14 % (2374153)Time elapsed: 11.479 s
% 214.46/40.14 % (2374153)Peak memory usage: 343 MB
% 214.46/40.14 % (2374153)Instructions burned: 34195 (million)
% 214.46/40.14 % (2374055)Success in time 39.8 s
% 214.46/40.14 % Vampire exiting
%------------------------------------------------------------------------------