%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG192+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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 09:29:12 AM UTC 2026
% Result : Unsatisfiable 0.82s 0.37s
% Output : Refutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 49
% Syntax : Number of formulae : 403 ( 60 unt; 38 def)
% Number of atoms : 1341 ( 621 equ)
% Maximal formula atoms : 125 ( 3 avg)
% Number of connectives : 1553 ( 615 ~; 708 |; 192 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 39 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f3,axiom,
( op(op(e0,e0),op(e0,e0)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e4,e4),op(e4,e4)) = e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e4)) = e4
& op(e1,op(e1,e0)) = e0
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e4)) = e4
& op(e2,op(e2,e0)) = e0
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e4)) = e4
& op(e3,op(e3,e0)) = e0
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e4)) = e4
& op(e4,op(e4,e0)) = e0
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e4)) = e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f8,axiom,
~ ( e0 = op(op(e4,e1),e4)
& e2 = op(e4,op(op(e4,e1),e4))
& e3 = op(e4,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f14,axiom,
~ ( e0 = op(op(e4,e2),e4)
& e1 = op(e4,op(op(e4,e2),e4))
& e3 = op(e4,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f32,axiom,
~ ( e1 = op(op(e4,e0),e4)
& e2 = op(e4,op(op(e4,e0),e4))
& e3 = op(e4,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax32) ).
fof(f38,axiom,
~ ( e1 = op(op(e4,e2),e4)
& e0 = op(e4,op(op(e4,e2),e4))
& e3 = op(e4,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax38) ).
fof(f56,axiom,
~ ( e2 = op(op(e4,e0),e4)
& e1 = op(e4,op(op(e4,e0),e4))
& e3 = op(e4,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax56) ).
fof(f62,axiom,
~ ( e2 = op(op(e4,e1),e4)
& e0 = op(e4,op(op(e4,e1),e4))
& e3 = op(e4,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax62) ).
fof(f128,plain,
( e0 != op(op(e4,e1),e4)
| e2 != op(e4,op(op(e4,e1),e4))
| e3 != op(e4,e1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f134,plain,
( e0 != op(op(e4,e2),e4)
| e1 != op(e4,op(op(e4,e2),e4))
| e3 != op(e4,e2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f152,plain,
( e1 != op(op(e4,e0),e4)
| e2 != op(e4,op(op(e4,e0),e4))
| e3 != op(e4,e0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f158,plain,
( e1 != op(op(e4,e2),e4)
| e0 != op(e4,op(op(e4,e2),e4))
| e3 != op(e4,e2) ),
inference(ennf_transformation,[],[f38]) ).
fof(f176,plain,
( e2 != op(op(e4,e0),e4)
| e1 != op(e4,op(op(e4,e0),e4))
| e3 != op(e4,e0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f182,plain,
( e2 != op(op(e4,e1),e4)
| e0 != op(e4,op(op(e4,e1),e4))
| e3 != op(e4,e1) ),
inference(ennf_transformation,[],[f62]) ).
fof(f247,plain,
( e0 = op(e4,e4)
| e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f248,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f250,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f251,plain,
( e0 = op(e4,e0)
| e1 = op(e4,e0)
| e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f252,plain,
( e0 = op(e3,e4)
| e1 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f322,plain,
e4 = op(op(e4,e4),op(e4,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f323,plain,
e4 = op(op(e3,e4),op(e4,e3)),
inference(cnf_transformation,[],[f3]) ).
fof(f327,plain,
e3 = op(op(e4,e3),op(e3,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f337,plain,
e1 = op(op(e4,e1),op(e1,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f342,plain,
e0 = op(op(e4,e0),op(e0,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f347,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f350,plain,
op(e4,e1) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f351,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f353,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f354,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f356,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f397,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f398,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f400,plain,
op(e1,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f403,plain,
op(e0,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f418,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f431,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f443,plain,
op(e0,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f447,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f450,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f453,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f458,plain,
e3 = op(e4,op(e4,e3)),
inference(cnf_transformation,[],[f6]) ).
fof(f460,plain,
e1 = op(e4,op(e4,e1)),
inference(cnf_transformation,[],[f6]) ).
fof(f461,plain,
e0 = op(e4,op(e4,e0)),
inference(cnf_transformation,[],[f6]) ).
fof(f462,plain,
e4 = op(e3,op(e3,e4)),
inference(cnf_transformation,[],[f6]) ).
fof(f463,plain,
e3 = op(e3,op(e3,e3)),
inference(cnf_transformation,[],[f6]) ).
fof(f464,plain,
e2 = op(e3,op(e3,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f465,plain,
e1 = op(e3,op(e3,e1)),
inference(cnf_transformation,[],[f6]) ).
fof(f466,plain,
e0 = op(e3,op(e3,e0)),
inference(cnf_transformation,[],[f6]) ).
fof(f469,plain,
e2 = op(e2,op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f472,plain,
e4 = op(e1,op(e1,e4)),
inference(cnf_transformation,[],[f6]) ).
fof(f475,plain,
e1 = op(e1,op(e1,e1)),
inference(cnf_transformation,[],[f6]) ).
fof(f477,plain,
e4 = op(e0,op(e0,e4)),
inference(cnf_transformation,[],[f6]) ).
fof(f481,plain,
e0 = op(e0,op(e0,e0)),
inference(cnf_transformation,[],[f6]) ).
fof(f483,plain,
( e0 != op(op(e4,e1),e4)
| e2 != op(e4,op(op(e4,e1),e4))
| e3 != op(e4,e1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f489,plain,
( e0 != op(op(e4,e2),e4)
| e1 != op(e4,op(op(e4,e2),e4))
| e3 != op(e4,e2) ),
inference(cnf_transformation,[],[f134]) ).
fof(f507,plain,
( e1 != op(op(e4,e0),e4)
| e2 != op(e4,op(op(e4,e0),e4))
| e3 != op(e4,e0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f513,plain,
( e1 != op(op(e4,e2),e4)
| e0 != op(e4,op(op(e4,e2),e4))
| e3 != op(e4,e2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f531,plain,
( e2 != op(op(e4,e0),e4)
| e1 != op(e4,op(op(e4,e0),e4))
| e3 != op(e4,e0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f537,plain,
( e2 != op(op(e4,e1),e4)
| e0 != op(e4,op(op(e4,e1),e4))
| e3 != op(e4,e1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f603,definition,
( spl0_1
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f604,plain,
( e4 = op(e3,e1)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f605,plain,
( e4 != op(e3,e1)
| spl0_1 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f616,definition,
( spl0_4
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f617,plain,
( e3 = op(e4,e1)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f618,plain,
( e3 != op(e4,e1)
| spl0_4 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f620,definition,
( spl0_5
<=> e2 = op(e4,op(op(e4,e1),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f622,plain,
( e2 != op(e4,op(op(e4,e1),e4))
| spl0_5 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f624,definition,
( spl0_6
<=> e0 = op(op(e4,e1),e4) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f626,plain,
( e0 != op(op(e4,e1),e4)
| spl0_6 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f627,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f483,f624,f620,f616]) ).
fof(f642,definition,
( spl0_10
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f643,plain,
( e2 = op(e4,e1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f644,plain,
( e2 != op(e4,e1)
| spl0_10 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f669,definition,
( spl0_16
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f670,plain,
( e4 = op(e3,e2)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f671,plain,
( e4 != op(e3,e2)
| spl0_16 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f682,definition,
( spl0_19
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f683,plain,
( e3 = op(e4,e2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f684,plain,
( e3 != op(e4,e2)
| spl0_19 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f686,definition,
( spl0_20
<=> e1 = op(e4,op(op(e4,e2),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f688,plain,
( e1 != op(e4,op(op(e4,e2),e4))
| spl0_20 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f690,definition,
( spl0_21
<=> e0 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f692,plain,
( e0 != op(op(e4,e2),e4)
| spl0_21 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f693,plain,
( ~ spl0_19
| ~ spl0_20
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f489,f690,f686,f682]) ).
fof(f708,definition,
( spl0_25
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f709,plain,
( e1 = op(e4,e2)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f710,plain,
( e1 != op(e4,e2)
| spl0_25 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f748,definition,
( spl0_34
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f749,plain,
( e2 = op(e4,e3)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f750,plain,
( e2 != op(e4,e3)
| spl0_34 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f774,definition,
( spl0_40
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f775,plain,
( e1 = op(e4,e3)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f776,plain,
( e1 != op(e4,e3)
| spl0_40 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f814,definition,
( spl0_49
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f815,plain,
( e2 = op(e3,e4)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f816,plain,
( e2 != op(e3,e4)
| spl0_49 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f840,definition,
( spl0_55
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f841,plain,
( e1 = op(e3,e4)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f842,plain,
( e1 != op(e3,e4)
| spl0_55 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f867,definition,
( spl0_61
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f868,plain,
( e4 = op(e3,e0)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f869,plain,
( e4 != op(e3,e0)
| spl0_61 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f880,definition,
( spl0_64
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f881,plain,
( e3 = op(e4,e0)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f882,plain,
( e3 != op(e4,e0)
| spl0_64 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl0_65
<=> e2 = op(e4,op(op(e4,e0),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f886,plain,
( e2 != op(e4,op(op(e4,e0),e4))
| spl0_65 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f888,definition,
( spl0_66
<=> e1 = op(op(e4,e0),e4) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f890,plain,
( e1 != op(op(e4,e0),e4)
| spl0_66 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f891,plain,
( ~ spl0_64
| ~ spl0_65
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f507,f888,f884,f880]) ).
fof(f906,definition,
( spl0_70
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f907,plain,
( e2 = op(e4,e0)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f908,plain,
( e2 != op(e4,e0)
| spl0_70 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f946,definition,
( spl0_79
<=> e0 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f948,plain,
( e0 != op(e4,e2)
| spl0_79 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f950,definition,
( spl0_80
<=> e1 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f952,plain,
( e1 != op(op(e4,e2),e4)
| spl0_80 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f986,definition,
( spl0_88
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f987,plain,
( e0 = op(e4,e3)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f986]) ).
fof(f1026,definition,
( spl0_97
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f1027,plain,
( e0 = op(e3,e4)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1028,plain,
( e0 != op(e3,e4)
| spl0_97 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1066,definition,
( spl0_106
<=> e1 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f1067,plain,
( e1 = op(e4,e0)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1068,plain,
( e1 != op(e4,e0)
| spl0_106 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1070,definition,
( spl0_107
<=> e2 = op(op(e4,e0),e4) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f1072,plain,
( e2 != op(op(e4,e0),e4)
| spl0_107 ),
inference(avatar_component_clause,[],[f1070]) ).
fof(f1106,definition,
( spl0_115
<=> e0 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f1107,plain,
( e0 = op(e4,e1)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1110,definition,
( spl0_116
<=> e2 = op(op(e4,e1),e4) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f1112,plain,
( e2 != op(op(e4,e1),e4)
| spl0_116 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1189,definition,
( spl0_133
<=> e1 = op(e4,op(op(e4,e0),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1191,plain,
( e1 != op(e4,op(op(e4,e0),e4))
| spl0_133 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1217,definition,
( spl0_139
<=> e0 = op(e4,op(op(e4,e1),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1219,plain,
( e0 != op(e4,op(op(e4,e1),e4))
| spl0_139 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1245,definition,
( spl0_145
<=> e0 = op(e4,op(op(e4,e2),e4)) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1247,plain,
( e0 != op(e4,op(op(e4,e2),e4))
| spl0_145 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1249,definition,
( spl0_146
<=> e3 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1250,plain,
( e3 = op(op(e4,e2),e4)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1249]) ).
fof(f1251,plain,
( e3 != op(op(e4,e2),e4)
| spl0_146 ),
inference(avatar_component_clause,[],[f1249]) ).
fof(f1423,definition,
( spl0_181
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1425,plain,
( e4 = op(e4,e4)
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f1423]) ).
fof(f1427,definition,
( spl0_182
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f1429,plain,
( e3 = op(e4,e4)
| ~ spl0_182 ),
inference(avatar_component_clause,[],[f1427]) ).
fof(f1431,definition,
( spl0_183
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1433,plain,
( e2 = op(e4,e4)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1431]) ).
fof(f1435,definition,
( spl0_184
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1437,plain,
( e1 = op(e4,e4)
| ~ spl0_184 ),
inference(avatar_component_clause,[],[f1435]) ).
fof(f1439,definition,
( spl0_185
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_185])],[avatar_definition]) ).
fof(f1441,plain,
( e0 = op(e4,e4)
| ~ spl0_185 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1442,plain,
( spl0_181
| spl0_182
| spl0_183
| spl0_184
| spl0_185 ),
inference(avatar_split_clause,[],[f247,f1439,f1435,f1431,f1427,f1423]) ).
fof(f1444,plain,
( e4 != op(e4,e3)
| ~ spl0_181 ),
inference(superposition,[],[f347,f1425]) ).
fof(f1446,plain,
( e4 != op(e4,e1)
| ~ spl0_181 ),
inference(superposition,[],[f350,f1425]) ).
fof(f1448,plain,
( e4 != op(e3,e4)
| ~ spl0_181 ),
inference(superposition,[],[f397,f1425]) ).
fof(f1453,plain,
( e0 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f248,f776]) ).
fof(f1454,plain,
( e0 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl0_34
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f1453,f750]) ).
fof(f1455,plain,
( e0 = op(e4,e3)
| e3 = op(e4,e3)
| spl0_34
| spl0_40
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f1454,f1444]) ).
fof(f1457,definition,
( spl0_186
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f1459,plain,
( e3 = op(e4,e3)
| ~ spl0_186 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1460,plain,
( spl0_186
| spl0_88
| spl0_34
| spl0_40
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f1455,f1423,f774,f748,f986,f1457]) ).
fof(f1462,plain,
( e3 = op(e3,op(e3,e4))
| ~ spl0_186 ),
inference(superposition,[],[f327,f1459]) ).
fof(f1481,plain,
( e3 = e4
| ~ spl0_186 ),
inference(superposition,[],[f1462,f462]) ).
fof(f1485,plain,
( $false
| ~ spl0_186 ),
inference(forward_subsumption_resolution,[],[f1481,f447]) ).
fof(f1486,plain,
~ spl0_186,
inference(avatar_contradiction_clause,[],[f1485]) ).
fof(f1492,plain,
( e2 != op(e4,e1)
| ~ spl0_34 ),
inference(superposition,[],[f351,f749]) ).
fof(f1498,plain,
( e3 = op(e4,e2)
| ~ spl0_34 ),
inference(superposition,[],[f458,f749]) ).
fof(f1506,plain,
( $false
| spl0_19
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1498,f684]) ).
fof(f1507,plain,
( spl0_19
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f1506]) ).
fof(f1509,plain,
( ~ spl0_19
| ~ spl0_145
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f513,f950,f1245,f682]) ).
fof(f1526,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1)
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f250,f644]) ).
fof(f1527,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e4 = op(e4,e1)
| spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1526,f618]) ).
fof(f1528,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| spl0_4
| spl0_10
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f1527,f1446]) ).
fof(f1530,definition,
( spl0_187
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1532,plain,
( e1 = op(e4,e1)
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f1530]) ).
fof(f1533,plain,
( spl0_187
| spl0_115
| spl0_4
| spl0_10
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f1528,f1423,f642,f616,f1106,f1530]) ).
fof(f1535,plain,
( e1 = op(e1,op(e1,e4))
| ~ spl0_187 ),
inference(superposition,[],[f337,f1532]) ).
fof(f1553,plain,
( e1 = e4
| ~ spl0_187 ),
inference(superposition,[],[f1535,f472]) ).
fof(f1557,plain,
( $false
| ~ spl0_187 ),
inference(forward_subsumption_resolution,[],[f1553,f450]) ).
fof(f1558,plain,
~ spl0_187,
inference(avatar_contradiction_clause,[],[f1557]) ).
fof(f1560,plain,
( ~ spl0_4
| ~ spl0_139
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f537,f1110,f1217,f616]) ).
fof(f1564,plain,
( ~ spl0_10
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1492,f748,f642]) ).
fof(f1574,plain,
( e1 = op(e4,e2)
| ~ spl0_10 ),
inference(superposition,[],[f460,f643]) ).
fof(f1583,plain,
( $false
| ~ spl0_10
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1574,f710]) ).
fof(f1584,plain,
( ~ spl0_10
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f1583]) ).
fof(f1617,plain,
( e3 = op(e4,e1)
| ~ spl0_40 ),
inference(superposition,[],[f458,f775]) ).
fof(f1626,plain,
( $false
| spl0_4
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f1617,f618]) ).
fof(f1627,plain,
( spl0_4
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f1626]) ).
fof(f1632,plain,
( e0 != op(e4,e1)
| ~ spl0_88 ),
inference(superposition,[],[f351,f987]) ).
fof(f1638,plain,
( e3 = op(e4,e0)
| ~ spl0_88 ),
inference(superposition,[],[f458,f987]) ).
fof(f1648,plain,
( $false
| spl0_64
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1638,f882]) ).
fof(f1649,plain,
( spl0_64
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1648]) ).
fof(f1654,plain,
( ~ spl0_115
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f1632,f986,f1106]) ).
fof(f1660,plain,
( e3 != op(e2,e2)
| ~ spl0_19 ),
inference(superposition,[],[f418,f683]) ).
fof(f1664,plain,
( e1 != op(e4,op(e3,e4))
| ~ spl0_19
| spl0_20 ),
inference(superposition,[],[f688,f683]) ).
fof(f1665,plain,
( e0 != op(e3,e4)
| ~ spl0_19
| spl0_21 ),
inference(superposition,[],[f692,f683]) ).
fof(f1669,plain,
( e1 != op(e3,e4)
| ~ spl0_19
| spl0_80 ),
inference(superposition,[],[f952,f683]) ).
fof(f1670,plain,
( e3 != op(e3,e4)
| ~ spl0_19
| spl0_146 ),
inference(superposition,[],[f1251,f683]) ).
fof(f1699,plain,
( e1 = op(e4,e0)
| ~ spl0_115 ),
inference(superposition,[],[f460,f1107]) ).
fof(f1709,plain,
( $false
| spl0_106
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1699,f1068]) ).
fof(f1710,plain,
( spl0_106
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f1709]) ).
fof(f1729,plain,
( e1 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f252,f1028]) ).
fof(f1730,plain,
( e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_55
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f1729,f842]) ).
fof(f1731,plain,
( e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_49
| spl0_55
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f1730,f816]) ).
fof(f1732,plain,
( e4 = op(e3,e4)
| ~ spl0_19
| spl0_49
| spl0_55
| spl0_97
| spl0_146 ),
inference(forward_subsumption_resolution,[],[f1731,f1670]) ).
fof(f1733,plain,
( $false
| ~ spl0_19
| spl0_49
| spl0_55
| spl0_97
| spl0_146
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f1732,f1448]) ).
fof(f1734,plain,
( ~ spl0_19
| spl0_49
| spl0_55
| spl0_97
| spl0_146
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f1733]) ).
fof(f1739,plain,
( ~ spl0_97
| ~ spl0_19
| spl0_21 ),
inference(avatar_split_clause,[],[f1665,f690,f682,f1026]) ).
fof(f1744,plain,
( e3 = op(op(e4,e3),e2)
| ~ spl0_49 ),
inference(superposition,[],[f327,f815]) ).
fof(f1771,plain,
( e3 = op(e2,e2)
| ~ spl0_34
| ~ spl0_49 ),
inference(forward_demodulation,[],[f1744,f749]) ).
fof(f1773,plain,
( $false
| ~ spl0_19
| ~ spl0_34
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1771,f1660]) ).
fof(f1774,plain,
( ~ spl0_19
| ~ spl0_34
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f1773]) ).
fof(f1775,plain,
( e3 = op(e3,e4)
| ~ spl0_19
| ~ spl0_146 ),
inference(forward_demodulation,[],[f1250,f683]) ).
fof(f1778,plain,
( e4 = op(e3,op(e4,e3))
| ~ spl0_19
| ~ spl0_146 ),
inference(superposition,[],[f323,f1775]) ).
fof(f1805,plain,
( e4 = op(e3,e2)
| ~ spl0_19
| ~ spl0_34
| ~ spl0_146 ),
inference(forward_demodulation,[],[f1778,f749]) ).
fof(f1806,plain,
( $false
| spl0_16
| ~ spl0_19
| ~ spl0_34
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f1805,f671]) ).
fof(f1807,plain,
( spl0_16
| ~ spl0_19
| ~ spl0_34
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f1806]) ).
fof(f1812,plain,
( ~ spl0_55
| ~ spl0_19
| spl0_80 ),
inference(avatar_split_clause,[],[f1669,f950,f682,f840]) ).
fof(f1814,plain,
( e0 = op(e3,e4)
| e1 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_49 ),
inference(forward_subsumption_resolution,[],[f252,f816]) ).
fof(f1835,plain,
( e1 != op(e4,e0)
| ~ spl0_19
| spl0_20
| ~ spl0_97 ),
inference(superposition,[],[f1664,f1027]) ).
fof(f1844,plain,
( $false
| ~ spl0_19
| spl0_20
| ~ spl0_97
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f1835,f1067]) ).
fof(f1845,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_97
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f1844]) ).
fof(f1865,plain,
( e2 = op(e3,e4)
| ~ spl0_16 ),
inference(superposition,[],[f464,f670]) ).
fof(f1874,plain,
( $false
| ~ spl0_16
| spl0_49 ),
inference(forward_subsumption_resolution,[],[f1865,f816]) ).
fof(f1875,plain,
( ~ spl0_16
| spl0_49 ),
inference(avatar_contradiction_clause,[],[f1874]) ).
fof(f1879,plain,
( e0 != op(e4,op(e3,e4))
| ~ spl0_19
| spl0_145 ),
inference(forward_demodulation,[],[f1247,f683]) ).
fof(f1881,plain,
( e1 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_49
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f1814,f1028]) ).
fof(f1892,plain,
( e4 = op(e3,e1)
| ~ spl0_55 ),
inference(superposition,[],[f462,f841]) ).
fof(f1905,plain,
( e0 != op(e4,e1)
| ~ spl0_19
| ~ spl0_55
| spl0_145 ),
inference(superposition,[],[f1879,f841]) ).
fof(f1907,plain,
( $false
| ~ spl0_19
| ~ spl0_55
| ~ spl0_115
| spl0_145 ),
inference(forward_subsumption_resolution,[],[f1905,f1107]) ).
fof(f1908,plain,
( ~ spl0_19
| ~ spl0_55
| ~ spl0_115
| spl0_145 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1913,plain,
( $false
| spl0_1
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f1892,f605]) ).
fof(f1914,plain,
( spl0_1
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1913]) ).
fof(f2005,plain,
( op(e0,e0) = e4
| ~ spl0_185 ),
inference(superposition,[],[f322,f1441]) ).
fof(f2013,plain,
( e0 != op(e0,e4)
| ~ spl0_185 ),
inference(superposition,[],[f403,f1441]) ).
fof(f2169,plain,
( e0 = op(e0,e4)
| ~ spl0_185 ),
inference(superposition,[],[f481,f2005]) ).
fof(f2170,plain,
( $false
| ~ spl0_185 ),
inference(forward_subsumption_resolution,[],[f2169,f2013]) ).
fof(f2171,plain,
~ spl0_185,
inference(avatar_contradiction_clause,[],[f2170]) ).
fof(f2172,plain,
( e4 = op(e1,e1)
| ~ spl0_184 ),
inference(superposition,[],[f322,f1437]) ).
fof(f2179,plain,
( e1 != op(e1,e4)
| ~ spl0_184 ),
inference(superposition,[],[f400,f1437]) ).
fof(f2203,plain,
( e1 = op(e1,e4)
| ~ spl0_184 ),
inference(superposition,[],[f475,f2172]) ).
fof(f2205,plain,
( $false
| ~ spl0_184 ),
inference(forward_subsumption_resolution,[],[f2203,f2179]) ).
fof(f2206,plain,
~ spl0_184,
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2209,plain,
( e4 = op(e3,e3)
| ~ spl0_182 ),
inference(superposition,[],[f322,f1429]) ).
fof(f2214,plain,
( e3 != op(e3,e4)
| ~ spl0_182 ),
inference(superposition,[],[f397,f1429]) ).
fof(f2230,plain,
( e3 = op(e3,e4)
| ~ spl0_182 ),
inference(superposition,[],[f463,f2209]) ).
fof(f2231,plain,
( $false
| ~ spl0_182 ),
inference(forward_subsumption_resolution,[],[f2230,f2214]) ).
fof(f2232,plain,
~ spl0_182,
inference(avatar_contradiction_clause,[],[f2231]) ).
fof(f2233,plain,
( e4 = op(e2,e2)
| ~ spl0_183 ),
inference(superposition,[],[f322,f1433]) ).
fof(f2239,plain,
( e2 != op(e2,e4)
| ~ spl0_183 ),
inference(superposition,[],[f398,f1433]) ).
fof(f2252,plain,
( e2 = op(e2,e4)
| ~ spl0_183 ),
inference(superposition,[],[f469,f2233]) ).
fof(f2254,plain,
( $false
| ~ spl0_183 ),
inference(forward_subsumption_resolution,[],[f2252,f2239]) ).
fof(f2255,plain,
~ spl0_183,
inference(avatar_contradiction_clause,[],[f2254]) ).
fof(f2262,plain,
( ~ spl0_64
| ~ spl0_133
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f531,f1070,f1189,f880]) ).
fof(f2302,plain,
( op(e0,e0) != e3
| ~ spl0_64 ),
inference(superposition,[],[f443,f881]) ).
fof(f2304,plain,
( e2 != op(e4,op(e3,e4))
| ~ spl0_64
| spl0_65 ),
inference(superposition,[],[f886,f881]) ).
fof(f2305,plain,
( e1 != op(e3,e4)
| ~ spl0_64
| spl0_66 ),
inference(superposition,[],[f890,f881]) ).
fof(f2309,plain,
( e2 != op(e3,e4)
| ~ spl0_64
| spl0_107 ),
inference(superposition,[],[f1072,f881]) ).
fof(f2334,plain,
( e4 != op(e4,e0)
| ~ spl0_181 ),
inference(superposition,[],[f353,f1425]) ).
fof(f2335,plain,
( e4 != op(e3,e4)
| ~ spl0_181 ),
inference(superposition,[],[f397,f1425]) ).
fof(f2356,plain,
( e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_49
| spl0_55
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f1881,f842]) ).
fof(f2357,plain,
( e3 = op(e3,e4)
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2356,f2335]) ).
fof(f2358,plain,
( e4 = op(e3,op(e4,e3))
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(superposition,[],[f323,f2357]) ).
fof(f2387,plain,
( e4 = op(e3,e0)
| spl0_49
| spl0_55
| ~ spl0_88
| spl0_97
| ~ spl0_181 ),
inference(forward_demodulation,[],[f2358,f987]) ).
fof(f2388,plain,
( $false
| spl0_49
| spl0_55
| spl0_61
| ~ spl0_88
| spl0_97
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2387,f869]) ).
fof(f2389,plain,
( spl0_49
| spl0_55
| spl0_61
| ~ spl0_88
| spl0_97
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f2388]) ).
fof(f2395,plain,
( e0 = op(e3,e4)
| ~ spl0_61 ),
inference(superposition,[],[f466,f868]) ).
fof(f2405,plain,
( $false
| ~ spl0_61
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f2395,f1028]) ).
fof(f2406,plain,
( ~ spl0_61
| spl0_97 ),
inference(avatar_contradiction_clause,[],[f2405]) ).
fof(f2410,plain,
( ~ spl0_55
| ~ spl0_64
| spl0_66 ),
inference(avatar_split_clause,[],[f2305,f888,f880,f840]) ).
fof(f2452,plain,
( e2 != op(e4,e1)
| ~ spl0_55
| ~ spl0_64
| spl0_65 ),
inference(superposition,[],[f2304,f841]) ).
fof(f2461,plain,
( $false
| ~ spl0_10
| ~ spl0_55
| ~ spl0_64
| spl0_65 ),
inference(forward_subsumption_resolution,[],[f2452,f643]) ).
fof(f2462,plain,
( ~ spl0_10
| ~ spl0_55
| ~ spl0_64
| spl0_65 ),
inference(avatar_contradiction_clause,[],[f2461]) ).
fof(f2488,plain,
( e3 = op(op(e4,e3),e0)
| ~ spl0_97 ),
inference(superposition,[],[f327,f1027]) ).
fof(f2516,plain,
( op(e0,e0) = e3
| ~ spl0_88
| ~ spl0_97 ),
inference(forward_demodulation,[],[f2488,f987]) ).
fof(f2518,plain,
( $false
| ~ spl0_64
| ~ spl0_88
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f2516,f2302]) ).
fof(f2519,plain,
( ~ spl0_64
| ~ spl0_88
| ~ spl0_97 ),
inference(avatar_contradiction_clause,[],[f2518]) ).
fof(f2529,plain,
( e0 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f252,f842]) ).
fof(f2530,plain,
( e0 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| spl0_55
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2529,f2335]) ).
fof(f2531,plain,
( ~ spl0_49
| ~ spl0_64
| spl0_107 ),
inference(avatar_split_clause,[],[f2309,f1070,f880,f814]) ).
fof(f2533,plain,
( e1 != op(e4,op(e3,e4))
| ~ spl0_64
| spl0_133 ),
inference(forward_demodulation,[],[f1191,f881]) ).
fof(f2581,plain,
( e1 != op(e4,e2)
| ~ spl0_49
| ~ spl0_64
| spl0_133 ),
inference(superposition,[],[f2533,f815]) ).
fof(f2582,plain,
( $false
| ~ spl0_25
| ~ spl0_49
| ~ spl0_64
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f2581,f709]) ).
fof(f2583,plain,
( ~ spl0_25
| ~ spl0_49
| ~ spl0_64
| spl0_133 ),
inference(avatar_contradiction_clause,[],[f2582]) ).
fof(f2589,plain,
( e3 != op(e4,e0)
| ~ spl0_4 ),
inference(superposition,[],[f356,f617]) ).
fof(f2594,plain,
( e1 = op(e4,e3)
| ~ spl0_4 ),
inference(superposition,[],[f460,f617]) ).
fof(f2595,plain,
( e2 != op(e4,op(e3,e4))
| ~ spl0_4
| spl0_5 ),
inference(superposition,[],[f622,f617]) ).
fof(f2596,plain,
( e0 != op(e3,e4)
| ~ spl0_4
| spl0_6 ),
inference(superposition,[],[f626,f617]) ).
fof(f2600,plain,
( e2 != op(e3,e4)
| ~ spl0_4
| spl0_116 ),
inference(superposition,[],[f1112,f617]) ).
fof(f2605,plain,
( $false
| ~ spl0_4
| ~ spl0_49
| spl0_116 ),
inference(forward_subsumption_resolution,[],[f2600,f815]) ).
fof(f2606,plain,
( ~ spl0_4
| ~ spl0_49
| spl0_116 ),
inference(avatar_contradiction_clause,[],[f2605]) ).
fof(f2608,plain,
( $false
| ~ spl0_4
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f2594,f776]) ).
fof(f2609,plain,
( ~ spl0_4
| spl0_40 ),
inference(avatar_contradiction_clause,[],[f2608]) ).
fof(f2610,plain,
( $false
| ~ spl0_4
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f2589,f881]) ).
fof(f2611,plain,
( ~ spl0_4
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f2610]) ).
fof(f2613,plain,
( e0 != op(e4,op(e3,e4))
| ~ spl0_4
| spl0_139 ),
inference(forward_demodulation,[],[f1219,f617]) ).
fof(f2615,plain,
( e0 != op(e4,e2)
| ~ spl0_4
| ~ spl0_49
| spl0_139 ),
inference(forward_demodulation,[],[f2613,f815]) ).
fof(f2623,plain,
( e1 != op(e4,e0)
| ~ spl0_40 ),
inference(superposition,[],[f354,f775]) ).
fof(f2771,plain,
( e0 = op(e4,e0)
| e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0)
| spl0_106 ),
inference(forward_subsumption_resolution,[],[f251,f1068]) ).
fof(f2772,plain,
( e0 = op(e4,e0)
| e2 = op(e4,e0)
| e4 = op(e4,e0)
| spl0_64
| spl0_106 ),
inference(forward_subsumption_resolution,[],[f2771,f882]) ).
fof(f2773,plain,
( e0 = op(e4,e0)
| e2 = op(e4,e0)
| spl0_64
| spl0_106
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2772,f2334]) ).
fof(f2780,plain,
( e0 = op(e4,e2)
| ~ spl0_70 ),
inference(superposition,[],[f461,f907]) ).
fof(f2794,plain,
( $false
| ~ spl0_70
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f2780,f948]) ).
fof(f2795,plain,
( ~ spl0_70
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f2794]) ).
fof(f2797,plain,
( e0 = op(e4,e0)
| spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2773,f908]) ).
fof(f2799,plain,
( e0 = op(e0,op(e0,e4))
| spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(superposition,[],[f342,f2797]) ).
fof(f2818,plain,
( e0 = e4
| spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(superposition,[],[f2799,f477]) ).
fof(f2822,plain,
( $false
| spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2818,f453]) ).
fof(f2823,plain,
( spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f2822]) ).
fof(f2828,plain,
( ~ spl0_79
| ~ spl0_4
| ~ spl0_49
| spl0_139 ),
inference(avatar_split_clause,[],[f2615,f1217,f814,f616,f946]) ).
fof(f2831,plain,
( ~ spl0_106
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f2623,f774,f1066]) ).
fof(f2889,plain,
( e2 = op(e3,e4)
| e3 = op(e3,e4)
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2530,f1028]) ).
fof(f2890,plain,
( e3 = op(e3,e4)
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2889,f816]) ).
fof(f2894,plain,
( e4 = op(e3,op(e4,e3))
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(superposition,[],[f323,f2890]) ).
fof(f2925,plain,
( e4 = op(e3,e1)
| ~ spl0_40
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(forward_demodulation,[],[f2894,f775]) ).
fof(f2928,plain,
( $false
| spl0_1
| ~ spl0_40
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f2925,f605]) ).
fof(f2929,plain,
( spl0_1
| ~ spl0_40
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f2928]) ).
fof(f2948,plain,
( e1 = op(e3,e4)
| ~ spl0_1 ),
inference(superposition,[],[f465,f604]) ).
fof(f2963,plain,
( $false
| ~ spl0_1
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f2948,f842]) ).
fof(f2964,plain,
( ~ spl0_1
| spl0_55 ),
inference(avatar_contradiction_clause,[],[f2963]) ).
fof(f2968,plain,
( ~ spl0_97
| ~ spl0_4
| spl0_6 ),
inference(avatar_split_clause,[],[f2596,f624,f616,f1026]) ).
fof(f3012,plain,
( e2 != op(e4,e0)
| ~ spl0_4
| spl0_5
| ~ spl0_97 ),
inference(superposition,[],[f2595,f1027]) ).
fof(f3020,plain,
( $false
| ~ spl0_4
| spl0_5
| ~ spl0_70
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f3012,f907]) ).
fof(f3021,plain,
( ~ spl0_4
| spl0_5
| ~ spl0_70
| ~ spl0_97 ),
inference(avatar_contradiction_clause,[],[f3020]) ).
fof(f3036,plain,
( e4 != op(e1,e1)
| ~ spl0_1 ),
inference(superposition,[],[f431,f604]) ).
fof(f3050,plain,
( e4 = op(e1,op(e4,e3))
| ~ spl0_55 ),
inference(superposition,[],[f323,f841]) ).
fof(f3078,plain,
( e4 = op(e1,e1)
| ~ spl0_40
| ~ spl0_55 ),
inference(forward_demodulation,[],[f3050,f775]) ).
fof(f3081,plain,
( $false
| ~ spl0_1
| ~ spl0_40
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3078,f3036]) ).
fof(f3082,plain,
( ~ spl0_1
| ~ spl0_40
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f3081]) ).
cnf(s473,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f627]) ).
cnf(s497,plain,
( ~ spl0_19
| ~ spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f693]) ).
cnf(s569,plain,
( ~ spl0_64
| ~ spl0_65
| ~ spl0_66 ),
inference(sat_conversion,[],[f891]) ).
cnf(s917,plain,
( spl0_181
| spl0_182
| spl0_183
| spl0_184
| spl0_185 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s938,plain,
( spl0_34
| spl0_40
| spl0_88
| ~ spl0_181
| spl0_186 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s963,plain,
~ spl0_186,
inference(sat_conversion,[],[f1486]) ).
cnf(s977,plain,
( spl0_19
| ~ spl0_34 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s996,plain,
( ~ spl0_19
| ~ spl0_80
| ~ spl0_145 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s1016,plain,
( spl0_4
| spl0_10
| spl0_115
| ~ spl0_181
| spl0_187 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s1046,plain,
~ spl0_187,
inference(sat_conversion,[],[f1558]) ).
cnf(s1054,plain,
( ~ spl0_4
| ~ spl0_116
| ~ spl0_139 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s1065,plain,
( ~ spl0_10
| ~ spl0_34 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s1079,plain,
( ~ spl0_10
| spl0_25 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s1116,plain,
( spl0_4
| ~ spl0_40 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s1130,plain,
( spl0_64
| ~ spl0_88 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s1157,plain,
( ~ spl0_88
| ~ spl0_115 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s1196,plain,
( spl0_106
| ~ spl0_115 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s1251,plain,
( ~ spl0_19
| spl0_49
| spl0_55
| spl0_97
| spl0_146
| ~ spl0_181 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s1256,plain,
( ~ spl0_19
| spl0_21
| ~ spl0_97 ),
inference(sat_conversion,[],[f1739]) ).
cnf(s1275,plain,
( ~ spl0_19
| ~ spl0_34
| ~ spl0_49 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s1291,plain,
( spl0_16
| ~ spl0_19
| ~ spl0_34
| ~ spl0_146 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s1299,plain,
( ~ spl0_19
| ~ spl0_55
| spl0_80 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s1309,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_97
| ~ spl0_106 ),
inference(sat_conversion,[],[f1845]) ).
cnf(s1332,plain,
( ~ spl0_16
| spl0_49 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s1347,plain,
( ~ spl0_19
| ~ spl0_55
| ~ spl0_115
| spl0_145 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s1355,plain,
( spl0_1
| ~ spl0_55 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s1576,plain,
~ spl0_185,
inference(sat_conversion,[],[f2171]) ).
cnf(s1633,plain,
~ spl0_184,
inference(sat_conversion,[],[f2206]) ).
cnf(s1656,plain,
~ spl0_182,
inference(sat_conversion,[],[f2232]) ).
cnf(s1668,plain,
~ spl0_183,
inference(sat_conversion,[],[f2255]) ).
cnf(s1682,plain,
( ~ spl0_64
| ~ spl0_107
| ~ spl0_133 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s1775,plain,
( spl0_49
| spl0_55
| spl0_61
| ~ spl0_88
| spl0_97
| ~ spl0_181 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s1784,plain,
( ~ spl0_61
| spl0_97 ),
inference(sat_conversion,[],[f2406]) ).
cnf(s1796,plain,
( ~ spl0_55
| ~ spl0_64
| spl0_66 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s1811,plain,
( ~ spl0_10
| ~ spl0_55
| ~ spl0_64
| spl0_65 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s1859,plain,
( ~ spl0_64
| ~ spl0_88
| ~ spl0_97 ),
inference(sat_conversion,[],[f2519]) ).
cnf(s1887,plain,
( ~ spl0_49
| ~ spl0_64
| spl0_107 ),
inference(sat_conversion,[],[f2531]) ).
cnf(s1929,plain,
( ~ spl0_25
| ~ spl0_49
| ~ spl0_64
| spl0_133 ),
inference(sat_conversion,[],[f2583]) ).
cnf(s1961,plain,
( ~ spl0_4
| ~ spl0_49
| spl0_116 ),
inference(sat_conversion,[],[f2606]) ).
cnf(s1962,plain,
( ~ spl0_4
| spl0_40 ),
inference(sat_conversion,[],[f2609]) ).
cnf(s1965,plain,
( ~ spl0_4
| ~ spl0_64 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s2092,plain,
( ~ spl0_70
| spl0_79 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s2130,plain,
( spl0_64
| spl0_70
| spl0_106
| ~ spl0_181 ),
inference(sat_conversion,[],[f2823]) ).
cnf(s2139,plain,
( ~ spl0_4
| ~ spl0_49
| ~ spl0_79
| spl0_139 ),
inference(sat_conversion,[],[f2828]) ).
cnf(s2148,plain,
( ~ spl0_40
| ~ spl0_106 ),
inference(sat_conversion,[],[f2831]) ).
cnf(s2253,plain,
( spl0_1
| ~ spl0_40
| spl0_49
| spl0_55
| spl0_97
| ~ spl0_181 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s2283,plain,
( ~ spl0_1
| spl0_55 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s2296,plain,
( ~ spl0_4
| spl0_6
| ~ spl0_97 ),
inference(sat_conversion,[],[f2968]) ).
cnf(s2312,plain,
( ~ spl0_4
| spl0_5
| ~ spl0_70
| ~ spl0_97 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s2360,plain,
( ~ spl0_1
| ~ spl0_40
| ~ spl0_55 ),
inference(sat_conversion,[],[f3082]) ).
cnf(s2361,plain,
( spl0_4
| spl0_10
| spl0_115
| ~ spl0_181 ),
inference(rat,[],[s1016,s1046]) ).
cnf(s2362,plain,
( spl0_34
| spl0_40
| spl0_88
| ~ spl0_181 ),
inference(rat,[],[s938,s963]) ).
cnf(s2363,plain,
spl0_181,
inference(rat,[],[s917,s1576,s1633,s1668,s1656]) ).
cnf(s2364,plain,
( ~ spl0_97
| ~ spl0_106
| ~ spl0_19 ),
inference(rat,[],[s497,s1256,s1309]) ).
cnf(s2365,plain,
( ~ spl0_115
| spl0_40
| spl0_55 ),
inference(rat,[],[s2364,s1251,s1291,s1332,s1275,s977,s2362,s1157,s1196,s2363]) ).
cnf(s2366,plain,
( ~ spl0_49
| ~ spl0_64
| ~ spl0_25 ),
inference(rat,[],[s1682,s1887,s1929]) ).
cnf(s2367,plain,
( spl0_4
| spl0_55 ),
inference(rat,[],[s2366,s1775,s1784,s1859,s1130,s2362,s1065,s1079,s2361,s2365,s1116,s2363]) ).
cnf(s2368,plain,
( ~ spl0_97
| ~ spl0_4 ),
inference(rat,[],[s473,s2312,s2296,s2130,s2148,s1962,s1965,s2363]) ).
cnf(s2369,plain,
( ~ spl0_49
| ~ spl0_79
| ~ spl0_4 ),
inference(rat,[],[s1054,s1961,s2139]) ).
cnf(s2370,plain,
spl0_1,
inference(rat,[],[s2369,s2253,s2368,s2092,s2130,s2148,s1962,s1965,s2367,s1355,s2363]) ).
cnf(s2372,plain,
spl0_55,
inference(rat,[],[s2283,s2370]) ).
cnf(s2375,plain,
~ spl0_40,
inference(rat,[],[s2360,s2370,s2372]) ).
cnf(s2377,plain,
~ spl0_4,
inference(rat,[],[s1962,s2375]) ).
cnf(s2378,plain,
~ spl0_88,
inference(rat,[],[s569,s1811,s1796,s2361,s1130,s1157,s2372,s2377,s2363]) ).
cnf(s2379,plain,
spl0_34,
inference(rat,[],[s2362,s2363,s2375,s2378]) ).
cnf(s2384,plain,
~ spl0_10,
inference(rat,[],[s1065,s2379]) ).
cnf(s2385,plain,
spl0_19,
inference(rat,[],[s977,s2379]) ).
cnf(s2392,plain,
spl0_115,
inference(rat,[],[s2361,s2363,s2377,s2384]) ).
cnf(s2393,plain,
spl0_80,
inference(rat,[],[s1299,s2372,s2385]) ).
cnf(s2405,plain,
spl0_145,
inference(rat,[],[s1347,s2385,s2372,s2392]) ).
cnf(s2406,plain,
$false,
inference(rat,[],[s996,s2385,s2405,s2393]) ).
fof(f3083,plain,
$false,
inference(avatar_sat_refutation,[],[s2406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG192+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.19 % Computer : n015.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Mon Sep 28 19:44:32 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.22 Running first-order model finding
% 0.06/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.37 % (2939422)Will run a generic schedule for satisfiability detection.
% 0.82/0.37 % (2939431)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=503449862:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.82/0.37 % (2939428)% WARNING: option uhcvi not known.
% 0.82/0.37 % (2939427)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3389090286_2999 on theBenchmark for (2999ds/0Mi)
% 0.82/0.37 % (2939428)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2729140710:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.82/0.37 % (2939429)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2697251829:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.82/0.37 % (2939432)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=956946115:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.82/0.37 % (2939433)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3194915249:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.82/0.37 % (2939430)dis+10_1_sil=32000:sp=arity:random_seed=1030174409:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.82/0.37 % (2939431)Instruction limit reached!
% 0.82/0.37 % (2939431)------------------------------
% 0.82/0.37 % (2939431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.37 % (2939431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.37 % (2939431)CaDiCaL version: 2.1.3
% 0.82/0.37 % (2939431)Termination reason: Instruction limit
% 0.82/0.37 % (2939431)Termination phase: Saturation
% 0.82/0.37 % (2939431)Time elapsed: 0.032 s
% 0.82/0.37 % (2939431)Peak memory usage: 13 MB
% 0.82/0.37 % (2939431)Instructions burned: 117 (million)
% 0.82/0.37 % Detected minimum model sizes of [5]
% 0.82/0.37 % Detected maximum model sizes of [max]
% 0.82/0.37 % TRYING [5]
% 0.82/0.37 % (2939441)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=347478094:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.82/0.37 % Detected minimum model sizes of [5]
% 0.82/0.37 % Detected maximum model sizes of [max]
% 0.82/0.37 % TRYING [5]
% 0.82/0.37 % TRYING [6]
% 0.82/0.37 % (2939432)Instruction limit reached!
% 0.82/0.37 % (2939432)------------------------------
% 0.82/0.37 % (2939432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.37 % (2939432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.37 % (2939432)CaDiCaL version: 2.1.3
% 0.82/0.37 % (2939432)Termination reason: Instruction limit
% 0.82/0.37 % (2939432)Termination phase: Saturation
% 0.82/0.37 % (2939432)Time elapsed: 0.064 s
% 0.82/0.37 % (2939432)Peak memory usage: 13 MB
% 0.82/0.37 % (2939432)Instructions burned: 131 (million)
% 0.82/0.37 % TRYING [6]
% 0.82/0.37 % (2939429) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2939422-2939429"...
% 0.82/0.37 % (2939429)...printing done.
% 0.82/0.37 % (2939433)Instruction limit reached!
% 0.82/0.37 % (2939433)------------------------------
% 0.82/0.37 % (2939433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.37 % (2939433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.37 % (2939433)CaDiCaL version: 2.1.3
% 0.82/0.37 % (2939433)Termination reason: Instruction limit
% 0.82/0.37 % (2939433)Termination phase: Saturation
% 0.82/0.37 % (2939433)Time elapsed: 0.083 s
% 0.82/0.37 % (2939433)Peak memory usage: 13 MB
% 0.82/0.37 % (2939433)Instructions burned: 162 (million)
% 0.82/0.37 % (2939429)Refutation found. Thanks to Tanya!
% 0.82/0.37 % SZS status Unsatisfiable for theBenchmark
% 0.82/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.82/0.38 % (2939429)------------------------------
% 0.82/0.38 % (2939429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.38 % (2939429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.38 % (2939429)CaDiCaL version: 2.1.3
% 0.82/0.38 % (2939429)Termination reason: Refutation
% 0.82/0.38 % (2939429)Time elapsed: 0.082 s
% 0.82/0.38 % (2939429)Peak memory usage: 14 MB
% 0.82/0.38 % (2939429)Instructions burned: 145 (million)
% 0.82/0.38 % (2939422)Success in time 0.138 s
% 0.82/0.38 % Vampire exiting
%------------------------------------------------------------------------------