%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO038-1.003.004 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 02:24:47 PM UTC 2026
% Result : Unsatisfiable 6.73s 1.76s
% Output : Refutation 8.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 101
% Number of leaves : 52
% Syntax : Number of formulae : 641 ( 93 unt; 46 def)
% Number of atoms : 1200 ( 40 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 1112 ( 553 ~; 517 |; 0 &)
% ( 42 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 17 ( 4 avg)
% Number of predicates : 45 ( 43 usr; 43 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 66 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : f(X0,one) = s(one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
! [X0] : f(one,s(X0)) = s(s(f(one,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
! [X0,X1] : f(s(X0),s(X1)) = f(X0,f(s(X0),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
d(one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
! [X0] :
( d(s(X0))
| ~ d(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,negated_conjecture,
~ d(f(s(s(one)),s(s(s(one))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
fof(f7,definition,
sF0 = s(one),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f8,plain,
s(one) = sF0,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF1 = s(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f10,plain,
s(sF0) = sF1,
inference(reorient_equations,[],[f9]) ).
fof(f11,definition,
sF2 = s(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f12,plain,
s(sF1) = sF2,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF3 = f(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f14,plain,
f(sF1,sF2) = sF3,
inference(reorient_equations,[],[f13]) ).
fof(f15,plain,
~ d(sF3),
inference(definition_folding,[],[f6,f14,f12,f10,f8,f10,f8]) ).
fof(f17,plain,
! [X0] : f(sF1,s(X0)) = f(sF0,f(sF1,X0)),
inference(superposition,[],[f3,f10]) ).
fof(f18,plain,
! [X0] : f(sF0,s(X0)) = f(one,f(sF0,X0)),
inference(superposition,[],[f3,f8]) ).
fof(f20,plain,
( d(sF2)
| ~ d(sF1) ),
inference(superposition,[],[f5,f12]) ).
fof(f21,plain,
( d(sF1)
| ~ d(sF0) ),
inference(superposition,[],[f5,f10]) ).
fof(f22,plain,
( d(sF0)
| ~ d(one) ),
inference(superposition,[],[f5,f8]) ).
fof(f23,plain,
d(sF0),
inference(forward_subsumption_resolution,[],[f22,f4]) ).
fof(f25,definition,
( spl4_1
<=> d(sF0) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f29,definition,
( spl4_2
<=> d(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f32,plain,
( ~ spl4_1
| spl4_2 ),
inference(avatar_split_clause,[],[f21,f29,f25]) ).
fof(f34,definition,
( spl4_3
<=> d(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f36,plain,
( d(sF2)
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f37,plain,
( ~ spl4_2
| spl4_3 ),
inference(avatar_split_clause,[],[f20,f34,f29]) ).
fof(f38,plain,
spl4_1,
inference(avatar_split_clause,[],[f23,f25]) ).
fof(f39,plain,
! [X0] : f(one,s(f(s(one),X0))) = s(s(f(s(one),s(X0)))),
inference(superposition,[],[f2,f3]) ).
fof(f40,plain,
! [X0] :
( ~ d(s(f(one,X0)))
| d(f(one,s(X0))) ),
inference(superposition,[],[f5,f2]) ).
fof(f42,plain,
! [X0] : f(one,s(f(sF0,X0))) = s(s(f(sF0,s(X0)))),
inference(forward_demodulation,[],[f39,f8]) ).
fof(f43,plain,
s(s(s(one))) = f(one,s(one)),
inference(superposition,[],[f2,f1]) ).
fof(f44,plain,
! [X0] : f(s(X0),s(one)) = f(X0,s(one)),
inference(superposition,[],[f3,f1]) ).
fof(f45,plain,
! [X0] : f(s(X0),sF0) = f(X0,sF0),
inference(forward_demodulation,[],[f44,f8]) ).
fof(f46,plain,
s(s(sF0)) = f(one,sF0),
inference(forward_demodulation,[],[f43,f8]) ).
fof(f47,plain,
s(sF1) = f(one,sF0),
inference(forward_demodulation,[],[f46,f10]) ).
fof(f48,plain,
sF2 = f(one,sF0),
inference(forward_demodulation,[],[f47,f12]) ).
fof(f49,plain,
f(one,s(sF0)) = s(s(sF2)),
inference(superposition,[],[f2,f48]) ).
fof(f50,plain,
s(s(sF2)) = f(one,sF1),
inference(forward_demodulation,[],[f49,f10]) ).
fof(f51,plain,
f(one,sF0) = f(sF0,sF0),
inference(superposition,[],[f45,f8]) ).
fof(f53,plain,
f(sF0,sF0) = f(sF1,sF0),
inference(superposition,[],[f45,f10]) ).
fof(f55,plain,
! [X0] : f(s(X0),s(sF0)) = f(X0,f(X0,sF0)),
inference(superposition,[],[f3,f45]) ).
fof(f56,plain,
! [X0] : f(X0,f(X0,sF0)) = f(s(X0),sF1),
inference(forward_demodulation,[],[f55,f10]) ).
fof(f58,plain,
f(one,sF0) = f(sF1,sF0),
inference(forward_demodulation,[],[f51,f53]) ).
fof(f59,plain,
sF2 = f(sF1,sF0),
inference(forward_demodulation,[],[f58,f48]) ).
fof(f60,plain,
f(s(one),sF1) = f(one,sF2),
inference(superposition,[],[f56,f48]) ).
fof(f63,plain,
f(one,s(f(one,sF0))) = s(s(f(s(one),sF1))),
inference(superposition,[],[f2,f56]) ).
fof(f66,plain,
f(one,s(f(one,sF0))) = s(s(f(sF0,sF1))),
inference(forward_demodulation,[],[f63,f8]) ).
fof(f68,plain,
f(one,sF2) = f(sF0,sF1),
inference(forward_demodulation,[],[f60,f8]) ).
fof(f69,plain,
s(s(f(sF0,sF1))) = f(one,s(sF2)),
inference(forward_demodulation,[],[f66,f48]) ).
fof(f72,plain,
f(one,s(sF1)) = s(s(s(s(sF2)))),
inference(superposition,[],[f2,f50]) ).
fof(f73,plain,
f(one,sF2) = s(s(s(s(sF2)))),
inference(forward_demodulation,[],[f72,f12]) ).
fof(f74,plain,
f(sF0,sF1) = s(s(s(s(sF2)))),
inference(forward_demodulation,[],[f73,f68]) ).
fof(f105,definition,
( spl4_5
<=> d(f(sF0,sF1)) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f107,plain,
( d(f(sF0,sF1))
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f124,plain,
f(sF1,s(sF0)) = f(sF0,sF2),
inference(superposition,[],[f17,f59]) ).
fof(f132,plain,
f(sF0,sF2) = f(sF1,sF1),
inference(forward_demodulation,[],[f124,f10]) ).
fof(f158,plain,
s(s(f(sF0,s(sF2)))) = f(one,s(f(sF1,sF1))),
inference(superposition,[],[f42,f132]) ).
fof(f182,plain,
! [X0] :
( d(f(one,s(X0)))
| ~ d(f(one,X0)) ),
inference(resolution,[],[f40,f5]) ).
fof(f215,plain,
! [X0] :
( ~ d(f(one,s(f(one,X0))))
| d(f(one,f(one,s(X0)))) ),
inference(superposition,[],[f182,f2]) ).
fof(f217,plain,
( d(f(one,sF1))
| ~ d(f(one,sF0)) ),
inference(superposition,[],[f182,f10]) ).
fof(f218,plain,
( d(f(one,sF2))
| ~ d(f(one,sF1)) ),
inference(superposition,[],[f182,f12]) ).
fof(f221,plain,
( d(f(sF0,sF1))
| ~ d(f(one,sF1)) ),
inference(forward_demodulation,[],[f218,f68]) ).
fof(f222,plain,
( d(s(s(sF2)))
| ~ d(f(one,sF0)) ),
inference(forward_demodulation,[],[f217,f50]) ).
fof(f225,plain,
( ~ d(s(s(sF2)))
| d(f(sF0,sF1)) ),
inference(forward_demodulation,[],[f221,f50]) ).
fof(f226,plain,
( ~ d(sF2)
| d(s(s(sF2))) ),
inference(forward_demodulation,[],[f222,f48]) ).
fof(f229,definition,
( spl4_8
<=> d(s(s(sF2))) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f232,plain,
( spl4_5
| ~ spl4_8 ),
inference(avatar_split_clause,[],[f225,f229,f105]) ).
fof(f233,plain,
( d(s(s(sF2)))
| ~ spl4_3 ),
inference(forward_subsumption_resolution,[],[f226,f36]) ).
fof(f235,plain,
( spl4_8
| ~ spl4_3 ),
inference(avatar_split_clause,[],[f233,f34,f229]) ).
fof(f241,definition,
( spl4_10
<=> d(f(sF1,sF1)) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f243,plain,
( d(f(sF1,sF1))
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f245,plain,
! [X0] :
( d(f(one,f(one,s(X0))))
| ~ d(f(one,f(one,X0))) ),
inference(resolution,[],[f215,f182]) ).
fof(f305,plain,
! [X0] :
( ~ d(f(one,f(one,s(f(one,X0)))))
| d(f(one,f(one,f(one,s(X0))))) ),
inference(superposition,[],[f245,f2]) ).
fof(f306,plain,
( d(f(one,f(one,f(sF0,sF1))))
| ~ d(f(one,f(one,s(s(s(sF2)))))) ),
inference(superposition,[],[f245,f74]) ).
fof(f307,plain,
( d(f(one,f(one,sF1)))
| ~ d(f(one,f(one,sF0))) ),
inference(superposition,[],[f245,f10]) ).
fof(f308,plain,
( d(f(one,f(one,sF2)))
| ~ d(f(one,f(one,sF1))) ),
inference(superposition,[],[f245,f12]) ).
fof(f311,plain,
( d(f(one,f(sF0,sF1)))
| ~ d(f(one,f(one,sF1))) ),
inference(forward_demodulation,[],[f308,f68]) ).
fof(f312,plain,
( d(f(one,s(s(sF2))))
| ~ d(f(one,f(one,sF0))) ),
inference(forward_demodulation,[],[f307,f50]) ).
fof(f313,plain,
( d(f(one,f(sF0,s(sF1))))
| ~ d(f(one,f(one,s(s(s(sF2)))))) ),
inference(forward_demodulation,[],[f306,f18]) ).
fof(f316,plain,
( d(f(sF0,s(sF1)))
| ~ d(f(one,f(one,sF1))) ),
inference(forward_demodulation,[],[f311,f18]) ).
fof(f317,plain,
( ~ d(f(s(one),sF1))
| d(f(one,s(s(sF2)))) ),
inference(forward_demodulation,[],[f312,f56]) ).
fof(f318,plain,
( d(f(sF0,s(s(sF1))))
| ~ d(f(one,f(one,s(s(s(sF2)))))) ),
inference(forward_demodulation,[],[f313,f18]) ).
fof(f320,plain,
( d(f(sF0,sF2))
| ~ d(f(one,f(one,sF1))) ),
inference(forward_demodulation,[],[f316,f12]) ).
fof(f321,plain,
( ~ d(f(sF0,sF1))
| d(f(one,s(s(sF2)))) ),
inference(forward_demodulation,[],[f317,f8]) ).
fof(f322,plain,
( d(f(sF0,s(sF2)))
| ~ d(f(one,f(one,s(s(s(sF2)))))) ),
inference(forward_demodulation,[],[f318,f12]) ).
fof(f323,plain,
( d(f(sF1,sF1))
| ~ d(f(one,f(one,sF1))) ),
inference(forward_demodulation,[],[f320,f132]) ).
fof(f324,plain,
( d(f(one,s(s(sF2))))
| ~ spl4_5 ),
inference(forward_subsumption_resolution,[],[f321,f107]) ).
fof(f326,definition,
( spl4_13
<=> d(f(one,f(one,s(s(s(sF2)))))) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f328,plain,
( ~ d(f(one,f(one,s(s(s(sF2))))))
| spl4_13 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f330,definition,
( spl4_14
<=> d(f(sF0,s(sF2))) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f332,plain,
( d(f(sF0,s(sF2)))
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,plain,
( ~ spl4_13
| spl4_14 ),
inference(avatar_split_clause,[],[f322,f330,f326]) ).
fof(f334,plain,
( ~ d(f(one,s(s(sF2))))
| d(f(sF1,sF1)) ),
inference(forward_demodulation,[],[f323,f50]) ).
fof(f335,plain,
( d(f(sF1,sF1))
| ~ spl4_5 ),
inference(forward_subsumption_resolution,[],[f334,f324]) ).
fof(f336,plain,
( spl4_10
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f335,f105,f241]) ).
fof(f466,plain,
( ~ d(f(one,f(one,s(s(sF2)))))
| spl4_13 ),
inference(resolution,[],[f328,f245]) ).
fof(f550,plain,
! [X0] :
( d(f(one,f(one,f(one,s(X0)))))
| ~ d(f(one,f(one,f(one,X0)))) ),
inference(resolution,[],[f305,f245]) ).
fof(f587,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,s(f(one,X0))))))
| d(f(one,f(one,f(one,f(one,s(X0)))))) ),
inference(superposition,[],[f550,f2]) ).
fof(f589,plain,
( d(f(one,f(one,f(one,f(sF0,sF1)))))
| ~ d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
inference(superposition,[],[f550,f74]) ).
fof(f590,plain,
( d(f(one,f(one,f(one,sF1))))
| ~ d(f(one,f(one,f(one,sF0)))) ),
inference(superposition,[],[f550,f10]) ).
fof(f595,plain,
( d(f(one,f(one,s(s(sF2)))))
| ~ d(f(one,f(one,f(one,sF0)))) ),
inference(forward_demodulation,[],[f590,f50]) ).
fof(f596,plain,
( d(f(one,f(one,f(sF0,s(sF1)))))
| ~ d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
inference(forward_demodulation,[],[f589,f18]) ).
fof(f601,plain,
( ~ d(f(one,f(one,f(one,sF0))))
| spl4_13 ),
inference(forward_subsumption_resolution,[],[f595,f466]) ).
fof(f602,plain,
( d(f(one,f(sF0,s(s(sF1)))))
| ~ d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
inference(forward_demodulation,[],[f596,f18]) ).
fof(f607,plain,
( ~ d(f(one,f(s(one),sF1)))
| spl4_13 ),
inference(forward_demodulation,[],[f601,f56]) ).
fof(f608,plain,
( d(f(sF0,s(s(s(sF1)))))
| ~ d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
inference(forward_demodulation,[],[f602,f18]) ).
fof(f612,plain,
( ~ d(f(s(one),s(sF1)))
| spl4_13 ),
inference(forward_demodulation,[],[f607,f3]) ).
fof(f613,plain,
( d(f(sF0,s(s(sF2))))
| ~ d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
inference(forward_demodulation,[],[f608,f12]) ).
fof(f615,definition,
( spl4_17
<=> d(f(one,f(one,f(one,f(one,s(sF2)))))) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f616,plain,
( ~ d(f(one,f(one,f(one,f(one,s(sF2))))))
| spl4_17 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f625,plain,
( ~ d(f(s(one),sF2))
| spl4_13 ),
inference(forward_demodulation,[],[f612,f12]) ).
fof(f627,definition,
( spl4_19
<=> d(f(one,f(one,f(one,s(s(s(sF2))))))) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f629,plain,
( ~ d(f(one,f(one,f(one,s(s(s(sF2)))))))
| spl4_19 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f631,definition,
( spl4_20
<=> d(f(sF0,s(s(sF2)))) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f633,plain,
( d(f(sF0,s(s(sF2))))
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f634,plain,
( ~ spl4_19
| spl4_20 ),
inference(avatar_split_clause,[],[f613,f631,f627]) ).
fof(f636,plain,
( ~ d(f(sF0,sF2))
| spl4_13 ),
inference(forward_demodulation,[],[f625,f8]) ).
fof(f637,plain,
( ~ d(f(sF1,sF1))
| spl4_13 ),
inference(forward_demodulation,[],[f636,f132]) ).
fof(f638,plain,
( $false
| ~ spl4_10
| spl4_13 ),
inference(forward_subsumption_resolution,[],[f637,f243]) ).
fof(f639,plain,
( ~ spl4_10
| spl4_13 ),
inference(avatar_contradiction_clause,[],[f638]) ).
fof(f654,plain,
( ~ d(f(one,f(one,f(one,s(s(sF2))))))
| spl4_19 ),
inference(resolution,[],[f629,f550]) ).
fof(f655,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,s(X0))))))
| ~ d(f(one,f(one,f(one,f(one,X0))))) ),
inference(resolution,[],[f587,f550]) ).
fof(f692,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,s(f(one,X0)))))))
| d(f(one,f(one,f(one,f(one,f(one,s(X0))))))) ),
inference(superposition,[],[f655,f2]) ).
fof(f694,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,sF1))))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(superposition,[],[f655,f74]) ).
fof(f695,plain,
( d(f(one,f(one,f(one,f(one,sF1)))))
| ~ d(f(one,f(one,f(one,f(one,sF0))))) ),
inference(superposition,[],[f655,f10]) ).
fof(f700,plain,
( d(f(one,f(one,f(one,s(s(sF2))))))
| ~ d(f(one,f(one,f(one,f(one,sF0))))) ),
inference(forward_demodulation,[],[f695,f50]) ).
fof(f701,plain,
( d(f(one,f(one,f(one,f(sF0,s(sF1))))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f694,f18]) ).
fof(f706,plain,
( ~ d(f(one,f(one,f(one,f(one,sF0)))))
| spl4_19 ),
inference(forward_subsumption_resolution,[],[f700,f654]) ).
fof(f707,plain,
( d(f(one,f(one,f(sF0,s(s(sF1))))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f701,f18]) ).
fof(f712,plain,
( ~ d(f(one,f(one,f(s(one),sF1))))
| spl4_19 ),
inference(forward_demodulation,[],[f706,f56]) ).
fof(f713,plain,
( d(f(one,f(sF0,s(s(s(sF1))))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f707,f18]) ).
fof(f718,plain,
( ~ d(f(one,f(s(one),s(sF1))))
| spl4_19 ),
inference(forward_demodulation,[],[f712,f3]) ).
fof(f719,plain,
( d(f(sF0,s(s(s(s(sF1))))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f713,f18]) ).
fof(f721,definition,
( spl4_21
<=> d(f(one,f(one,f(one,f(one,f(one,s(sF2))))))) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f722,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,s(sF2)))))))
| spl4_21 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f731,plain,
( ~ d(f(s(one),s(s(sF1))))
| spl4_19 ),
inference(forward_demodulation,[],[f718,f3]) ).
fof(f732,plain,
( d(f(sF0,s(s(s(sF2)))))
| ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f719,f12]) ).
fof(f735,plain,
( ~ d(f(s(one),s(sF2)))
| spl4_19 ),
inference(forward_demodulation,[],[f731,f12]) ).
fof(f737,definition,
( spl4_23
<=> d(f(one,f(one,f(one,f(one,s(s(s(sF2)))))))) ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f739,plain,
( ~ d(f(one,f(one,f(one,f(one,s(s(s(sF2))))))))
| spl4_23 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f741,definition,
( spl4_24
<=> d(f(sF0,s(s(s(sF2))))) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f743,plain,
( d(f(sF0,s(s(s(sF2)))))
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f744,plain,
( ~ spl4_23
| spl4_24 ),
inference(avatar_split_clause,[],[f732,f741,f737]) ).
fof(f745,plain,
( ~ d(f(sF0,s(sF2)))
| spl4_19 ),
inference(forward_demodulation,[],[f735,f8]) ).
fof(f746,plain,
( $false
| ~ spl4_14
| spl4_19 ),
inference(forward_subsumption_resolution,[],[f745,f332]) ).
fof(f747,plain,
( ~ spl4_14
| spl4_19 ),
inference(avatar_contradiction_clause,[],[f746]) ).
fof(f763,plain,
( ~ d(f(one,f(one,f(one,f(one,s(s(sF2)))))))
| spl4_23 ),
inference(resolution,[],[f739,f655]) ).
fof(f764,plain,
( ~ d(f(one,f(one,f(one,f(one,s(sF2))))))
| spl4_23 ),
inference(resolution,[],[f763,f655]) ).
fof(f765,plain,
( ~ spl4_17
| spl4_23 ),
inference(avatar_split_clause,[],[f764,f737,f615]) ).
fof(f766,plain,
( ~ d(f(one,f(one,f(one,f(one,sF2)))))
| spl4_17 ),
inference(resolution,[],[f616,f655]) ).
fof(f767,plain,
( ~ d(f(one,f(one,f(one,f(sF0,sF1)))))
| spl4_17 ),
inference(forward_demodulation,[],[f766,f68]) ).
fof(f768,plain,
( ~ d(f(one,f(one,f(sF0,s(sF1)))))
| spl4_17 ),
inference(forward_demodulation,[],[f767,f18]) ).
fof(f769,plain,
( ~ d(f(one,f(sF0,s(s(sF1)))))
| spl4_17 ),
inference(forward_demodulation,[],[f768,f18]) ).
fof(f770,plain,
( ~ d(f(sF0,s(s(s(sF1)))))
| spl4_17 ),
inference(forward_demodulation,[],[f769,f18]) ).
fof(f771,plain,
( ~ d(f(sF0,s(s(sF2))))
| spl4_17 ),
inference(forward_demodulation,[],[f770,f12]) ).
fof(f772,plain,
( $false
| spl4_17
| ~ spl4_20 ),
inference(forward_subsumption_resolution,[],[f771,f633]) ).
fof(f773,plain,
( spl4_17
| ~ spl4_20 ),
inference(avatar_contradiction_clause,[],[f772]) ).
fof(f774,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,s(X0)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,X0)))))) ),
inference(resolution,[],[f692,f655]) ).
fof(f821,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,s(f(one,X0))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))) ),
inference(superposition,[],[f774,f2]) ).
fof(f823,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(superposition,[],[f774,f74]) ).
fof(f830,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f823,f18]) ).
fof(f835,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f830,f18]) ).
fof(f840,plain,
( d(f(one,f(one,f(sF0,s(s(s(sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f835,f18]) ).
fof(f845,plain,
( d(f(one,f(sF0,s(s(s(s(sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f840,f18]) ).
fof(f847,definition,
( spl4_25
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f848,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))
| spl4_25 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f858,plain,
( d(f(sF0,s(s(s(s(s(sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f845,f18]) ).
fof(f861,plain,
( d(f(sF0,s(s(s(s(sF2))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f858,f12]) ).
fof(f863,plain,
( d(f(sF0,f(sF0,sF1)))
| ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
inference(forward_demodulation,[],[f861,f74]) ).
fof(f865,definition,
( spl4_27
<=> d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f867,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))
| spl4_27 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f869,definition,
( spl4_28
<=> d(f(sF0,f(sF0,sF1))) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f871,plain,
( d(f(sF0,f(sF0,sF1)))
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f872,plain,
( ~ spl4_27
| spl4_28 ),
inference(avatar_split_clause,[],[f863,f869,f865]) ).
fof(f877,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))
| spl4_27 ),
inference(resolution,[],[f867,f774]) ).
fof(f878,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,s(sF2)))))))
| spl4_27 ),
inference(resolution,[],[f877,f774]) ).
fof(f879,plain,
( ~ spl4_21
| spl4_27 ),
inference(avatar_split_clause,[],[f878,f865,f721]) ).
fof(f880,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,sF2))))))
| spl4_21 ),
inference(resolution,[],[f722,f774]) ).
fof(f881,plain,
( ~ d(f(one,f(one,f(one,f(one,f(sF0,sF1))))))
| spl4_21 ),
inference(forward_demodulation,[],[f880,f68]) ).
fof(f882,plain,
( ~ d(f(one,f(one,f(one,f(sF0,s(sF1))))))
| spl4_21 ),
inference(forward_demodulation,[],[f881,f18]) ).
fof(f883,plain,
( ~ d(f(one,f(one,f(sF0,s(s(sF1))))))
| spl4_21 ),
inference(forward_demodulation,[],[f882,f18]) ).
fof(f884,plain,
( ~ d(f(one,f(sF0,s(s(s(sF1))))))
| spl4_21 ),
inference(forward_demodulation,[],[f883,f18]) ).
fof(f885,plain,
( ~ d(f(sF0,s(s(s(s(sF1))))))
| spl4_21 ),
inference(forward_demodulation,[],[f884,f18]) ).
fof(f886,plain,
( ~ d(f(sF0,s(s(s(sF2)))))
| spl4_21 ),
inference(forward_demodulation,[],[f885,f12]) ).
fof(f887,plain,
( $false
| spl4_21
| ~ spl4_24 ),
inference(forward_subsumption_resolution,[],[f886,f743]) ).
fof(f888,plain,
( spl4_21
| ~ spl4_24 ),
inference(avatar_contradiction_clause,[],[f887]) ).
fof(f889,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,X0))))))) ),
inference(resolution,[],[f821,f774]) ).
fof(f939,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))) ),
inference(superposition,[],[f889,f2]) ).
fof(f941,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(superposition,[],[f889,f74]) ).
fof(f948,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f941,f18]) ).
fof(f953,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f948,f18]) ).
fof(f958,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f953,f18]) ).
fof(f963,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f958,f18]) ).
fof(f965,definition,
( spl4_29
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f967,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))
| ~ spl4_29 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f976,plain,
( d(f(one,f(sF0,s(s(s(s(s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f963,f18]) ).
fof(f980,plain,
( d(f(sF0,s(s(s(s(s(s(sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f976,f18]) ).
fof(f983,plain,
( d(f(sF0,s(s(s(s(s(sF2)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f980,f12]) ).
fof(f986,plain,
( d(f(sF0,s(f(sF0,sF1))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
inference(forward_demodulation,[],[f983,f74]) ).
fof(f988,definition,
( spl4_31
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition]) ).
fof(f990,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))
| spl4_31 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f992,definition,
( spl4_32
<=> d(f(sF0,s(f(sF0,sF1)))) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f994,plain,
( d(f(sF0,s(f(sF0,sF1))))
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f995,plain,
( ~ spl4_31
| spl4_32 ),
inference(avatar_split_clause,[],[f986,f992,f988]) ).
fof(f1002,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))
| spl4_31 ),
inference(resolution,[],[f990,f889]) ).
fof(f1003,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))
| spl4_31 ),
inference(resolution,[],[f1002,f889]) ).
fof(f1004,plain,
( ~ spl4_25
| spl4_31 ),
inference(avatar_split_clause,[],[f1003,f988,f847]) ).
fof(f1005,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,sF2)))))))
| spl4_25 ),
inference(resolution,[],[f848,f889]) ).
fof(f1006,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1005,f68]) ).
fof(f1007,plain,
( ~ d(f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1006,f18]) ).
fof(f1008,plain,
( ~ d(f(one,f(one,f(one,f(sF0,s(s(sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1007,f18]) ).
fof(f1009,plain,
( ~ d(f(one,f(one,f(sF0,s(s(s(sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1008,f18]) ).
fof(f1010,plain,
( ~ d(f(one,f(sF0,s(s(s(s(sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1009,f18]) ).
fof(f1011,plain,
( ~ d(f(sF0,s(s(s(s(s(sF1)))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1010,f18]) ).
fof(f1012,plain,
( ~ d(f(sF0,s(s(s(s(sF2))))))
| spl4_25 ),
inference(forward_demodulation,[],[f1011,f12]) ).
fof(f1013,plain,
( ~ d(f(sF0,f(sF0,sF1)))
| spl4_25 ),
inference(forward_demodulation,[],[f1012,f74]) ).
fof(f1014,plain,
( $false
| spl4_25
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f1013,f871]) ).
fof(f1015,plain,
( spl4_25
| ~ spl4_28 ),
inference(avatar_contradiction_clause,[],[f1014]) ).
fof(f1016,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0)))))))) ),
inference(resolution,[],[f939,f889]) ).
fof(f1069,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))) ),
inference(superposition,[],[f1016,f2]) ).
fof(f1070,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1)))))))))) ),
inference(superposition,[],[f1016,f69]) ).
fof(f1071,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(superposition,[],[f1016,f74]) ).
fof(f1074,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,X0))))))))) ),
inference(superposition,[],[f1016,f42]) ).
fof(f1075,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1074,f18]) ).
fof(f1078,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1071,f18]) ).
fof(f1079,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))) ),
inference(forward_demodulation,[],[f1070,f42]) ).
fof(f1081,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1075,f18]) ).
fof(f1083,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1078,f18]) ).
fof(f1084,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))) ),
inference(forward_demodulation,[],[f1079,f12]) ).
fof(f1086,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1081,f18]) ).
fof(f1088,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1083,f18]) ).
fof(f1089,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))) ),
inference(forward_demodulation,[],[f1084,f132]) ).
fof(f1091,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(sF0,s(s(s(s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1086,f18]) ).
fof(f1093,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1088,f18]) ).
fof(f1095,definition,
( spl4_33
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f1097,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1099,definition,
( spl4_34
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f1101,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))
| spl4_34 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1102,plain,
( spl4_33
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f1089,f1099,f1095]) ).
fof(f1104,plain,
! [X0] :
( ~ d(f(one,f(one,f(sF0,s(s(s(s(s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1091,f18]) ).
fof(f1106,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1093,f18]) ).
fof(f1108,plain,
! [X0] :
( ~ d(f(one,f(sF0,s(s(s(s(s(s(X0)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))) ),
inference(forward_demodulation,[],[f1104,f18]) ).
fof(f1110,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1106,f18]) ).
fof(f1112,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(s(X0))))))))) ),
inference(forward_demodulation,[],[f1108,f18]) ).
fof(f1114,plain,
( d(f(sF0,s(s(s(s(s(s(s(sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1110,f18]) ).
fof(f1117,plain,
( d(f(sF0,s(s(s(s(s(s(sF2))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1114,f12]) ).
fof(f1120,plain,
( d(f(sF0,s(s(f(sF0,sF1)))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1117,f74]) ).
fof(f1122,plain,
( d(f(sF0,f(one,s(sF2))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1120,f69]) ).
fof(f1124,definition,
( spl4_35
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f1126,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))
| spl4_35 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1128,definition,
( spl4_36
<=> d(f(sF0,f(one,s(sF2)))) ),
introduced(definition,[new_symbols(definition,[spl4_36])],[avatar_definition]) ).
fof(f1131,plain,
( ~ spl4_35
| spl4_36 ),
inference(avatar_split_clause,[],[f1122,f1128,f1124]) ).
fof(f1144,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(f(sF0,sF1))))))))) ),
inference(superposition,[],[f1112,f74]) ).
fof(f1145,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF1))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(sF1)))))))) ),
inference(superposition,[],[f1112,f10]) ).
fof(f1146,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(sF2)))))))) ),
inference(superposition,[],[f1112,f12]) ).
fof(f1149,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(sF2)))))))) ),
inference(forward_demodulation,[],[f1146,f132]) ).
fof(f1150,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))
| ~ d(f(sF0,s(s(s(s(s(s(sF1)))))))) ),
inference(forward_demodulation,[],[f1145,f69]) ).
fof(f1151,plain,
( ~ d(f(sF0,s(s(s(s(f(one,s(sF2))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))) ),
inference(forward_demodulation,[],[f1144,f69]) ).
fof(f1164,plain,
( ~ d(f(sF0,s(s(s(s(s(s(sF2))))))))
| spl4_34 ),
inference(forward_subsumption_resolution,[],[f1149,f1101]) ).
fof(f1165,plain,
( ~ d(f(sF0,s(s(s(s(s(sF2)))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))) ),
inference(forward_demodulation,[],[f1150,f12]) ).
fof(f1166,plain,
( ~ d(f(sF0,s(s(f(one,s(s(sF2)))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))) ),
inference(forward_demodulation,[],[f1151,f2]) ).
fof(f1170,plain,
( ~ d(f(sF0,s(s(f(sF0,sF1)))))
| spl4_34 ),
inference(forward_demodulation,[],[f1164,f74]) ).
fof(f1171,plain,
( ~ d(f(sF0,s(f(sF0,sF1))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))) ),
inference(forward_demodulation,[],[f1165,f74]) ).
fof(f1172,plain,
( ~ d(f(sF0,f(one,s(s(s(sF2))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))) ),
inference(forward_demodulation,[],[f1166,f2]) ).
fof(f1175,plain,
( ~ d(f(sF0,f(one,s(sF2))))
| spl4_34 ),
inference(forward_demodulation,[],[f1170,f69]) ).
fof(f1176,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f1171,f994]) ).
fof(f1178,definition,
( spl4_39
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f1182,definition,
( spl4_40
<=> d(f(sF0,f(one,s(s(s(sF2)))))) ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f1184,plain,
( ~ d(f(sF0,f(one,s(s(s(sF2))))))
| spl4_40 ),
inference(avatar_component_clause,[],[f1182]) ).
fof(f1185,plain,
( spl4_39
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f1172,f1182,f1178]) ).
fof(f1187,plain,
( ~ spl4_36
| spl4_34 ),
inference(avatar_split_clause,[],[f1175,f1099,f1128]) ).
fof(f1188,plain,
( spl4_29
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f1176,f992,f965]) ).
fof(f1195,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))))
| spl4_35 ),
inference(resolution,[],[f1126,f1016]) ).
fof(f1196,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))
| spl4_35 ),
inference(resolution,[],[f1195,f1016]) ).
fof(f1197,plain,
( $false
| ~ spl4_29
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f1196,f967]) ).
fof(f1198,plain,
( ~ spl4_29
| spl4_35 ),
inference(avatar_contradiction_clause,[],[f1197]) ).
fof(f1199,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0))))))))) ),
inference(resolution,[],[f1069,f1016]) ).
fof(f1254,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))) ),
inference(superposition,[],[f1199,f2]) ).
fof(f1255,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1))))))))))) ),
inference(superposition,[],[f1199,f69]) ).
fof(f1256,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(superposition,[],[f1199,f74]) ).
fof(f1259,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,X0)))))))))) ),
inference(superposition,[],[f1199,f42]) ).
fof(f1260,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1259,f18]) ).
fof(f1263,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1256,f18]) ).
fof(f1264,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1255,f42]) ).
fof(f1266,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1260,f18]) ).
fof(f1268,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1263,f18]) ).
fof(f1269,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1264,f12]) ).
fof(f1271,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1266,f18]) ).
fof(f1273,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1268,f18]) ).
fof(f1274,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))) ),
inference(forward_demodulation,[],[f1269,f132]) ).
fof(f1276,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1271,f18]) ).
fof(f1278,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1273,f18]) ).
fof(f1280,definition,
( spl4_41
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition]) ).
fof(f1282,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))
| ~ spl4_41 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1284,definition,
( spl4_42
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition]) ).
fof(f1286,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))
| spl4_42 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1287,plain,
( spl4_41
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f1274,f1284,f1280]) ).
fof(f1289,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1276,f18]) ).
fof(f1291,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1278,f18]) ).
fof(f1293,plain,
! [X0] :
( ~ d(f(one,f(one,f(sF0,s(s(s(s(s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1289,f18]) ).
fof(f1295,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1291,f18]) ).
fof(f1297,plain,
! [X0] :
( ~ d(f(one,f(sF0,s(s(s(s(s(s(s(X0))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))) ),
inference(forward_demodulation,[],[f1293,f18]) ).
fof(f1299,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1295,f18]) ).
fof(f1301,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(s(s(X0)))))))))) ),
inference(forward_demodulation,[],[f1297,f18]) ).
fof(f1303,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1299,f18]) ).
fof(f1306,plain,
( d(f(sF0,s(s(s(s(s(s(s(sF2)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1303,f12]) ).
fof(f1309,plain,
( d(f(sF0,s(s(s(f(sF0,sF1))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1306,f74]) ).
fof(f1312,plain,
( d(f(sF0,s(f(one,s(sF2)))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1309,f69]) ).
fof(f1314,definition,
( spl4_43
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2)))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f1316,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))
| spl4_43 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1318,definition,
( spl4_44
<=> d(f(sF0,s(f(one,s(sF2))))) ),
introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition]) ).
fof(f1321,plain,
( ~ spl4_43
| spl4_44 ),
inference(avatar_split_clause,[],[f1312,f1318,f1314]) ).
fof(f1322,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF1,sF1))))))))))
| spl4_42 ),
inference(resolution,[],[f1286,f1016]) ).
fof(f1323,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF2)))))))))))
| spl4_42 ),
inference(forward_demodulation,[],[f1322,f158]) ).
fof(f1324,plain,
( ~ d(f(sF0,s(s(s(s(s(s(s(sF2)))))))))
| spl4_42 ),
inference(resolution,[],[f1323,f1112]) ).
fof(f1327,plain,
( ~ d(f(sF0,s(s(s(f(sF0,sF1))))))
| spl4_42 ),
inference(forward_demodulation,[],[f1324,f74]) ).
fof(f1328,plain,
( ~ d(f(sF0,s(f(one,s(sF2)))))
| spl4_42 ),
inference(forward_demodulation,[],[f1327,f69]) ).
fof(f1329,plain,
( ~ spl4_44
| spl4_42 ),
inference(avatar_split_clause,[],[f1328,f1284,f1318]) ).
fof(f1343,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(s(f(sF0,sF1)))))))))) ),
inference(superposition,[],[f1301,f74]) ).
fof(f1350,plain,
( ~ d(f(sF0,s(s(s(s(s(f(one,s(sF2)))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1343,f69]) ).
fof(f1364,plain,
( ~ d(f(sF0,s(s(s(f(one,s(s(sF2))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1350,f2]) ).
fof(f1369,plain,
( ~ d(f(sF0,s(f(one,s(s(s(sF2)))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1364,f2]) ).
fof(f1374,definition,
( spl4_47
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f1378,definition,
( spl4_48
<=> d(f(sF0,s(f(one,s(s(s(sF2))))))) ),
introduced(definition,[new_symbols(definition,[spl4_48])],[avatar_definition]) ).
fof(f1380,plain,
( ~ d(f(sF0,s(f(one,s(s(s(sF2)))))))
| spl4_48 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1381,plain,
( spl4_47
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f1369,f1378,f1374]) ).
fof(f1396,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))
| spl4_43 ),
inference(resolution,[],[f1316,f1199]) ).
fof(f1397,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))
| spl4_43 ),
inference(resolution,[],[f1396,f1199]) ).
fof(f1398,plain,
( $false
| ~ spl4_33
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f1397,f1097]) ).
fof(f1399,plain,
( ~ spl4_33
| spl4_43 ),
inference(avatar_contradiction_clause,[],[f1398]) ).
fof(f1400,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0)))))))))) ),
inference(resolution,[],[f1254,f1199]) ).
fof(f1458,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))))) ),
inference(superposition,[],[f1400,f2]) ).
fof(f1459,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1)))))))))))) ),
inference(superposition,[],[f1400,f69]) ).
fof(f1463,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,X0))))))))))) ),
inference(superposition,[],[f1400,f42]) ).
fof(f1464,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1463,f18]) ).
fof(f1468,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1)))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1459,f42]) ).
fof(f1470,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1464,f18]) ).
fof(f1473,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1468,f12]) ).
fof(f1475,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1470,f18]) ).
fof(f1478,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))) ),
inference(forward_demodulation,[],[f1473,f132]) ).
fof(f1480,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1475,f18]) ).
fof(f1484,definition,
( spl4_51
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f1486,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1488,definition,
( spl4_52
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_52])],[avatar_definition]) ).
fof(f1490,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))
| spl4_52 ),
inference(avatar_component_clause,[],[f1488]) ).
fof(f1491,plain,
( spl4_51
| ~ spl4_52 ),
inference(avatar_split_clause,[],[f1478,f1488,f1484]) ).
fof(f1493,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1480,f18]) ).
fof(f1497,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1493,f18]) ).
fof(f1501,plain,
! [X0] :
( ~ d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1497,f18]) ).
fof(f1505,plain,
! [X0] :
( ~ d(f(one,f(sF0,s(s(s(s(s(s(s(s(X0)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0))))))))))))) ),
inference(forward_demodulation,[],[f1501,f18]) ).
fof(f1509,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(X0)))))))))))))
| ~ d(f(sF0,s(s(s(s(s(s(s(s(s(X0))))))))))) ),
inference(forward_demodulation,[],[f1505,f18]) ).
fof(f1528,definition,
( spl4_54
<=> d(f(sF0,f(one,s(s(sF2))))) ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f1529,plain,
( ~ d(f(sF0,f(one,s(s(sF2)))))
| spl4_54 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1532,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF1,sF1)))))))))))
| spl4_52 ),
inference(resolution,[],[f1490,f1199]) ).
fof(f1533,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF2))))))))))))
| spl4_52 ),
inference(forward_demodulation,[],[f1532,f158]) ).
fof(f1534,plain,
( ~ d(f(sF0,s(s(s(s(s(s(s(s(sF2))))))))))
| spl4_52 ),
inference(resolution,[],[f1533,f1301]) ).
fof(f1537,plain,
( ~ d(f(sF0,s(s(s(s(f(sF0,sF1)))))))
| spl4_52 ),
inference(forward_demodulation,[],[f1534,f74]) ).
fof(f1538,plain,
( ~ d(f(sF0,s(s(f(one,s(sF2))))))
| spl4_52 ),
inference(forward_demodulation,[],[f1537,f69]) ).
fof(f1539,plain,
( ~ d(f(sF0,f(one,s(s(sF2)))))
| spl4_52 ),
inference(forward_demodulation,[],[f1538,f2]) ).
fof(f1540,plain,
( ~ spl4_54
| spl4_52 ),
inference(avatar_split_clause,[],[f1539,f1488,f1528]) ).
fof(f1613,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0))))))))))) ),
inference(resolution,[],[f1458,f1400]) ).
fof(f1617,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0)))))))))))) ),
inference(superposition,[],[f1458,f48]) ).
fof(f1627,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0))))))))))))
| ~ spl4_41 ),
inference(forward_subsumption_resolution,[],[f1617,f1282]) ).
fof(f1634,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))
| ~ spl4_41 ),
inference(forward_demodulation,[],[f1627,f10]) ).
fof(f1640,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))))))
| ~ spl4_41 ),
inference(forward_demodulation,[],[f1634,f50]) ).
fof(f1659,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0)))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))))) ),
inference(superposition,[],[f1613,f2]) ).
fof(f1660,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1))))))))))))) ),
inference(superposition,[],[f1613,f69]) ).
fof(f1663,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF2)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(superposition,[],[f1613,f12]) ).
fof(f1666,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1663,f68]) ).
fof(f1669,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))) ),
inference(forward_demodulation,[],[f1660,f42]) ).
fof(f1672,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1666,f18]) ).
fof(f1674,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2)))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))) ),
inference(forward_demodulation,[],[f1669,f12]) ).
fof(f1677,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1672,f18]) ).
fof(f1679,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))) ),
inference(forward_demodulation,[],[f1674,f132]) ).
fof(f1682,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1677,f18]) ).
fof(f1685,definition,
( spl4_59
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f1687,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))
| ~ spl4_59 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1689,definition,
( spl4_60
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1691,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))))
| spl4_60 ),
inference(avatar_component_clause,[],[f1689]) ).
fof(f1692,plain,
( spl4_59
| ~ spl4_60 ),
inference(avatar_split_clause,[],[f1679,f1689,f1685]) ).
fof(f1695,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1682,f18]) ).
fof(f1699,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1695,f18]) ).
fof(f1703,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1699,f18]) ).
fof(f1707,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1703,f18]) ).
fof(f1711,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1707,f18]) ).
fof(f1715,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1711,f18]) ).
fof(f1718,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(sF2))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1715,f12]) ).
fof(f1721,plain,
( d(f(sF0,s(s(s(s(f(sF0,sF1)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1718,f74]) ).
fof(f1724,plain,
( d(f(sF0,s(s(f(one,s(sF2))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1721,f69]) ).
fof(f1727,plain,
( d(f(sF0,f(one,s(s(sF2)))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))) ),
inference(forward_demodulation,[],[f1724,f2]) ).
fof(f1729,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1727,f1529]) ).
fof(f1735,definition,
( spl4_62
<=> d(f(sF0,s(f(one,s(s(sF2)))))) ),
introduced(definition,[new_symbols(definition,[spl4_62])],[avatar_definition]) ).
fof(f1736,plain,
( ~ d(f(sF0,s(f(one,s(s(sF2))))))
| spl4_62 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1739,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))))))
| spl4_54 ),
inference(forward_demodulation,[],[f1729,f50]) ).
fof(f1740,plain,
( $false
| ~ spl4_41
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1739,f1640]) ).
fof(f1741,plain,
( ~ spl4_41
| spl4_54 ),
inference(avatar_contradiction_clause,[],[f1740]) ).
fof(f1744,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF1,sF1))))))))))))
| spl4_60 ),
inference(resolution,[],[f1691,f1400]) ).
fof(f1745,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF2)))))))))))))
| spl4_60 ),
inference(forward_demodulation,[],[f1744,f158]) ).
fof(f1746,plain,
( ~ d(f(sF0,s(s(s(s(s(s(s(s(s(sF2)))))))))))
| spl4_60 ),
inference(resolution,[],[f1745,f1509]) ).
fof(f1749,plain,
( ~ d(f(sF0,s(s(s(s(s(f(sF0,sF1))))))))
| spl4_60 ),
inference(forward_demodulation,[],[f1746,f74]) ).
fof(f1750,plain,
( ~ d(f(sF0,s(s(s(f(one,s(sF2)))))))
| spl4_60 ),
inference(forward_demodulation,[],[f1749,f69]) ).
fof(f1751,plain,
( ~ d(f(sF0,s(f(one,s(s(sF2))))))
| spl4_60 ),
inference(forward_demodulation,[],[f1750,f2]) ).
fof(f1752,plain,
( ~ spl4_62
| spl4_60 ),
inference(avatar_split_clause,[],[f1751,f1689,f1735]) ).
fof(f1831,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0)))))))))))) ),
inference(resolution,[],[f1659,f1613]) ).
fof(f1835,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0))))))))))))) ),
inference(superposition,[],[f1659,f48]) ).
fof(f1845,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0)))))))))))))
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f1835,f1486]) ).
fof(f1852,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))
| ~ spl4_51 ),
inference(forward_demodulation,[],[f1845,f10]) ).
fof(f1858,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))))
| ~ spl4_51 ),
inference(forward_demodulation,[],[f1852,f50]) ).
fof(f1879,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))))))) ),
inference(superposition,[],[f1831,f2]) ).
fof(f1880,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1)))))))))))))) ),
inference(superposition,[],[f1831,f69]) ).
fof(f1883,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF2))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(superposition,[],[f1831,f12]) ).
fof(f1886,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1883,f68]) ).
fof(f1889,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1)))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))) ),
inference(forward_demodulation,[],[f1880,f42]) ).
fof(f1892,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1886,f18]) ).
fof(f1894,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))) ),
inference(forward_demodulation,[],[f1889,f12]) ).
fof(f1897,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1892,f18]) ).
fof(f1899,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))) ),
inference(forward_demodulation,[],[f1894,f132]) ).
fof(f1902,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1897,f18]) ).
fof(f1905,definition,
( spl4_67
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f1907,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1909,definition,
( spl4_68
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_68])],[avatar_definition]) ).
fof(f1911,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))))
| spl4_68 ),
inference(avatar_component_clause,[],[f1909]) ).
fof(f1912,plain,
( spl4_67
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1899,f1909,f1905]) ).
fof(f1915,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1902,f18]) ).
fof(f1919,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1915,f18]) ).
fof(f1923,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1919,f18]) ).
fof(f1927,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1923,f18]) ).
fof(f1931,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1927,f18]) ).
fof(f1935,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1931,f18]) ).
fof(f1939,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(sF1))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1935,f18]) ).
fof(f1942,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(sF2)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1939,f12]) ).
fof(f1945,plain,
( d(f(sF0,s(s(s(s(s(f(sF0,sF1))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1942,f74]) ).
fof(f1948,plain,
( d(f(sF0,s(s(s(f(one,s(sF2)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1945,f69]) ).
fof(f1951,plain,
( d(f(sF0,s(f(one,s(s(sF2))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))) ),
inference(forward_demodulation,[],[f1948,f2]) ).
fof(f1954,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))
| spl4_62 ),
inference(forward_subsumption_resolution,[],[f1951,f1736]) ).
fof(f1956,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))))
| spl4_62 ),
inference(forward_demodulation,[],[f1954,f50]) ).
fof(f1958,plain,
( $false
| ~ spl4_51
| spl4_62 ),
inference(forward_subsumption_resolution,[],[f1956,f1858]) ).
fof(f1959,plain,
( ~ spl4_51
| spl4_62 ),
inference(avatar_contradiction_clause,[],[f1958]) ).
fof(f1962,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF1,sF1)))))))))))))
| spl4_68 ),
inference(resolution,[],[f1911,f1613]) ).
fof(f1963,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF2))))))))))))))
| spl4_68 ),
inference(forward_demodulation,[],[f1962,f158]) ).
fof(f1965,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(sF2)))))))))))))
| spl4_68 ),
inference(resolution,[],[f1963,f1400]) ).
fof(f1966,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(sF2))))))))))))))
| spl4_68 ),
inference(forward_demodulation,[],[f1965,f42]) ).
fof(f1972,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(s(sF2)))))))))))))
| spl4_68 ),
inference(resolution,[],[f1966,f1199]) ).
fof(f1973,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(s(sF2))))))))))))))
| spl4_68 ),
inference(forward_demodulation,[],[f1972,f42]) ).
fof(f1979,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(s(s(sF2)))))))))))))
| spl4_68 ),
inference(resolution,[],[f1973,f1016]) ).
fof(f1980,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(s(s(sF2))))))))))))))
| spl4_68 ),
inference(forward_demodulation,[],[f1979,f42]) ).
fof(f1982,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1)))))))))))
| spl4_68 ),
inference(forward_demodulation,[],[f1980,f74]) ).
fof(f1984,plain,
( ~ spl4_39
| spl4_68 ),
inference(avatar_split_clause,[],[f1982,f1909,f1178]) ).
fof(f2063,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0))))))))))))) ),
inference(resolution,[],[f1879,f1831]) ).
fof(f2067,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0)))))))))))))) ),
inference(superposition,[],[f1879,f48]) ).
fof(f2077,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0))))))))))))))
| ~ spl4_59 ),
inference(forward_subsumption_resolution,[],[f2067,f1687]) ).
fof(f2084,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))
| ~ spl4_59 ),
inference(forward_demodulation,[],[f2077,f10]) ).
fof(f2090,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))))))))
| ~ spl4_59 ),
inference(forward_demodulation,[],[f2084,f50]) ).
fof(f2112,plain,
! [X0] :
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(one,X0)))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0))))))))))))))) ),
inference(superposition,[],[f2063,f2]) ).
fof(f2113,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,sF1))))))))))))))) ),
inference(superposition,[],[f2063,f69]) ).
fof(f2116,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF2)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(superposition,[],[f2063,f12]) ).
fof(f2119,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2116,f68]) ).
fof(f2122,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF1))))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))) ),
inference(forward_demodulation,[],[f2113,f42]) ).
fof(f2125,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2119,f18]) ).
fof(f2127,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,sF2)))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))) ),
inference(forward_demodulation,[],[f2122,f12]) ).
fof(f2130,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2125,f18]) ).
fof(f2132,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))) ),
inference(forward_demodulation,[],[f2127,f132]) ).
fof(f2135,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2130,f18]) ).
fof(f2138,definition,
( spl4_73
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_73])],[avatar_definition]) ).
fof(f2140,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2)))))))))))))))
| ~ spl4_73 ),
inference(avatar_component_clause,[],[f2138]) ).
fof(f2142,definition,
( spl4_74
<=> d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl4_74])],[avatar_definition]) ).
fof(f2144,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF1,sF1)))))))))))))))
| spl4_74 ),
inference(avatar_component_clause,[],[f2142]) ).
fof(f2145,plain,
( spl4_73
| ~ spl4_74 ),
inference(avatar_split_clause,[],[f2132,f2142,f2138]) ).
fof(f2148,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2135,f18]) ).
fof(f2152,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2148,f18]) ).
fof(f2156,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2152,f18]) ).
fof(f2160,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2156,f18]) ).
fof(f2164,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2160,f18]) ).
fof(f2168,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2164,f18]) ).
fof(f2172,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2168,f18]) ).
fof(f2176,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2172,f18]) ).
fof(f2179,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(sF2))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2176,f12]) ).
fof(f2182,plain,
( d(f(sF0,s(s(s(s(s(s(f(sF0,sF1)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2179,f74]) ).
fof(f2185,plain,
( d(f(sF0,s(s(s(s(f(one,s(sF2))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2182,f69]) ).
fof(f2188,plain,
( d(f(sF0,s(s(f(one,s(s(sF2)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2185,f2]) ).
fof(f2191,plain,
( d(f(sF0,f(one,s(s(s(sF2))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))) ),
inference(forward_demodulation,[],[f2188,f2]) ).
fof(f2193,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))
| spl4_40 ),
inference(forward_subsumption_resolution,[],[f2191,f1184]) ).
fof(f2195,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2))))))))))))))
| spl4_40 ),
inference(forward_demodulation,[],[f2193,f50]) ).
fof(f2196,plain,
( $false
| spl4_40
| ~ spl4_59 ),
inference(forward_subsumption_resolution,[],[f2195,f2090]) ).
fof(f2197,plain,
( spl4_40
| ~ spl4_59 ),
inference(avatar_contradiction_clause,[],[f2196]) ).
fof(f2218,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF1,sF1))))))))))))))
| spl4_74 ),
inference(resolution,[],[f2144,f1831]) ).
fof(f2219,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(sF2)))))))))))))))
| spl4_74 ),
inference(forward_demodulation,[],[f2218,f158]) ).
fof(f2221,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(sF2))))))))))))))
| spl4_74 ),
inference(resolution,[],[f2219,f1613]) ).
fof(f2222,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(sF2)))))))))))))))
| spl4_74 ),
inference(forward_demodulation,[],[f2221,f42]) ).
fof(f2228,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(s(sF2))))))))))))))
| spl4_74 ),
inference(resolution,[],[f2222,f1400]) ).
fof(f2229,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(s(sF2)))))))))))))))
| spl4_74 ),
inference(forward_demodulation,[],[f2228,f42]) ).
fof(f2235,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(f(sF0,s(s(s(sF2))))))))))))))
| spl4_74 ),
inference(resolution,[],[f2229,f1199]) ).
fof(f2236,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,s(s(s(s(sF2)))))))))))))))
| spl4_74 ),
inference(forward_demodulation,[],[f2235,f42]) ).
fof(f2238,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(f(sF0,f(sF0,sF1))))))))))))
| spl4_74 ),
inference(forward_demodulation,[],[f2236,f74]) ).
fof(f2240,plain,
( ~ spl4_47
| spl4_74 ),
inference(avatar_split_clause,[],[f2238,f2142,f1374]) ).
fof(f2338,plain,
! [X0] :
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(X0)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,X0)))))))))))))) ),
inference(resolution,[],[f2112,f2063]) ).
fof(f2342,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))
| d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0))))))))))))))) ),
inference(superposition,[],[f2112,f48]) ).
fof(f2352,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF0)))))))))))))))
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f2342,f1907]) ).
fof(f2359,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))))
| ~ spl4_67 ),
inference(forward_demodulation,[],[f2352,f10]) ).
fof(f2365,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))))))
| ~ spl4_67 ),
inference(forward_demodulation,[],[f2359,f50]) ).
fof(f2391,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(superposition,[],[f2338,f74]) ).
fof(f2393,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF2))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(superposition,[],[f2338,f12]) ).
fof(f2396,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2393,f68]) ).
fof(f2398,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2391,f18]) ).
fof(f2402,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2396,f18]) ).
fof(f2403,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2398,f18]) ).
fof(f2407,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2402,f18]) ).
fof(f2408,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2403,f18]) ).
fof(f2412,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2407,f18]) ).
fof(f2413,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2408,f18]) ).
fof(f2425,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2412,f18]) ).
fof(f2426,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2413,f18]) ).
fof(f2429,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2425,f18]) ).
fof(f2430,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2426,f18]) ).
fof(f2433,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2429,f18]) ).
fof(f2434,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2430,f18]) ).
fof(f2437,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2433,f18]) ).
fof(f2438,plain,
( d(f(one,f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2434,f18]) ).
fof(f2441,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2437,f18]) ).
fof(f2442,plain,
( d(f(one,f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2438,f18]) ).
fof(f2445,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2441,f18]) ).
fof(f2446,plain,
( d(f(one,f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2442,f18]) ).
fof(f2449,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2445,f18]) ).
fof(f2450,plain,
( d(f(one,f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2446,f18]) ).
fof(f2453,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2449,f18]) ).
fof(f2454,plain,
( d(f(one,f(sF0,s(s(s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2450,f18]) ).
fof(f2457,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(s(s(sF1))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2453,f18]) ).
fof(f2458,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(s(s(s(sF1)))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2454,f18]) ).
fof(f2460,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(s(sF2)))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2457,f12]) ).
fof(f2461,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(s(s(s(s(sF2))))))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2458,f12]) ).
fof(f2463,plain,
( d(f(sF0,s(s(s(s(s(s(s(f(sF0,sF1))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2460,f74]) ).
fof(f2464,plain,
( d(f(sF0,s(s(s(s(s(s(s(s(f(sF0,sF1)))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2461,f74]) ).
fof(f2466,plain,
( d(f(sF0,s(s(s(s(s(f(one,s(sF2)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2463,f69]) ).
fof(f2467,plain,
( d(f(sF0,s(s(s(s(s(s(f(one,s(sF2))))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2464,f69]) ).
fof(f2469,plain,
( d(f(sF0,s(s(s(f(one,s(s(sF2))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2466,f2]) ).
fof(f2470,plain,
( d(f(sF0,s(s(s(s(f(one,s(s(sF2)))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2467,f2]) ).
fof(f2472,plain,
( d(f(sF0,s(f(one,s(s(s(sF2)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1)))))))))))))) ),
inference(forward_demodulation,[],[f2469,f2]) ).
fof(f2473,plain,
( d(f(sF0,s(s(f(one,s(s(s(sF2))))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2470,f2]) ).
fof(f2475,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,sF1))))))))))))))
| spl4_48 ),
inference(forward_subsumption_resolution,[],[f2472,f1380]) ).
fof(f2476,plain,
( d(f(sF0,f(one,s(s(s(s(sF2)))))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2473,f2]) ).
fof(f2477,plain,
( ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))))))
| spl4_48 ),
inference(forward_demodulation,[],[f2475,f50]) ).
fof(f2478,plain,
( d(f(sF0,f(one,f(sF0,sF1))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2476,f74]) ).
fof(f2479,plain,
( $false
| spl4_48
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f2477,f2365]) ).
fof(f2480,plain,
( spl4_48
| ~ spl4_67 ),
inference(avatar_contradiction_clause,[],[f2479]) ).
fof(f2481,plain,
( d(f(sF0,f(sF0,s(sF1))))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2478,f18]) ).
fof(f2482,plain,
( d(f(sF0,f(sF0,sF2)))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2481,f12]) ).
fof(f2483,plain,
( d(f(sF0,f(sF1,sF1)))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2482,f132]) ).
fof(f2484,plain,
( d(f(sF1,s(sF1)))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2483,f17]) ).
fof(f2485,plain,
( d(f(sF1,sF2))
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2484,f12]) ).
fof(f2486,plain,
( d(sF3)
| ~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))) ),
inference(forward_demodulation,[],[f2485,f14]) ).
fof(f2487,plain,
~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(s(sF2))))))))))))))))),
inference(forward_subsumption_resolution,[],[f2486,f15]) ).
fof(f2509,plain,
~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(s(sF2)))))))))))))))),
inference(resolution,[],[f2487,f2338]) ).
fof(f2510,plain,
~ d(f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,f(one,s(sF2))))))))))))))),
inference(resolution,[],[f2509,f2338]) ).
fof(f2511,plain,
( $false
| ~ spl4_73 ),
inference(forward_subsumption_resolution,[],[f2510,f2140]) ).
fof(f2512,plain,
~ spl4_73,
inference(avatar_contradiction_clause,[],[f2511]) ).
cnf(s1,plain,
( ~ spl4_1
| spl4_2 ),
inference(sat_conversion,[],[f32]) ).
cnf(s2,plain,
( ~ spl4_2
| spl4_3 ),
inference(sat_conversion,[],[f37]) ).
cnf(s3,plain,
spl4_1,
inference(sat_conversion,[],[f38]) ).
cnf(s7,plain,
( spl4_5
| ~ spl4_8 ),
inference(sat_conversion,[],[f232]) ).
cnf(s8,plain,
( ~ spl4_3
| spl4_8 ),
inference(sat_conversion,[],[f235]) ).
cnf(s12,plain,
( ~ spl4_13
| spl4_14 ),
inference(sat_conversion,[],[f333]) ).
cnf(s13,plain,
( ~ spl4_5
| spl4_10 ),
inference(sat_conversion,[],[f336]) ).
cnf(s18,plain,
( ~ spl4_19
| spl4_20 ),
inference(sat_conversion,[],[f634]) ).
cnf(s19,plain,
( ~ spl4_10
| spl4_13 ),
inference(sat_conversion,[],[f639]) ).
cnf(s21,plain,
( ~ spl4_23
| spl4_24 ),
inference(sat_conversion,[],[f744]) ).
cnf(s22,plain,
( ~ spl4_14
| spl4_19 ),
inference(sat_conversion,[],[f747]) ).
cnf(s23,plain,
( ~ spl4_17
| spl4_23 ),
inference(sat_conversion,[],[f765]) ).
cnf(s24,plain,
( spl4_17
| ~ spl4_20 ),
inference(sat_conversion,[],[f773]) ).
cnf(s26,plain,
( ~ spl4_27
| spl4_28 ),
inference(sat_conversion,[],[f872]) ).
cnf(s27,plain,
( ~ spl4_21
| spl4_27 ),
inference(sat_conversion,[],[f879]) ).
cnf(s28,plain,
( spl4_21
| ~ spl4_24 ),
inference(sat_conversion,[],[f888]) ).
cnf(s30,plain,
( ~ spl4_31
| spl4_32 ),
inference(sat_conversion,[],[f995]) ).
cnf(s31,plain,
( ~ spl4_25
| spl4_31 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s32,plain,
( spl4_25
| ~ spl4_28 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s33,plain,
( spl4_33
| ~ spl4_34 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s34,plain,
( ~ spl4_35
| spl4_36 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s36,plain,
( spl4_39
| ~ spl4_40 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s37,plain,
( spl4_34
| ~ spl4_36 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s38,plain,
( spl4_29
| ~ spl4_32 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s39,plain,
( ~ spl4_29
| spl4_35 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s40,plain,
( spl4_41
| ~ spl4_42 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s41,plain,
( ~ spl4_43
| spl4_44 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s42,plain,
( spl4_42
| ~ spl4_44 ),
inference(sat_conversion,[],[f1329]) ).
cnf(s44,plain,
( spl4_47
| ~ spl4_48 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s46,plain,
( ~ spl4_33
| spl4_43 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s47,plain,
( spl4_51
| ~ spl4_52 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s49,plain,
( spl4_52
| ~ spl4_54 ),
inference(sat_conversion,[],[f1540]) ).
cnf(s52,plain,
( spl4_59
| ~ spl4_60 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s54,plain,
( ~ spl4_41
| spl4_54 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s55,plain,
( spl4_60
| ~ spl4_62 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s58,plain,
( spl4_67
| ~ spl4_68 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s59,plain,
( ~ spl4_51
| spl4_62 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s60,plain,
( ~ spl4_39
| spl4_68 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s64,plain,
( spl4_73
| ~ spl4_74 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s65,plain,
( spl4_40
| ~ spl4_59 ),
inference(sat_conversion,[],[f2197]) ).
cnf(s66,plain,
( ~ spl4_47
| spl4_74 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s71,plain,
( spl4_48
| ~ spl4_67 ),
inference(sat_conversion,[],[f2480]) ).
cnf(s72,plain,
~ spl4_73,
inference(sat_conversion,[],[f2512]) ).
cnf(s73,plain,
~ spl4_74,
inference(rat,[],[s64,s72]) ).
cnf(s74,plain,
~ spl4_47,
inference(rat,[],[s66,s73]) ).
cnf(s75,plain,
~ spl4_48,
inference(rat,[],[s44,s74]) ).
cnf(s76,plain,
~ spl4_67,
inference(rat,[],[s71,s75]) ).
cnf(s77,plain,
~ spl4_68,
inference(rat,[],[s58,s76]) ).
cnf(s78,plain,
~ spl4_39,
inference(rat,[],[s60,s77]) ).
cnf(s79,plain,
~ spl4_40,
inference(rat,[],[s36,s78]) ).
cnf(s80,plain,
~ spl4_59,
inference(rat,[],[s65,s79]) ).
cnf(s81,plain,
~ spl4_60,
inference(rat,[],[s52,s80]) ).
cnf(s82,plain,
~ spl4_62,
inference(rat,[],[s55,s81]) ).
cnf(s83,plain,
~ spl4_51,
inference(rat,[],[s59,s82]) ).
cnf(s85,plain,
~ spl4_52,
inference(rat,[],[s47,s83]) ).
cnf(s86,plain,
~ spl4_54,
inference(rat,[],[s49,s85]) ).
cnf(s87,plain,
~ spl4_41,
inference(rat,[],[s54,s86]) ).
cnf(s89,plain,
~ spl4_42,
inference(rat,[],[s40,s87]) ).
cnf(s90,plain,
~ spl4_44,
inference(rat,[],[s42,s89]) ).
cnf(s91,plain,
~ spl4_43,
inference(rat,[],[s41,s90]) ).
cnf(s92,plain,
~ spl4_33,
inference(rat,[],[s46,s91]) ).
cnf(s93,plain,
~ spl4_34,
inference(rat,[],[s33,s92]) ).
cnf(s94,plain,
~ spl4_36,
inference(rat,[],[s37,s93]) ).
cnf(s95,plain,
~ spl4_35,
inference(rat,[],[s34,s94]) ).
cnf(s96,plain,
~ spl4_29,
inference(rat,[],[s39,s95]) ).
cnf(s97,plain,
~ spl4_32,
inference(rat,[],[s38,s96]) ).
cnf(s98,plain,
~ spl4_31,
inference(rat,[],[s30,s97]) ).
cnf(s99,plain,
~ spl4_25,
inference(rat,[],[s31,s98]) ).
cnf(s100,plain,
~ spl4_28,
inference(rat,[],[s32,s99]) ).
cnf(s102,plain,
~ spl4_27,
inference(rat,[],[s26,s100]) ).
cnf(s103,plain,
~ spl4_21,
inference(rat,[],[s27,s102]) ).
cnf(s104,plain,
~ spl4_24,
inference(rat,[],[s28,s103]) ).
cnf(s106,plain,
~ spl4_23,
inference(rat,[],[s21,s104]) ).
cnf(s107,plain,
~ spl4_17,
inference(rat,[],[s23,s106]) ).
cnf(s108,plain,
~ spl4_20,
inference(rat,[],[s24,s107]) ).
cnf(s110,plain,
~ spl4_19,
inference(rat,[],[s18,s108]) ).
cnf(s111,plain,
~ spl4_14,
inference(rat,[],[s22,s110]) ).
cnf(s113,plain,
~ spl4_13,
inference(rat,[],[s12,s111]) ).
cnf(s114,plain,
~ spl4_10,
inference(rat,[],[s19,s113]) ).
cnf(s115,plain,
~ spl4_5,
inference(rat,[],[s13,s114]) ).
cnf(s117,plain,
~ spl4_8,
inference(rat,[],[s7,s115]) ).
cnf(s118,plain,
~ spl4_3,
inference(rat,[],[s8,s117]) ).
cnf(s120,plain,
~ spl4_2,
inference(rat,[],[s2,s118]) ).
cnf(s121,plain,
$false,
inference(rat,[],[s1,s120,s3]) ).
fof(f2513,plain,
$false,
inference(avatar_sat_refutation,[],[s121]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO038-1.003.004 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n017.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 17:17:21 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.73/1.76 % (3731000)Input is clausal, will run a generic CNF schedule.
% 6.73/1.76 % (3731020)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2462957255:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.73/1.76 % (3731024)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=474978140:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.73/1.76 % (3731026)dis-21_1_sil=8000:lcm=predicate:random_seed=2916322167:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.73/1.76 % (3731026)Refutation not found, incomplete strategy
% 6.73/1.76 % (3731026)------------------------------
% 6.73/1.76 % (3731026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731026)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731026)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.76 % (3731026)Time elapsed: 0.001 s
% 6.73/1.76 % (3731026)Peak memory usage: 88 MB
% 6.73/1.76 % (3731021)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=174612357:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.73/1.76 % (3731023)lrs+10_1_sil=8000:sp=occurrence:random_seed=242135507:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.73/1.76 % (3731022)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3318797127:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.73/1.76 % (3731025)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=758489942:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.73/1.76 % (3731024)Instruction limit reached!
% 6.73/1.76 % (3731024)------------------------------
% 6.73/1.76 % (3731024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731024)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731024)Termination reason: Instruction limit
% 6.73/1.76 % (3731024)Termination phase: Saturation
% 6.73/1.76 % (3731024)Time elapsed: 0.068 s
% 6.73/1.76 % (3731024)Peak memory usage: 88 MB
% 6.73/1.76 % (3731024)Instructions burned: 115 (million)
% 6.73/1.76 % (3731023)Instruction limit reached!
% 6.73/1.76 % (3731023)------------------------------
% 6.73/1.76 % (3731023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731023)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731023)Termination reason: Instruction limit
% 6.73/1.76 % (3731023)Termination phase: Saturation
% 6.73/1.76 % (3731023)Time elapsed: 0.063 s
% 6.73/1.76 % (3731023)Peak memory usage: 89 MB
% 6.73/1.76 % (3731023)Instructions burned: 108 (million)
% 6.73/1.76 % (3731025)Instruction limit reached!
% 6.73/1.76 % (3731025)------------------------------
% 6.73/1.76 % (3731025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731025)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731025)Termination reason: Instruction limit
% 6.73/1.76 % (3731025)Termination phase: Saturation
% 6.73/1.76 % (3731025)Time elapsed: 0.098 s
% 6.73/1.76 % (3731025)Peak memory usage: 89 MB
% 6.73/1.76 % (3731025)Instructions burned: 180 (million)
% 6.73/1.76 % (3731034)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=331218963:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.73/1.76 % (3731034)Refutation not found, incomplete strategy
% 6.73/1.76 % (3731034)------------------------------
% 6.73/1.76 % (3731034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731034)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731034)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.76 % (3731034)Time elapsed: 0.001 s
% 6.73/1.76 % (3731034)Peak memory usage: 88 MB
% 6.73/1.76 % (3731035)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4010944199:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.73/1.76 % (3731036)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1107044958:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 6.73/1.76 % (3731026)------------------------------
% 6.73/1.76 % (3731026)------------------------------
% 6.73/1.76 % (3731035)Instruction limit reached!
% 6.73/1.76 % (3731035)------------------------------
% 6.73/1.76 % (3731035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731035)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731035)Termination reason: Instruction limit
% 6.73/1.76 % (3731035)Termination phase: Saturation
% 6.73/1.76 % (3731035)Time elapsed: 0.086 s
% 6.73/1.76 % (3731035)Peak memory usage: 93 MB
% 6.73/1.76 % (3731035)Instructions burned: 195 (million)
% 6.73/1.76 % (3731036)Instruction limit reached!
% 6.73/1.76 % (3731036)------------------------------
% 6.73/1.76 % (3731036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731036)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731036)Termination reason: Instruction limit
% 6.73/1.76 % (3731036)Termination phase: Saturation
% 6.73/1.76 % (3731036)Time elapsed: 0.098 s
% 6.73/1.76 % (3731036)Peak memory usage: 93 MB
% 6.73/1.76 % (3731036)Instructions burned: 220 (million)
% 6.73/1.76 % (3731041)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=183014152:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.73/1.76 % (3731034)------------------------------
% 6.73/1.76 % (3731034)------------------------------
% 6.73/1.76 % (3731040)lrs+10_64_to=lpo:sil=8000:random_seed=486035279:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.73/1.76 % (3731040)Instruction limit reached!
% 6.73/1.76 % (3731040)------------------------------
% 6.73/1.76 % (3731040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731040)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731040)Termination reason: Instruction limit
% 6.73/1.76 % (3731040)Termination phase: Saturation
% 6.73/1.76 % (3731040)Time elapsed: 0.040 s
% 6.73/1.76 % (3731040)Peak memory usage: 90 MB
% 6.73/1.76 % (3731040)Instructions burned: 130 (million)
% 6.73/1.76 % (3731043)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2824165108:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.73/1.76 % (3731041)Instruction limit reached!
% 6.73/1.76 % (3731041)------------------------------
% 6.73/1.76 % (3731041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731041)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731041)Termination reason: Instruction limit
% 6.73/1.76 % (3731041)Termination phase: Saturation
% 6.73/1.76 % (3731041)Time elapsed: 0.111 s
% 6.73/1.76 % (3731041)Peak memory usage: 89 MB
% 6.73/1.76 % (3731041)Instructions burned: 195 (million)
% 6.73/1.76 % (3731046)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=255138337:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.73/1.76 % (3731047)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=98916786:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.73/1.76 % (3731047)Instruction limit reached!
% 6.73/1.76 % (3731047)------------------------------
% 6.73/1.76 % (3731047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731047)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731047)Termination reason: Instruction limit
% 6.73/1.76 % (3731047)Termination phase: Saturation
% 6.73/1.76 % (3731047)Time elapsed: 0.026 s
% 6.73/1.76 % (3731047)Peak memory usage: 88 MB
% 6.73/1.76 % (3731047)Instructions burned: 111 (million)
% 6.73/1.76 % (3731043)Instruction limit reached!
% 6.73/1.76 % (3731043)------------------------------
% 6.73/1.76 % (3731043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731043)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731043)Termination reason: Instruction limit
% 6.73/1.76 % (3731043)Termination phase: Saturation
% 6.73/1.76 % (3731043)Time elapsed: 0.098 s
% 6.73/1.76 % (3731043)Peak memory usage: 91 MB
% 6.73/1.76 % (3731043)Instructions burned: 157 (million)
% 6.73/1.76 % (3731020)First to succeed.
% 6.73/1.76 % (3731020)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3731000"
% 6.73/1.76 % (3731065)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3298121163:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.73/1.76 % (3731065)Refutation not found, incomplete strategy
% 6.73/1.76 % (3731065)------------------------------
% 6.73/1.76 % (3731065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731065)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731065)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.76 % (3731065)Time elapsed: 0.001 s
% 6.73/1.76 % (3731065)Peak memory usage: 87 MB
% 6.73/1.76 % (3731089)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=204357086:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 6.73/1.76 % (3731091)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=119279524:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 6.73/1.76 % (3731089)Instruction limit reached!
% 6.73/1.76 % (3731089)------------------------------
% 6.73/1.76 % (3731089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731089)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731089)Termination reason: Instruction limit
% 6.73/1.76 % (3731089)Termination phase: Saturation
% 6.73/1.76 % (3731089)Time elapsed: 0.071 s
% 6.73/1.76 % (3731089)Peak memory usage: 90 MB
% 6.73/1.76 % (3731089)Instructions burned: 243 (million)
% 6.73/1.76 % (3731130)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=643150224:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 6.73/1.76 % (3731130)Instruction limit reached!
% 6.73/1.76 % (3731130)------------------------------
% 6.73/1.76 % (3731130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.76 % (3731130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.76 % (3731130)CaDiCaL version: 2.1.3
% 6.73/1.76 % (3731130)Termination reason: Instruction limit
% 6.73/1.76 % (3731130)Termination phase: Saturation
% 6.73/1.76 % (3731130)Time elapsed: 0.044 s
% 6.73/1.76 % (3731130)Peak memory usage: 89 MB
% 6.73/1.76 % (3731130)Instructions burned: 136 (million)
% 6.73/1.76 % (3731065)------------------------------
% 6.73/1.76 % (3731065)------------------------------
% 6.73/1.76 % (3731020)Refutation found. Thanks to Tanya!
% 6.73/1.76 % SZS status Unsatisfiable for theBenchmark
% 6.73/1.76 % SZS output start Proof for theBenchmark
% See solution above
% 8.37/1.95 % (3731020)------------------------------
% 8.37/1.95 % (3731020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.95 % (3731020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.95 % (3731020)CaDiCaL version: 2.1.3
% 8.37/1.95 % (3731020)Termination reason: Refutation
% 8.37/1.95 % (3731020)Time elapsed: 0.691 s
% 8.37/1.95 % (3731020)Peak memory usage: 131 MB
% 8.37/1.95 % (3731020)Instructions burned: 1302 (million)
% 8.37/1.95 % (3731020)------------------------------
% 8.37/1.95 % (3731020)------------------------------
% 8.37/1.95 % (3731000)Success in time 1.094 s
% 8.37/1.95 % Vampire exiting
%------------------------------------------------------------------------------