%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW429-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:19 PM UTC 2026
% Result : Unsatisfiable 5.96s 1.59s
% Output : Refutation 7.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 15
% Syntax : Number of formulae : 246 ( 36 unt; 8 def)
% Number of atoms : 788 ( 107 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1047 ( 505 ~; 534 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 11 ( 9 usr; 9 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 91 ( 0 sgn 91 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_commutative) ).
fof(f2,axiom,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',normalization) ).
fof(f8,axiom,
! [X2,X3,X0,X1] :
( ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_5) ).
fof(f13,axiom,
x4 != x7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_1) ).
fof(f15,axiom,
x3 != x8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_3) ).
fof(f17,axiom,
x5 != x9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_5) ).
fof(f18,plain,
x9 != x5,
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
heap(sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_6) ).
fof(f24,plain,
! [X2,X3,X0,X1] : sep(X1,sep(X3,sep(X0,X2))) = sep(X3,sep(X0,sep(X1,X2))),
inference(superposition,[],[f1,f1]) ).
fof(f32,plain,
heap(sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(superposition,[],[f19,f1]) ).
fof(f37,plain,
heap(sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x7,x12),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f32,f1]) ).
fof(f47,plain,
heap(sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f37,f24]) ).
fof(f57,plain,
heap(sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f47,f24]) ).
fof(f67,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f57,f1]) ).
fof(f77,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f67,f24]) ).
fof(f87,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x4,x7),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f77,f24]) ).
fof(f97,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x7,x12),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f87,f24]) ).
fof(f107,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x6,x9),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f97,f24]) ).
fof(f117,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f107,f24]) ).
fof(f127,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[],[f117,f1]) ).
fof(f137,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x8,x11),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))),
inference(forward_demodulation,[],[f127,f24]) ).
fof(f147,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))),
inference(forward_demodulation,[],[f137,f24]) ).
fof(f157,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x8,x11),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))),
inference(forward_demodulation,[],[f147,f24]) ).
fof(f167,plain,
heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))),
inference(forward_demodulation,[],[f157,f24]) ).
fof(f177,plain,
heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))),
inference(forward_demodulation,[],[f167,f24]) ).
fof(f200,plain,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(lseg(X1,X4),sep(X0,sep(lseg(X1,X2),X3))))
| X1 = X4
| X1 = X2 ),
inference(superposition,[],[f8,f1]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4,X5] : sep(X4,sep(X5,sep(X0,sep(X1,sep(X2,X3))))) = sep(X2,sep(X4,sep(X5,sep(X0,sep(X1,X3))))),
inference(superposition,[],[f24,f24]) ).
fof(f239,plain,
! [X2,X3,X0,X1] : sep(X0,sep(X1,sep(X2,X3))) = sep(X0,sep(X2,sep(X1,X3))),
inference(superposition,[],[f1,f24]) ).
fof(f241,plain,
! [X2,X3,X0,X1,X4] : sep(X2,sep(X4,sep(X0,sep(X1,X3)))) = sep(X4,sep(X0,sep(X1,sep(X2,X3)))),
inference(superposition,[],[f1,f24]) ).
fof(f243,plain,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f8,f24]) ).
fof(f343,plain,
( x7 = x12
| x7 = x8 ),
inference(resolution,[],[f243,f19]) ).
fof(f344,plain,
( x3 = x5
| x3 = x12 ),
inference(resolution,[],[f243,f177]) ).
fof(f351,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ heap(sep(X5,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f243,f24]) ).
fof(f352,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ heap(sep(X5,sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4)))))
| X0 = X3
| X0 = X1 ),
inference(superposition,[],[f243,f24]) ).
fof(f359,definition,
( spl0_1
<=> x3 = x12 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f360,plain,
( x3 != x12
| spl0_1 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f361,plain,
( x3 = x12
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f363,definition,
( spl0_2
<=> x3 = x5 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f364,plain,
( x3 != x5
| spl0_2 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( x3 = x5
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f366,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f344,f363,f359]) ).
fof(f368,definition,
( spl0_3
<=> x7 = x8 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f370,plain,
( x7 = x8
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,definition,
( spl0_4
<=> x7 = x12 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f374,plain,
( x7 = x12
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f375,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f343,f372,f368]) ).
fof(f376,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp))))))))))))
| ~ spl0_2 ),
inference(backward_demodulation,[],[f177,f365]) ).
fof(f379,plain,
( x4 != x8
| ~ spl0_3 ),
inference(backward_demodulation,[],[f13,f370]) ).
fof(f381,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f376,f2]) ).
fof(f383,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f381,f239]) ).
fof(f385,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x8,x8),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp)))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f383,f370]) ).
fof(f387,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x8,x8),sep(lseg(x3,x12),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp)))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f385,f220]) ).
fof(f389,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f387,f2]) ).
fof(f391,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x8),sep(lseg(x4,x8),emp))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f389,f220]) ).
fof(f393,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x4,x8),emp))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f391,f220]) ).
fof(f395,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f393,f24]) ).
fof(f412,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f351,f24]) ).
fof(f413,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))))
| X0 = X3
| X0 = X1 ),
inference(superposition,[],[f351,f24]) ).
fof(f430,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f412,f24]) ).
fof(f453,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X8,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f430,f24]) ).
fof(f475,plain,
( x8 = x11
| x8 = x12
| ~ spl0_2
| ~ spl0_3 ),
inference(resolution,[],[f200,f395]) ).
fof(f490,definition,
( spl0_5
<=> x8 = x12 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f492,plain,
( x8 = x12
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f494,definition,
( spl0_6
<=> x8 = x11 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f496,plain,
( x8 = x11
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f497,plain,
( spl0_5
| spl0_6
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f475,f368,f363,f494,f490]) ).
fof(f498,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x8,x8),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp))))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f177,f370]) ).
fof(f500,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x8,x8),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp))))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f498,f220]) ).
fof(f502,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x8,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp))))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f500,f239]) ).
fof(f504,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x4,x8),emp)))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f502,f2]) ).
fof(f506,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x8),sep(lseg(x4,x8),emp)))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f504,f220]) ).
fof(f508,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x4,x8),emp)))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f506,f220]) ).
fof(f510,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x12),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f508,f241]) ).
fof(f512,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x3),sep(lseg(x8,x3),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f510,f361]) ).
fof(f514,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x5),sep(lseg(x8,x3),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f512,f239]) ).
fof(f516,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x8,x3),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f514,f2]) ).
fof(f518,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x8,x3),sep(lseg(x3,x5),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f516,f239]) ).
fof(f520,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x8,x3),sep(lseg(x3,x5),sep(lseg(x6,x8),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f518,f241]) ).
fof(f533,plain,
( x8 = x11
| x3 = x8
| ~ spl0_1
| ~ spl0_3 ),
inference(resolution,[],[f520,f8]) ).
fof(f534,plain,
( x8 = x11
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f533,f15]) ).
fof(f535,plain,
( spl0_6
| ~ spl0_1
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f534,f368,f359,f494]) ).
fof(f538,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x8),sep(lseg(x8,x8),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x8),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f510,f492]) ).
fof(f540,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x8,x8),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x8),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f538,f239]) ).
fof(f542,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x8,x8),sep(lseg(x3,x5),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x8),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f540,f239]) ).
fof(f544,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x4,x8),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f542,f2]) ).
fof(f546,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x8),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f544,f24]) ).
fof(f548,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x3),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x8),sep(lseg(x3,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f546,f365]) ).
fof(f550,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x8),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x8),sep(lseg(x3,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f548,f239]) ).
fof(f552,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x6,x8),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x8),sep(lseg(x3,x1),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f550,f2]) ).
fof(f554,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x6,x8),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x8),sep(lseg(x4,x8),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f552,f241]) ).
fof(f556,plain,
( x4 = x8
| x4 = x8
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f453,f554]) ).
fof(f563,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X8,sep(X9,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f453,f24]) ).
fof(f590,plain,
( x4 = x8
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f556]) ).
fof(f591,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f590,f379]) ).
fof(f592,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[],[f591]) ).
fof(f596,plain,
( x3 != x11
| ~ spl0_6 ),
inference(backward_demodulation,[],[f15,f496]) ).
fof(f608,plain,
( x3 != x9
| ~ spl0_2 ),
inference(backward_demodulation,[],[f18,f365]) ).
fof(f682,definition,
( spl0_8
<=> x9 = x6 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f683,plain,
( x9 != x6
| spl0_8 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f684,plain,
( x9 = x6
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f691,plain,
( x7 = x11
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f370,f496]) ).
fof(f692,plain,
( heap(sep(lseg(x11,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x11),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp))))))))))))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f177,f496]) ).
fof(f694,plain,
( x4 != x11
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f13,f691]) ).
fof(f696,plain,
( heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x7,x11),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f692,f2]) ).
fof(f698,plain,
( heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x7,x12),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f696,f24]) ).
fof(f700,plain,
( heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x11,x11),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f698,f691]) ).
fof(f702,plain,
( heap(sep(lseg(x11,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f700,f241]) ).
fof(f704,plain,
( heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x4,x11),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f702,f2]) ).
fof(f706,plain,
( heap(sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f704,f220]) ).
fof(f708,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f706,f24]) ).
fof(f710,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x11),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x4,x11),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f708,f220]) ).
fof(f712,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x4,x11),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f710,f239]) ).
fof(f714,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f712,f220]) ).
fof(f716,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x3),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f714,f365]) ).
fof(f718,plain,
( heap(sep(lseg(x3,x3),sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f716,f1]) ).
fof(f720,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f718,f2]) ).
fof(f722,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f720,f239]) ).
fof(f784,plain,
( x3 = x1
| x3 = x12
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f413,f722]) ).
fof(f809,plain,
( x3 = x1
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f784,f360]) ).
fof(f810,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x3),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x3,x6),emp)))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f722,f809]) ).
fof(f811,plain,
( heap(sep(lseg(x3,x3),sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x3,x6),emp)))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f810,f220]) ).
fof(f812,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x6,x9),sep(lseg(x4,x12),sep(lseg(x3,x6),emp))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f811,f2]) ).
fof(f813,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x6,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x6),sep(lseg(x6,x9),sep(lseg(x4,x12),emp))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f812,f24]) ).
fof(f814,plain,
( x3 = x6
| x3 = x12
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f813,f413]) ).
fof(f815,plain,
( x3 = x6
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f814,f360]) ).
fof(f816,plain,
( heap(sep(lseg(x11,x12),sep(lseg(x3,x11),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x3),sep(lseg(x3,x9),sep(lseg(x4,x12),emp))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f813,f815]) ).
fof(f817,plain,
( heap(sep(lseg(x3,x11),sep(lseg(x11,x12),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x3),sep(lseg(x3,x9),sep(lseg(x4,x12),emp))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f816,f1]) ).
fof(f818,plain,
( heap(sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x11,x12),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x9),sep(lseg(x4,x12),emp))))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f817,f241]) ).
fof(f819,plain,
( heap(sep(lseg(x3,x11),sep(lseg(x11,x12),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x3,x9),sep(lseg(x4,x12),emp)))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f818,f2]) ).
fof(f820,plain,
( heap(sep(lseg(x3,x11),sep(lseg(x11,x12),sep(lseg(x3,x9),sep(lseg(x3,x12),sep(lseg(x4,x11),sep(lseg(x4,x12),emp)))))))
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f819,f24]) ).
fof(f821,plain,
( x3 = x9
| x3 = x12
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f820,f351]) ).
fof(f826,plain,
( x3 = x12
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f821,f608]) ).
fof(f832,plain,
( $false
| spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f826,f360]) ).
fof(f833,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f832]) ).
fof(f837,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x6,x11),sep(lseg(x3,x3),sep(lseg(x4,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f722,f361]) ).
fof(f838,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x3),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f837,f239]) ).
fof(f839,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f838,f2]) ).
fof(f840,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f839,f24]) ).
fof(f841,plain,
( x4 = x11
| x4 = x3
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f840,f351]) ).
fof(f842,plain,
( x4 = x3
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f841,f694]) ).
fof(f843,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x6,x11),sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f840,f842]) ).
fof(f846,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x6,x11),sep(lseg(x3,x3),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f843,f239]) ).
fof(f847,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x6,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f846,f239]) ).
fof(f848,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x6,x11),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x1,x6),emp)))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f847,f2]) ).
fof(f849,plain,
( x9 = x6
| x6 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f848,f413]) ).
fof(f851,definition,
( spl0_9
<=> x6 = x11 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f853,plain,
( x6 = x11
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f854,plain,
( spl0_9
| spl0_8
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f849,f494,f368,f363,f359,f682,f851]) ).
fof(f855,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x9,x11),sep(lseg(x3,x1),sep(lseg(x9,x9),sep(lseg(x1,x9),emp)))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(backward_demodulation,[],[f848,f684]) ).
fof(f856,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x9,x11),sep(lseg(x9,x9),sep(lseg(x3,x1),sep(lseg(x1,x9),emp)))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f855,f239]) ).
fof(f857,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x9,x11),sep(lseg(x3,x1),sep(lseg(x1,x9),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f856,f2]) ).
fof(f957,plain,
( x3 = x1
| x3 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(resolution,[],[f352,f857]) ).
fof(f976,plain,
( x3 = x1
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f957,f596]) ).
fof(f977,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x9,x11),sep(lseg(x3,x3),sep(lseg(x3,x9),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(backward_demodulation,[],[f857,f976]) ).
fof(f978,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x9,x11),sep(lseg(x3,x9),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f977,f239]) ).
fof(f979,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x9,x11),sep(lseg(x3,x9),emp)))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f978,f2]) ).
fof(f980,plain,
( x3 = x9
| x3 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(resolution,[],[f979,f352]) ).
fof(f981,plain,
( x3 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f980,f608]) ).
fof(f982,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f981,f596]) ).
fof(f983,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f982]) ).
fof(f984,plain,
( x9 != x11
| spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f683,f853]) ).
fof(f985,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x11,x11),sep(lseg(x3,x1),sep(lseg(x11,x9),sep(lseg(x1,x11),emp)))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f848,f853]) ).
fof(f986,plain,
( heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x11,x9),sep(lseg(x1,x11),emp)))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f985,f24]) ).
fof(f987,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x11,x9),sep(lseg(x1,x11),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f986,f2]) ).
fof(f988,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x11,x9),sep(lseg(x3,x1),sep(lseg(x1,x11),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f987,f239]) ).
fof(f989,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x11,x9),sep(lseg(x1,x11),sep(lseg(x3,x1),emp))))))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f988,f239]) ).
fof(f991,plain,
( x3 = x11
| x9 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(resolution,[],[f989,f200]) ).
fof(f992,plain,
( x9 = x11
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f991,f596]) ).
fof(f994,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| spl0_8
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f992,f984]) ).
fof(f995,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| spl0_8
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f994]) ).
fof(f1078,plain,
( x4 != x12
| ~ spl0_4 ),
inference(forward_demodulation,[],[f13,f374]) ).
fof(f1080,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x12,x8),sep(lseg(x1,x6),sep(lseg(x12,x12),sep(lseg(x6,x12),sep(lseg(x4,x12),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f177,f374]) ).
fof(f1081,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x12,x12),sep(lseg(x6,x12),sep(lseg(x4,x12),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1080,f241]) ).
fof(f1082,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x12,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x12),sep(lseg(x4,x12),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1081,f241]) ).
fof(f1083,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x6,x12),sep(lseg(x4,x12),emp)))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1082,f2]) ).
fof(f1084,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x6,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x1,x6),sep(lseg(x4,x12),emp)))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1083,f241]) ).
fof(f1085,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x6,x12),sep(lseg(x5,x1),sep(lseg(x4,x12),sep(lseg(x4,x12),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1084,f24]) ).
fof(f1086,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x6,x12),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x4,x12),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1085,f365]) ).
fof(f1087,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x6,x9),sep(lseg(x6,x12),sep(lseg(x3,x1),sep(lseg(x4,x12),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1086,f2]) ).
fof(f1088,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x3,x1),sep(lseg(x6,x9),sep(lseg(x6,x12),sep(lseg(x4,x12),sep(lseg(x4,x12),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1087,f24]) ).
fof(f1091,plain,
( x4 = x12
| x4 = x12
| ~ spl0_2
| ~ spl0_4 ),
inference(resolution,[],[f1088,f563]) ).
fof(f1092,plain,
( x4 = x12
| ~ spl0_2
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f1091]) ).
fof(f1093,plain,
( $false
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1092,f1078]) ).
fof(f1094,plain,
( ~ spl0_2
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1093]) ).
fof(f1103,plain,
( x4 != x3
| ~ spl0_1
| ~ spl0_4 ),
inference(backward_demodulation,[],[f1078,f361]) ).
fof(f1106,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x3),sep(lseg(x3,x8),sep(lseg(x6,x9),sep(lseg(x6,x3),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1085,f361]) ).
fof(f1107,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x5),sep(lseg(x3,x8),sep(lseg(x6,x9),sep(lseg(x6,x3),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1106,f239]) ).
fof(f1108,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x8),sep(lseg(x6,x9),sep(lseg(x6,x3),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1107,f2]) ).
fof(f1109,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x9),sep(lseg(x6,x3),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1108,f239]) ).
fof(f1110,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1109,f239]) ).
fof(f1111,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x3),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1110,f24]) ).
fof(f1112,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x8),sep(lseg(x3,x5),sep(lseg(x6,x3),sep(lseg(x4,x3),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1111,f241]) ).
fof(f1114,plain,
( x4 = x3
| x4 = x3
| ~ spl0_1
| ~ spl0_4 ),
inference(resolution,[],[f1112,f430]) ).
fof(f1115,plain,
( x4 = x3
| ~ spl0_1
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f1114]) ).
fof(f1116,plain,
( $false
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1115,f1103]) ).
fof(f1117,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1116]) ).
fof(f1122,plain,
( x7 = x11
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f370,f496]) ).
fof(f1123,plain,
( x3 != x11
| ~ spl0_6 ),
inference(backward_demodulation,[],[f15,f496]) ).
fof(f1124,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x3,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x3),sep(lseg(x6,x7),sep(lseg(x4,x7),emp))))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f177,f361]) ).
fof(f1126,plain,
( x4 != x11
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f13,f1122]) ).
fof(f1127,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x3),sep(lseg(x3,x5),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x3),sep(lseg(x6,x7),sep(lseg(x4,x7),emp))))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1124,f239]) ).
fof(f1128,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x4,x3),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x3),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1127,f2]) ).
fof(f1129,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x7,x3),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1128,f24]) ).
fof(f1130,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x7,x3),sep(lseg(x5,x1),sep(lseg(x7,x8),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x4,x7),emp)))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1129,f241]) ).
fof(f1131,plain,
( heap(sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x11,x3),sep(lseg(x5,x1),sep(lseg(x11,x8),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1130,f1122]) ).
fof(f1132,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x11,x8),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1131,f220]) ).
fof(f1133,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x8,x11),sep(lseg(x11,x8),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1132,f220]) ).
fof(f1134,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x11),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1133,f239]) ).
fof(f1135,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x4,x11),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1134,f220]) ).
fof(f1136,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1135,f220]) ).
fof(f1137,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x11,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1136,f496]) ).
fof(f1138,plain,
( heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1137,f1]) ).
fof(f1139,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1138,f2]) ).
fof(f1140,plain,
( heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1139,f1]) ).
fof(f1141,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x4,x11),sep(lseg(x4,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1140,f2]) ).
fof(f1142,plain,
( x4 = x11
| x4 = x3
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f1141,f412]) ).
fof(f1143,plain,
( x4 = x3
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1142,f1126]) ).
fof(f1144,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[],[f1141,f1143]) ).
fof(f1147,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x3,x3),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1144,f24]) ).
fof(f1148,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x3),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1147,f24]) ).
fof(f1149,plain,
( heap(sep(lseg(x11,x3),sep(lseg(x3,x11),sep(lseg(x3,x5),sep(lseg(x6,x11),sep(lseg(x6,x9),sep(lseg(x5,x1),sep(lseg(x1,x6),emp))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1148,f2]) ).
fof(f1150,plain,
( x3 = x11
| x3 = x5
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(resolution,[],[f1149,f243]) ).
fof(f1153,plain,
( x3 = x5
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1150,f1123]) ).
fof(f1156,plain,
( $false
| ~ spl0_1
| spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1153,f364]) ).
fof(f1157,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f366]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f375]) ).
cnf(s3,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f497]) ).
cnf(s4,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_6 ),
inference(sat_conversion,[],[f535]) ).
cnf(s5,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(sat_conversion,[],[f592]) ).
cnf(s11,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(sat_conversion,[],[f833]) ).
cnf(s12,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f854]) ).
cnf(s13,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8 ),
inference(sat_conversion,[],[f983]) ).
cnf(s14,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f995]) ).
cnf(s17,plain,
( ~ spl0_2
| ~ spl0_4 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s19,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s22,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s23,plain,
spl0_1,
inference(rat,[],[s3,s11,s5,s2,s17,s1]) ).
cnf(s24,plain,
~ spl0_4,
inference(rat,[],[s19,s23]) ).
cnf(s25,plain,
spl0_3,
inference(rat,[],[s2,s24]) ).
cnf(s26,plain,
spl0_6,
inference(rat,[],[s4,s23,s25]) ).
cnf(s28,plain,
spl0_2,
inference(rat,[],[s22,s25,s23,s26]) ).
cnf(s29,plain,
~ spl0_8,
inference(rat,[],[s13,s25,s26,s23,s28]) ).
cnf(s30,plain,
~ spl0_9,
inference(rat,[],[s14,s28,s25,s26,s23,s29]) ).
cnf(s31,plain,
$false,
inference(rat,[],[s12,s23,s25,s26,s28,s30,s29]) ).
fof(f1158,plain,
$false,
inference(avatar_sat_refutation,[],[s31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW429-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n020.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 13:53:49 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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
% 5.96/1.59 % (172925)Input is clausal, will run a generic CNF schedule.
% 5.96/1.59 % (172932)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=953485885:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.96/1.59 % (172934)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1935452603:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.96/1.59 % (172931)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3723348446:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.96/1.59 % (172933)lrs+10_1_sil=8000:sp=occurrence:random_seed=3312417351:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.96/1.59 % (172936)dis-21_1_sil=8000:lcm=predicate:random_seed=2605309205: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)
% 5.96/1.59 % (172930)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=2079057803:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.96/1.59 % (172936)Refutation not found, incomplete strategy
% 5.96/1.59 % (172936)------------------------------
% 5.96/1.59 % (172936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172936)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172936)Termination reason: Refutation not found, incomplete strategy
% 5.96/1.59 % (172936)Time elapsed: 0.003 s
% 5.96/1.59 % (172936)Peak memory usage: 88 MB
% 5.96/1.59 % (172936)Instructions burned: 4 (million)
% 5.96/1.59 % (172935)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2158737012:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.96/1.59 % (172933)Instruction limit reached!
% 5.96/1.59 % (172933)------------------------------
% 5.96/1.59 % (172933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172933)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172933)Termination reason: Instruction limit
% 5.96/1.59 % (172933)Termination phase: Saturation
% 5.96/1.59 % (172933)Time elapsed: 0.055 s
% 5.96/1.59 % (172933)Peak memory usage: 88 MB
% 5.96/1.59 % (172933)Instructions burned: 107 (million)
% 5.96/1.59 % (172934)Instruction limit reached!
% 5.96/1.59 % (172934)------------------------------
% 5.96/1.59 % (172934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172934)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172934)Termination reason: Instruction limit
% 5.96/1.59 % (172934)Termination phase: Saturation
% 5.96/1.59 % (172934)Time elapsed: 0.065 s
% 5.96/1.59 % (172934)Peak memory usage: 88 MB
% 5.96/1.59 % (172934)Instructions burned: 114 (million)
% 5.96/1.59 % (172935)Instruction limit reached!
% 5.96/1.59 % (172935)------------------------------
% 5.96/1.59 % (172935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172935)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172935)Termination reason: Instruction limit
% 5.96/1.59 % (172935)Termination phase: Saturation
% 5.96/1.59 % (172935)Time elapsed: 0.101 s
% 5.96/1.59 % (172935)Peak memory usage: 89 MB
% 5.96/1.59 % (172935)Instructions burned: 181 (million)
% 5.96/1.59 % (172944)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=2721729549:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.96/1.59 % (172944)Refutation not found, incomplete strategy
% 5.96/1.59 % (172944)------------------------------
% 5.96/1.59 % (172944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172944)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172944)Termination reason: Refutation not found, incomplete strategy
% 5.96/1.59 % (172944)Time elapsed: 0.004 s
% 5.96/1.59 % (172944)Peak memory usage: 88 MB
% 5.96/1.59 % (172944)Instructions burned: 4 (million)
% 5.96/1.59 % (172945)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=571376715: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)
% 5.96/1.59 % (172936)------------------------------
% 5.96/1.59 % (172936)------------------------------
% 5.96/1.59 % (172946)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1433207176:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.96/1.59 % (172946)Refutation not found, incomplete strategy
% 5.96/1.59 % (172946)------------------------------
% 5.96/1.59 % (172946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172946)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172946)Termination reason: Refutation not found, incomplete strategy
% 5.96/1.59 % (172946)Time elapsed: 0.002 s
% 5.96/1.59 % (172946)Peak memory usage: 88 MB
% 5.96/1.59 % (172946)Instructions burned: 2 (million)
% 5.96/1.59 % (172945)Instruction limit reached!
% 5.96/1.59 % (172945)------------------------------
% 5.96/1.59 % (172945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172945)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172945)Termination reason: Instruction limit
% 5.96/1.59 % (172945)Termination phase: Saturation
% 5.96/1.59 % (172945)Time elapsed: 0.119 s
% 5.96/1.59 % (172945)Peak memory usage: 90 MB
% 5.96/1.59 % (172945)Instructions burned: 189 (million)
% 5.96/1.59 % (172949)lrs+10_64_to=lpo:sil=8000:random_seed=399493237:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.96/1.59 % (172949)Instruction limit reached!
% 5.96/1.59 % (172949)------------------------------
% 5.96/1.59 % (172949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172949)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172949)Termination reason: Instruction limit
% 5.96/1.59 % (172949)Termination phase: Saturation
% 5.96/1.59 % (172949)Time elapsed: 0.039 s
% 5.96/1.59 % (172949)Peak memory usage: 88 MB
% 5.96/1.59 % (172949)Instructions burned: 129 (million)
% 5.96/1.59 % (172944)------------------------------
% 5.96/1.59 % (172944)------------------------------
% 5.96/1.59 % (172932)First to succeed.
% 5.96/1.59 % (172951)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2036447463:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 5.96/1.59 % (172932)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-172925"
% 5.96/1.59 % (172946)------------------------------
% 5.96/1.59 % (172946)------------------------------
% 5.96/1.59 % (172953)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2538940484:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.96/1.59 % (172951)Instruction limit reached!
% 5.96/1.59 % (172951)------------------------------
% 5.96/1.59 % (172951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172951)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172951)Termination reason: Instruction limit
% 5.96/1.59 % (172951)Termination phase: Saturation
% 5.96/1.59 % (172951)Time elapsed: 0.113 s
% 5.96/1.59 % (172951)Peak memory usage: 89 MB
% 5.96/1.59 % (172951)Instructions burned: 195 (million)
% 5.96/1.59 % (172954)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1647987870:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.96/1.59 % (172953)Instruction limit reached!
% 5.96/1.59 % (172953)------------------------------
% 5.96/1.59 % (172953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.96/1.59 % (172953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.59 % (172953)CaDiCaL version: 2.1.3
% 5.96/1.59 % (172953)Termination reason: Instruction limit
% 5.96/1.59 % (172953)Termination phase: Saturation
% 5.96/1.59 % (172953)Time elapsed: 0.055 s
% 5.96/1.59 % (172953)Peak memory usage: 90 MB
% 5.96/1.59 % (172953)Instructions burned: 159 (million)
% 5.96/1.59 % (172956)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=212524808:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 5.96/1.59 % (172960)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1972068628:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 5.96/1.59 % (172932)Refutation found. Thanks to Tanya!
% 5.96/1.59 % SZS status Unsatisfiable for theBenchmark
% 5.96/1.59 % SZS output start Proof for theBenchmark
% See solution above
% 7.16/1.79 % (172932)------------------------------
% 7.16/1.79 % (172932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.79 % (172932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.79 % (172932)CaDiCaL version: 2.1.3
% 7.16/1.79 % (172932)Termination reason: Refutation
% 7.16/1.79 % (172932)Time elapsed: 0.531 s
% 7.16/1.79 % (172932)Peak memory usage: 130 MB
% 7.16/1.79 % (172932)Instructions burned: 1133 (million)
% 7.16/1.79 % (172932)------------------------------
% 7.16/1.79 % (172932)------------------------------
% 7.16/1.79 % (172925)Success in time 0.929 s
% 7.16/1.79 % Vampire exiting
%------------------------------------------------------------------------------