%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:20:13 PM UTC 2026
% Result : Theorem 0.19s 0.33s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 58
% Syntax : Number of formulae : 294 ( 141 unt; 32 def)
% Number of atoms : 580 ( 268 equ)
% Maximal formula atoms : 18 ( 1 avg)
% Number of connectives : 456 ( 170 ~; 206 |; 45 &)
% ( 32 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 33 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-3 aty)
% Number of variables : 52 ( 0 sgn 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_tptp_minus_1) ).
fof(f29,axiom,
! [X0] : plus(X0,n1) = succ(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_r) ).
fof(f30,axiom,
! [X0] : plus(n1,X0) = succ(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
fof(f31,axiom,
! [X0] : plus(X0,n2) = succ(succ(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_2_r) ).
fof(f33,axiom,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_3_r) ).
fof(f35,axiom,
! [X0] : plus(X0,n4) = succ(succ(succ(succ(X0)))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_4_r) ).
fof(f48,axiom,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( X0 != X1
& a_select2(X2,X1) = X3 )
=> a_select2(tptp_update2(X2,X0,X4),X1) = X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
fof(f53,conjecture,
( ( a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use )
=> ( a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_inuse_0015) ).
fof(f54,negated_conjecture,
~ ( ( a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use )
=> ( a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use
& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,axiom,
gt(n5,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4) ).
fof(f62,axiom,
gt(n4,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0) ).
fof(f63,axiom,
gt(n5,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0) ).
fof(f64,axiom,
gt(n1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0) ).
fof(f65,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
fof(f66,axiom,
gt(n3,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0) ).
fof(f67,axiom,
gt(n4,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1) ).
fof(f68,axiom,
gt(n5,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1) ).
fof(f71,axiom,
gt(n4,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2) ).
fof(f72,axiom,
gt(n5,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2) ).
fof(f75,axiom,
gt(n5,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3) ).
fof(f82,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4) ).
fof(f83,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5) ).
fof(f84,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1) ).
fof(f85,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2) ).
fof(f86,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(ennf_transformation,[],[f49]) ).
fof(f133,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(flattening,[],[f132]) ).
fof(f136,plain,
( ( use != a_select3(u_defuse,n0,n0)
| use != a_select3(u_defuse,n1,n0)
| use != a_select3(u_defuse,n2,n0)
| use != a_select2(xinit_defuse,n3)
| use != a_select2(xinit_defuse,n4)
| use != a_select2(xinit_defuse,n5)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) )
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use ),
inference(ennf_transformation,[],[f54]) ).
fof(f137,plain,
( ( use != a_select3(u_defuse,n0,n0)
| use != a_select3(u_defuse,n1,n0)
| use != a_select3(u_defuse,n2,n0)
| use != a_select2(xinit_defuse,n3)
| use != a_select2(xinit_defuse,n4)
| use != a_select2(xinit_defuse,n5)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) )
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use ),
inference(flattening,[],[f136]) ).
fof(f192,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f269,plain,
n0 = succ(tptp_minus_1),
inference(cnf_transformation,[],[f28]) ).
fof(f270,plain,
! [X0] : succ(X0) = plus(X0,n1),
inference(cnf_transformation,[],[f29]) ).
fof(f271,plain,
! [X0] : succ(X0) = plus(n1,X0),
inference(cnf_transformation,[],[f30]) ).
fof(f272,plain,
! [X0] : plus(X0,n2) = succ(succ(X0)),
inference(cnf_transformation,[],[f31]) ).
fof(f274,plain,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
inference(cnf_transformation,[],[f33]) ).
fof(f276,plain,
! [X0] : plus(X0,n4) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[],[f35]) ).
fof(f294,plain,
! [X2,X0,X1] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f48]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(cnf_transformation,[],[f133]) ).
fof(f300,plain,
use = a_select2(xinit_defuse,n5),
inference(cnf_transformation,[],[f137]) ).
fof(f301,plain,
use = a_select2(xinit_defuse,n4),
inference(cnf_transformation,[],[f137]) ).
fof(f302,plain,
use = a_select2(xinit_defuse,n3),
inference(cnf_transformation,[],[f137]) ).
fof(f303,plain,
use = a_select3(u_defuse,n2,n0),
inference(cnf_transformation,[],[f137]) ).
fof(f304,plain,
use = a_select3(u_defuse,n1,n0),
inference(cnf_transformation,[],[f137]) ).
fof(f305,plain,
use = a_select3(u_defuse,n0,n0),
inference(cnf_transformation,[],[f137]) ).
fof(f306,plain,
( use != a_select3(u_defuse,n0,n0)
| use != a_select3(u_defuse,n1,n0)
| use != a_select3(u_defuse,n2,n0)
| use != a_select2(xinit_defuse,n3)
| use != a_select2(xinit_defuse,n4)
| use != a_select2(xinit_defuse,n5)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
| use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) ),
inference(cnf_transformation,[],[f137]) ).
fof(f307,plain,
gt(n5,n4),
inference(cnf_transformation,[],[f55]) ).
fof(f314,plain,
gt(n4,n0),
inference(cnf_transformation,[],[f62]) ).
fof(f315,plain,
gt(n5,n0),
inference(cnf_transformation,[],[f63]) ).
fof(f316,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f64]) ).
fof(f317,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f65]) ).
fof(f318,plain,
gt(n3,n0),
inference(cnf_transformation,[],[f66]) ).
fof(f319,plain,
gt(n4,n1),
inference(cnf_transformation,[],[f67]) ).
fof(f320,plain,
gt(n5,n1),
inference(cnf_transformation,[],[f68]) ).
fof(f323,plain,
gt(n4,n2),
inference(cnf_transformation,[],[f71]) ).
fof(f324,plain,
gt(n5,n2),
inference(cnf_transformation,[],[f72]) ).
fof(f327,plain,
gt(n5,n3),
inference(cnf_transformation,[],[f75]) ).
fof(f334,plain,
n4 = succ(succ(succ(succ(n0)))),
inference(cnf_transformation,[],[f82]) ).
fof(f335,plain,
n5 = succ(succ(succ(succ(succ(n0))))),
inference(cnf_transformation,[],[f83]) ).
fof(f336,plain,
n1 = succ(n0),
inference(cnf_transformation,[],[f84]) ).
fof(f337,plain,
n2 = succ(succ(n0)),
inference(cnf_transformation,[],[f85]) ).
fof(f338,plain,
n3 = succ(succ(succ(n0))),
inference(cnf_transformation,[],[f86]) ).
fof(f345,plain,
n0 = plus(tptp_minus_1,n1),
inference(definition_unfolding,[],[f269,f270]) ).
fof(f346,plain,
! [X0] : plus(X0,n1) = plus(n1,X0),
inference(definition_unfolding,[],[f271,f270]) ).
fof(f347,plain,
! [X0] : plus(X0,n2) = plus(plus(X0,n1),n1),
inference(definition_unfolding,[],[f272,f270,f270]) ).
fof(f349,plain,
! [X0] : plus(X0,n3) = plus(plus(plus(X0,n1),n1),n1),
inference(definition_unfolding,[],[f274,f270,f270,f270]) ).
fof(f351,plain,
! [X0] : plus(X0,n4) = plus(plus(plus(plus(X0,n1),n1),n1),n1),
inference(definition_unfolding,[],[f276,f270,f270,f270,f270]) ).
fof(f360,plain,
n4 = plus(plus(plus(plus(n0,n1),n1),n1),n1),
inference(definition_unfolding,[],[f334,f270,f270,f270,f270]) ).
fof(f361,plain,
n5 = plus(plus(plus(plus(plus(n0,n1),n1),n1),n1),n1),
inference(definition_unfolding,[],[f335,f270,f270,f270,f270,f270]) ).
fof(f362,plain,
n1 = plus(n0,n1),
inference(definition_unfolding,[],[f336,f270]) ).
fof(f363,plain,
n2 = plus(plus(n0,n1),n1),
inference(definition_unfolding,[],[f337,f270,f270]) ).
fof(f364,plain,
n3 = plus(plus(plus(n0,n1),n1),n1),
inference(definition_unfolding,[],[f338,f270,f270,f270]) ).
fof(f367,plain,
! [X2,X0,X1,X4] :
( a_select2(X2,X1) = a_select2(tptp_update2(X2,X0,X4),X1)
| X0 = X1 ),
inference(equality_resolution,[],[f295]) ).
fof(f369,definition,
( spl31_1
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) ),
introduced(definition,[new_symbols(definition,[spl31_1])],[avatar_definition]) ).
fof(f371,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)
| spl31_1 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl31_2
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) ),
introduced(definition,[new_symbols(definition,[spl31_2])],[avatar_definition]) ).
fof(f375,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
| spl31_2 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f377,definition,
( spl31_3
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) ),
introduced(definition,[new_symbols(definition,[spl31_3])],[avatar_definition]) ).
fof(f379,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
| spl31_3 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f381,definition,
( spl31_4
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) ),
introduced(definition,[new_symbols(definition,[spl31_4])],[avatar_definition]) ).
fof(f383,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
| spl31_4 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f385,definition,
( spl31_5
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) ),
introduced(definition,[new_symbols(definition,[spl31_5])],[avatar_definition]) ).
fof(f387,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
| spl31_5 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl31_6
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) ),
introduced(definition,[new_symbols(definition,[spl31_6])],[avatar_definition]) ).
fof(f391,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
| spl31_6 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl31_7
<=> use = a_select2(xinit_defuse,n5) ),
introduced(definition,[new_symbols(definition,[spl31_7])],[avatar_definition]) ).
fof(f397,definition,
( spl31_8
<=> use = a_select2(xinit_defuse,n4) ),
introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition]) ).
fof(f401,definition,
( spl31_9
<=> use = a_select2(xinit_defuse,n3) ),
introduced(definition,[new_symbols(definition,[spl31_9])],[avatar_definition]) ).
fof(f405,definition,
( spl31_10
<=> use = a_select3(u_defuse,n2,n0) ),
introduced(definition,[new_symbols(definition,[spl31_10])],[avatar_definition]) ).
fof(f409,definition,
( spl31_11
<=> use = a_select3(u_defuse,n1,n0) ),
introduced(definition,[new_symbols(definition,[spl31_11])],[avatar_definition]) ).
fof(f413,definition,
( spl31_12
<=> use = a_select3(u_defuse,n0,n0) ),
introduced(definition,[new_symbols(definition,[spl31_12])],[avatar_definition]) ).
fof(f416,plain,
( ~ spl31_1
| ~ spl31_2
| ~ spl31_3
| ~ spl31_4
| ~ spl31_5
| ~ spl31_6
| ~ spl31_7
| ~ spl31_8
| ~ spl31_9
| ~ spl31_10
| ~ spl31_11
| ~ spl31_12 ),
inference(avatar_split_clause,[],[f306,f413,f409,f405,f401,f397,f393,f389,f385,f381,f377,f373,f369]) ).
fof(f417,plain,
spl31_7,
inference(avatar_split_clause,[],[f300,f393]) ).
fof(f418,plain,
spl31_8,
inference(avatar_split_clause,[],[f301,f397]) ).
fof(f419,plain,
spl31_9,
inference(avatar_split_clause,[],[f302,f401]) ).
fof(f420,plain,
spl31_10,
inference(avatar_split_clause,[],[f303,f405]) ).
fof(f421,plain,
spl31_11,
inference(avatar_split_clause,[],[f304,f409]) ).
fof(f422,plain,
spl31_12,
inference(avatar_split_clause,[],[f305,f413]) ).
fof(f453,plain,
n2 = plus(n1,plus(n0,n1)),
inference(forward_demodulation,[],[f363,f346]) ).
fof(f454,plain,
n2 = plus(n1,n1),
inference(forward_demodulation,[],[f453,f362]) ).
fof(f475,plain,
( use != use
| spl31_1 ),
inference(superposition,[],[f371,f294]) ).
fof(f476,plain,
( $false
| spl31_1 ),
inference(trivial_inequality_removal,[],[f475]) ).
fof(f477,plain,
spl31_1,
inference(avatar_contradiction_clause,[],[f476]) ).
fof(f703,definition,
( spl31_14
<=> n0 = n5 ),
introduced(definition,[new_symbols(definition,[spl31_14])],[avatar_definition]) ).
fof(f705,plain,
( n0 = n5
| ~ spl31_14 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f712,definition,
( spl31_16
<=> n0 = n4 ),
introduced(definition,[new_symbols(definition,[spl31_16])],[avatar_definition]) ).
fof(f714,plain,
( n0 = n4
| ~ spl31_16 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f721,definition,
( spl31_18
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl31_18])],[avatar_definition]) ).
fof(f723,plain,
( n0 = n3
| ~ spl31_18 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f730,definition,
( spl31_20
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl31_20])],[avatar_definition]) ).
fof(f732,plain,
( n0 = n2
| ~ spl31_20 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f734,plain,
! [X0] : plus(X0,n2) = plus(n1,plus(X0,n1)),
inference(forward_demodulation,[],[f347,f346]) ).
fof(f736,plain,
n3 = plus(n1,plus(plus(n0,n1),n1)),
inference(forward_demodulation,[],[f364,f346]) ).
fof(f737,plain,
n3 = plus(n1,plus(n1,plus(n0,n1))),
inference(forward_demodulation,[],[f736,f346]) ).
fof(f738,plain,
n3 = plus(n1,plus(n1,n1)),
inference(forward_demodulation,[],[f737,f362]) ).
fof(f739,plain,
n3 = plus(n1,n2),
inference(forward_demodulation,[],[f738,f454]) ).
fof(f744,plain,
plus(n1,n1) = plus(n0,n2),
inference(superposition,[],[f734,f362]) ).
fof(f750,plain,
n2 = plus(n0,n2),
inference(forward_demodulation,[],[f744,f454]) ).
fof(f788,plain,
! [X0] : plus(X0,n3) = plus(n1,plus(plus(X0,n1),n1)),
inference(forward_demodulation,[],[f349,f346]) ).
fof(f789,plain,
! [X0] : plus(X0,n3) = plus(plus(X0,n1),n2),
inference(forward_demodulation,[],[f788,f734]) ).
fof(f797,plain,
plus(n0,n2) = plus(tptp_minus_1,n3),
inference(superposition,[],[f789,f345]) ).
fof(f799,plain,
n2 = plus(tptp_minus_1,n3),
inference(forward_demodulation,[],[f797,f750]) ).
fof(f812,plain,
n4 = plus(n1,plus(plus(plus(n0,n1),n1),n1)),
inference(forward_demodulation,[],[f360,f346]) ).
fof(f813,plain,
n4 = plus(plus(plus(n0,n1),n1),n2),
inference(forward_demodulation,[],[f812,f734]) ).
fof(f814,plain,
n4 = plus(plus(n0,n1),n3),
inference(forward_demodulation,[],[f813,f789]) ).
fof(f815,plain,
n4 = plus(n1,n3),
inference(forward_demodulation,[],[f814,f362]) ).
fof(f844,definition,
( spl31_22
<=> n1 = n5 ),
introduced(definition,[new_symbols(definition,[spl31_22])],[avatar_definition]) ).
fof(f846,plain,
( n1 = n5
| ~ spl31_22 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f853,definition,
( spl31_24
<=> n1 = n4 ),
introduced(definition,[new_symbols(definition,[spl31_24])],[avatar_definition]) ).
fof(f855,plain,
( n1 = n4
| ~ spl31_24 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f862,definition,
( spl31_26
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl31_26])],[avatar_definition]) ).
fof(f864,plain,
( n1 = n3
| ~ spl31_26 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f866,plain,
! [X0] : plus(X0,n4) = plus(n1,plus(plus(plus(X0,n1),n1),n1)),
inference(forward_demodulation,[],[f351,f346]) ).
fof(f867,plain,
! [X0] : plus(X0,n4) = plus(plus(plus(X0,n1),n1),n2),
inference(forward_demodulation,[],[f866,f734]) ).
fof(f868,plain,
! [X0] : plus(X0,n4) = plus(plus(X0,n1),n3),
inference(forward_demodulation,[],[f867,f789]) ).
fof(f887,plain,
n5 = plus(n1,plus(plus(plus(plus(n0,n1),n1),n1),n1)),
inference(forward_demodulation,[],[f361,f346]) ).
fof(f888,plain,
n5 = plus(plus(plus(plus(n0,n1),n1),n1),n2),
inference(forward_demodulation,[],[f887,f734]) ).
fof(f889,plain,
n5 = plus(plus(plus(n0,n1),n1),n3),
inference(forward_demodulation,[],[f888,f789]) ).
fof(f890,plain,
n5 = plus(plus(n0,n1),n4),
inference(forward_demodulation,[],[f889,f868]) ).
fof(f891,plain,
n5 = plus(n1,n4),
inference(forward_demodulation,[],[f890,f362]) ).
fof(f895,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n4)
| n4 = n5
| spl31_2 ),
inference(superposition,[],[f375,f367]) ).
fof(f896,plain,
( n4 = n5
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f895,f294]) ).
fof(f897,plain,
( gt(n4,n4)
| spl31_2 ),
inference(superposition,[],[f307,f896]) ).
fof(f915,plain,
( $false
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f897,f192]) ).
fof(f916,plain,
spl31_2,
inference(avatar_contradiction_clause,[],[f915]) ).
fof(f919,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)
| n3 = n5
| spl31_3 ),
inference(superposition,[],[f379,f367]) ).
fof(f921,definition,
( spl31_27
<=> n3 = n5 ),
introduced(definition,[new_symbols(definition,[spl31_27])],[avatar_definition]) ).
fof(f923,plain,
( n3 = n5
| ~ spl31_27 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f925,definition,
( spl31_28
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3) ),
introduced(definition,[new_symbols(definition,[spl31_28])],[avatar_definition]) ).
fof(f927,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)
| spl31_28 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f928,plain,
( spl31_27
| ~ spl31_28
| spl31_3 ),
inference(avatar_split_clause,[],[f919,f377,f925,f921]) ).
fof(f975,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3)
| n3 = n4
| spl31_28 ),
inference(superposition,[],[f927,f367]) ).
fof(f976,plain,
( n3 = n4
| spl31_28 ),
inference(forward_subsumption_resolution,[],[f975,f294]) ).
fof(f1002,definition,
( spl31_30
<=> n2 = n5 ),
introduced(definition,[new_symbols(definition,[spl31_30])],[avatar_definition]) ).
fof(f1004,plain,
( n2 = n5
| ~ spl31_30 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1011,definition,
( spl31_32
<=> n2 = n4 ),
introduced(definition,[new_symbols(definition,[spl31_32])],[avatar_definition]) ).
fof(f1013,plain,
( n2 = n4
| ~ spl31_32 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1033,plain,
( n5 = plus(n1,n3)
| spl31_28 ),
inference(superposition,[],[f891,f976]) ).
fof(f1037,plain,
( n4 = n5
| spl31_28 ),
inference(forward_demodulation,[],[f1033,f815]) ).
fof(f1042,plain,
( n3 = n5
| spl31_28 ),
inference(forward_demodulation,[],[f1037,f976]) ).
fof(f1043,plain,
( spl31_27
| spl31_28 ),
inference(avatar_split_clause,[],[f1042,f925,f921]) ).
fof(f1053,plain,
( gt(n3,n3)
| ~ spl31_27 ),
inference(superposition,[],[f327,f923]) ).
fof(f1069,plain,
( $false
| ~ spl31_27 ),
inference(forward_subsumption_resolution,[],[f1053,f192]) ).
fof(f1070,plain,
~ spl31_27,
inference(avatar_contradiction_clause,[],[f1069]) ).
fof(f1075,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)
| n2 = n5
| spl31_4 ),
inference(superposition,[],[f383,f367]) ).
fof(f1077,definition,
( spl31_33
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2) ),
introduced(definition,[new_symbols(definition,[spl31_33])],[avatar_definition]) ).
fof(f1079,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)
| spl31_33 ),
inference(avatar_component_clause,[],[f1077]) ).
fof(f1080,plain,
( spl31_30
| ~ spl31_33
| spl31_4 ),
inference(avatar_split_clause,[],[f1075,f381,f1077,f1002]) ).
fof(f1088,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2)
| n2 = n4
| spl31_33 ),
inference(superposition,[],[f1079,f367]) ).
fof(f1090,definition,
( spl31_34
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2) ),
introduced(definition,[new_symbols(definition,[spl31_34])],[avatar_definition]) ).
fof(f1092,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2)
| spl31_34 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1093,plain,
( spl31_32
| ~ spl31_34
| spl31_33 ),
inference(avatar_split_clause,[],[f1088,f1077,f1090,f1011]) ).
fof(f1098,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2)
| n2 = n3
| spl31_34 ),
inference(superposition,[],[f1092,f367]) ).
fof(f1099,plain,
( n2 = n3
| spl31_34 ),
inference(forward_subsumption_resolution,[],[f1098,f294]) ).
fof(f1130,plain,
( n4 = plus(n1,n2)
| spl31_34 ),
inference(superposition,[],[f815,f1099]) ).
fof(f1143,plain,
( n3 = n4
| spl31_34 ),
inference(forward_demodulation,[],[f1130,f739]) ).
fof(f1152,plain,
( n2 = n4
| spl31_34 ),
inference(forward_demodulation,[],[f1143,f1099]) ).
fof(f1153,plain,
( spl31_32
| spl31_34 ),
inference(avatar_split_clause,[],[f1152,f1090,f1011]) ).
fof(f1186,plain,
( gt(n2,n2)
| ~ spl31_32 ),
inference(superposition,[],[f323,f1013]) ).
fof(f1218,plain,
( $false
| ~ spl31_32 ),
inference(forward_subsumption_resolution,[],[f1186,f192]) ).
fof(f1219,plain,
~ spl31_32,
inference(avatar_contradiction_clause,[],[f1218]) ).
fof(f1253,plain,
( gt(n2,n2)
| ~ spl31_30 ),
inference(superposition,[],[f324,f1004]) ).
fof(f1280,plain,
( $false
| ~ spl31_30 ),
inference(forward_subsumption_resolution,[],[f1253,f192]) ).
fof(f1281,plain,
~ spl31_30,
inference(avatar_contradiction_clause,[],[f1280]) ).
fof(f1284,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)
| n1 = n5
| spl31_5 ),
inference(superposition,[],[f387,f367]) ).
fof(f1286,definition,
( spl31_36
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1) ),
introduced(definition,[new_symbols(definition,[spl31_36])],[avatar_definition]) ).
fof(f1288,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)
| spl31_36 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1289,plain,
( spl31_22
| ~ spl31_36
| spl31_5 ),
inference(avatar_split_clause,[],[f1284,f385,f1286,f844]) ).
fof(f1315,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1)
| n1 = n4
| spl31_36 ),
inference(superposition,[],[f1288,f367]) ).
fof(f1317,definition,
( spl31_37
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1) ),
introduced(definition,[new_symbols(definition,[spl31_37])],[avatar_definition]) ).
fof(f1319,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1)
| spl31_37 ),
inference(avatar_component_clause,[],[f1317]) ).
fof(f1320,plain,
( spl31_24
| ~ spl31_37
| spl31_36 ),
inference(avatar_split_clause,[],[f1315,f1286,f1317,f853]) ).
fof(f1352,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1)
| n1 = n3
| spl31_37 ),
inference(superposition,[],[f1319,f367]) ).
fof(f1354,definition,
( spl31_40
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1) ),
introduced(definition,[new_symbols(definition,[spl31_40])],[avatar_definition]) ).
fof(f1356,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1)
| spl31_40 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1357,plain,
( spl31_26
| ~ spl31_40
| spl31_37 ),
inference(avatar_split_clause,[],[f1352,f1317,f1354,f862]) ).
fof(f1378,plain,
( use != a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1)
| n1 = n2
| spl31_40 ),
inference(superposition,[],[f1356,f367]) ).
fof(f1379,plain,
( n1 = n2
| spl31_40 ),
inference(forward_subsumption_resolution,[],[f1378,f294]) ).
fof(f1446,plain,
( n3 = plus(n1,n1)
| spl31_40 ),
inference(superposition,[],[f739,f1379]) ).
fof(f1469,plain,
( n2 = n3
| spl31_40 ),
inference(forward_demodulation,[],[f1446,f454]) ).
fof(f1478,plain,
( n1 = n3
| spl31_40 ),
inference(forward_demodulation,[],[f1469,f1379]) ).
fof(f1481,plain,
( spl31_26
| spl31_40 ),
inference(avatar_split_clause,[],[f1478,f1354,f862]) ).
fof(f1555,plain,
( n2 = plus(tptp_minus_1,n1)
| ~ spl31_26 ),
inference(superposition,[],[f799,f864]) ).
fof(f1579,plain,
( n0 = n2
| ~ spl31_26 ),
inference(forward_demodulation,[],[f1555,f345]) ).
fof(f1590,plain,
( spl31_20
| ~ spl31_26 ),
inference(avatar_split_clause,[],[f1579,f862,f730]) ).
fof(f1648,plain,
( gt(n1,n1)
| ~ spl31_24 ),
inference(superposition,[],[f319,f855]) ).
fof(f1688,plain,
( $false
| ~ spl31_24 ),
inference(forward_subsumption_resolution,[],[f1648,f192]) ).
fof(f1689,plain,
~ spl31_24,
inference(avatar_contradiction_clause,[],[f1688]) ).
fof(f1750,plain,
( gt(n1,n1)
| ~ spl31_22 ),
inference(superposition,[],[f320,f846]) ).
fof(f1787,plain,
( $false
| ~ spl31_22 ),
inference(forward_subsumption_resolution,[],[f1750,f192]) ).
fof(f1788,plain,
~ spl31_22,
inference(avatar_contradiction_clause,[],[f1787]) ).
fof(f1791,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)
| n0 = n5
| spl31_6 ),
inference(superposition,[],[f391,f367]) ).
fof(f1793,definition,
( spl31_41
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0) ),
introduced(definition,[new_symbols(definition,[spl31_41])],[avatar_definition]) ).
fof(f1795,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)
| spl31_41 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1796,plain,
( spl31_14
| ~ spl31_41
| spl31_6 ),
inference(avatar_split_clause,[],[f1791,f389,f1793,f703]) ).
fof(f1823,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0)
| n0 = n4
| spl31_41 ),
inference(superposition,[],[f1795,f367]) ).
fof(f1825,definition,
( spl31_42
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0) ),
introduced(definition,[new_symbols(definition,[spl31_42])],[avatar_definition]) ).
fof(f1827,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0)
| spl31_42 ),
inference(avatar_component_clause,[],[f1825]) ).
fof(f1828,plain,
( spl31_16
| ~ spl31_42
| spl31_41 ),
inference(avatar_split_clause,[],[f1823,f1793,f1825,f712]) ).
fof(f1855,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0)
| n0 = n3
| spl31_42 ),
inference(superposition,[],[f1827,f367]) ).
fof(f1857,definition,
( spl31_43
<=> use = a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0) ),
introduced(definition,[new_symbols(definition,[spl31_43])],[avatar_definition]) ).
fof(f1859,plain,
( use != a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0)
| spl31_43 ),
inference(avatar_component_clause,[],[f1857]) ).
fof(f1860,plain,
( spl31_18
| ~ spl31_43
| spl31_42 ),
inference(avatar_split_clause,[],[f1855,f1825,f1857,f721]) ).
fof(f1886,plain,
( use != a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0)
| n0 = n2
| spl31_43 ),
inference(superposition,[],[f1859,f367]) ).
fof(f1888,definition,
( spl31_44
<=> use = a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0) ),
introduced(definition,[new_symbols(definition,[spl31_44])],[avatar_definition]) ).
fof(f1890,plain,
( use != a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0)
| spl31_44 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1891,plain,
( spl31_20
| ~ spl31_44
| spl31_43 ),
inference(avatar_split_clause,[],[f1886,f1857,f1888,f730]) ).
fof(f1917,plain,
( use != a_select2(tptp_update2(sigma_defuse,n0,use),n0)
| n0 = n1
| spl31_44 ),
inference(superposition,[],[f1890,f367]) ).
fof(f1918,plain,
( n0 = n1
| spl31_44 ),
inference(forward_subsumption_resolution,[],[f1917,f294]) ).
fof(f1945,plain,
( gt(n0,n0)
| spl31_44 ),
inference(superposition,[],[f316,f1918]) ).
fof(f2020,plain,
( $false
| spl31_44 ),
inference(forward_subsumption_resolution,[],[f1945,f192]) ).
fof(f2021,plain,
spl31_44,
inference(avatar_contradiction_clause,[],[f2020]) ).
fof(f2076,plain,
( gt(n0,n0)
| ~ spl31_20 ),
inference(superposition,[],[f317,f732]) ).
fof(f2125,plain,
( $false
| ~ spl31_20 ),
inference(forward_subsumption_resolution,[],[f2076,f192]) ).
fof(f2126,plain,
~ spl31_20,
inference(avatar_contradiction_clause,[],[f2125]) ).
fof(f2184,plain,
( gt(n0,n0)
| ~ spl31_18 ),
inference(superposition,[],[f318,f723]) ).
fof(f2233,plain,
( $false
| ~ spl31_18 ),
inference(forward_subsumption_resolution,[],[f2184,f192]) ).
fof(f2234,plain,
~ spl31_18,
inference(avatar_contradiction_clause,[],[f2233]) ).
fof(f2293,plain,
( gt(n0,n0)
| ~ spl31_16 ),
inference(superposition,[],[f314,f714]) ).
fof(f2338,plain,
( $false
| ~ spl31_16 ),
inference(forward_subsumption_resolution,[],[f2293,f192]) ).
fof(f2339,plain,
~ spl31_16,
inference(avatar_contradiction_clause,[],[f2338]) ).
fof(f2398,plain,
( gt(n0,n0)
| ~ spl31_14 ),
inference(superposition,[],[f315,f705]) ).
fof(f2441,plain,
( $false
| ~ spl31_14 ),
inference(forward_subsumption_resolution,[],[f2398,f192]) ).
fof(f2442,plain,
~ spl31_14,
inference(avatar_contradiction_clause,[],[f2441]) ).
cnf(s1,plain,
( ~ spl31_1
| ~ spl31_2
| ~ spl31_3
| ~ spl31_4
| ~ spl31_5
| ~ spl31_6
| ~ spl31_7
| ~ spl31_8
| ~ spl31_9
| ~ spl31_10
| ~ spl31_11
| ~ spl31_12 ),
inference(sat_conversion,[],[f416]) ).
cnf(s2,plain,
spl31_7,
inference(sat_conversion,[],[f417]) ).
cnf(s3,plain,
spl31_8,
inference(sat_conversion,[],[f418]) ).
cnf(s4,plain,
spl31_9,
inference(sat_conversion,[],[f419]) ).
cnf(s5,plain,
spl31_10,
inference(sat_conversion,[],[f420]) ).
cnf(s6,plain,
spl31_11,
inference(sat_conversion,[],[f421]) ).
cnf(s7,plain,
spl31_12,
inference(sat_conversion,[],[f422]) ).
cnf(s8,plain,
spl31_1,
inference(sat_conversion,[],[f477]) ).
cnf(s17,plain,
spl31_2,
inference(sat_conversion,[],[f916]) ).
cnf(s18,plain,
( spl31_3
| spl31_27
| ~ spl31_28 ),
inference(sat_conversion,[],[f928]) ).
cnf(s24,plain,
( spl31_27
| spl31_28 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s27,plain,
~ spl31_27,
inference(sat_conversion,[],[f1070]) ).
cnf(s30,plain,
( spl31_4
| spl31_30
| ~ spl31_33 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s31,plain,
( spl31_32
| spl31_33
| ~ spl31_34 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s36,plain,
( spl31_32
| spl31_34 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s42,plain,
~ spl31_32,
inference(sat_conversion,[],[f1219]) ).
cnf(s49,plain,
~ spl31_30,
inference(sat_conversion,[],[f1281]) ).
cnf(s50,plain,
( spl31_5
| spl31_22
| ~ spl31_36 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s51,plain,
( spl31_24
| spl31_36
| ~ spl31_37 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s53,plain,
( spl31_26
| spl31_37
| ~ spl31_40 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s57,plain,
( spl31_26
| spl31_40 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s64,plain,
( spl31_20
| ~ spl31_26 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s72,plain,
~ spl31_24,
inference(sat_conversion,[],[f1689]) ).
cnf(s83,plain,
~ spl31_22,
inference(sat_conversion,[],[f1788]) ).
cnf(s84,plain,
( spl31_6
| spl31_14
| ~ spl31_41 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s85,plain,
( spl31_16
| spl31_41
| ~ spl31_42 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s86,plain,
( spl31_18
| spl31_42
| ~ spl31_43 ),
inference(sat_conversion,[],[f1860]) ).
cnf(s87,plain,
( spl31_20
| spl31_43
| ~ spl31_44 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s90,plain,
spl31_44,
inference(sat_conversion,[],[f2021]) ).
cnf(s95,plain,
~ spl31_20,
inference(sat_conversion,[],[f2126]) ).
cnf(s103,plain,
~ spl31_18,
inference(sat_conversion,[],[f2234]) ).
cnf(s113,plain,
~ spl31_16,
inference(sat_conversion,[],[f2339]) ).
cnf(s126,plain,
~ spl31_14,
inference(sat_conversion,[],[f2442]) ).
cnf(s127,plain,
spl31_43,
inference(rat,[],[s87,s90,s95]) ).
cnf(s128,plain,
spl31_42,
inference(rat,[],[s86,s127,s103]) ).
cnf(s129,plain,
spl31_41,
inference(rat,[],[s85,s128,s113]) ).
cnf(s130,plain,
spl31_6,
inference(rat,[],[s84,s129,s126]) ).
cnf(s131,plain,
~ spl31_26,
inference(rat,[],[s64,s95]) ).
cnf(s132,plain,
spl31_40,
inference(rat,[],[s57,s131]) ).
cnf(s133,plain,
spl31_37,
inference(rat,[],[s53,s132,s131]) ).
cnf(s135,plain,
spl31_36,
inference(rat,[],[s51,s133,s72]) ).
cnf(s136,plain,
spl31_5,
inference(rat,[],[s50,s135,s83]) ).
cnf(s138,plain,
spl31_34,
inference(rat,[],[s36,s42]) ).
cnf(s139,plain,
spl31_33,
inference(rat,[],[s31,s138,s42]) ).
cnf(s140,plain,
spl31_4,
inference(rat,[],[s30,s139,s49]) ).
cnf(s142,plain,
spl31_28,
inference(rat,[],[s24,s27]) ).
cnf(s145,plain,
spl31_3,
inference(rat,[],[s18,s142,s27]) ).
cnf(s153,plain,
$false,
inference(rat,[],[s1,s7,s6,s5,s4,s3,s2,s130,s136,s140,s145,s17,s8]) ).
fof(f2443,plain,
$false,
inference(avatar_sat_refutation,[],[s153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 09:55:09 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.33 % (2142980)Will run a generic schedule for satisfiability detection.
% 0.19/0.33 % (2142989)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1561887985:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.33 % (2142986)% WARNING: option uhcvi not known.
% 0.19/0.33 % (2142985)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3689600869_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.33 % (2142986)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1988011159:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.33 % (2142987)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1092924282:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.33 % (2142988)dis+10_1_sil=32000:sp=arity:random_seed=1973479254:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.33 % (2142991)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2977588293:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.33 % (2142990)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2347613164:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.33 % (2142989)Instruction limit reached!
% 0.19/0.33 % (2142989)------------------------------
% 0.19/0.33 % (2142989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.33 % (2142989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.33 % (2142989)CaDiCaL version: 2.1.3
% 0.19/0.33 % (2142989)Termination reason: Instruction limit
% 0.19/0.33 % (2142989)Termination phase: Saturation
% 0.19/0.33 % (2142989)Time elapsed: 0.034 s
% 0.19/0.33 % (2142989)Peak memory usage: 13 MB
% 0.19/0.33 % (2142989)Instructions burned: 116 (million)
% 0.19/0.33 % (2142999)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3814131831:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.33 % TRYING [1]
% 0.19/0.33 % TRYING [2]
% 0.19/0.33 % TRYING [1]
% 0.19/0.33 % TRYING [2]
% 0.19/0.33 % TRYING [3]
% 0.19/0.33 % (2142988) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2142980-2142988"...
% 0.19/0.33 % (2142986) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2142980-2142986"...
% 0.19/0.33 % TRYING [3]
% 0.19/0.33 % (2142986)...printing done.
% 0.19/0.33 % (2142988)...printing done.
% 0.19/0.33 % (2142988)Refutation found. Thanks to Tanya!
% 0.19/0.33 % SZS status Theorem for theBenchmark
% 0.19/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.34 % (2142988)------------------------------
% 0.19/0.34 % (2142988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (2142988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (2142988)CaDiCaL version: 2.1.3
% 0.19/0.34 % (2142988)Termination reason: Refutation
% 0.19/0.34 % (2142988)Time elapsed: 0.060 s
% 0.19/0.34 % (2142988)Peak memory usage: 13 MB
% 0.19/0.34 % (2142988)Instructions burned: 108 (million)
% 0.19/0.34 % (2142980)Success in time 0.099 s
% 0.19/0.34 % Vampire exiting
%------------------------------------------------------------------------------