%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG139+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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:24:35 AM UTC 2026
% Result : Unsatisfiable 0.18s 0.29s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 97
% Syntax : Number of formulae : 846 ( 38 unt; 79 def)
% Number of atoms : 2469 ( 787 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 2906 (1283 ~;1414 |; 130 &)
% ( 79 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 81 ( 79 usr; 80 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) != e3 ) )
& ( ( op(e0,e0) = e1
& op(e1,e1) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e2) = e1
& op(e1,e1) != e2 )
| ( op(e3,e3) = e1
& op(e1,e1) != e3 ) )
& ( ( op(e0,e0) = e2
& op(e2,e2) != e0 )
| ( op(e1,e1) = e2
& op(e2,e2) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e3,e3) = e2
& op(e2,e2) != e3 ) )
& ( ( op(e0,e0) = e3
& op(e3,e3) != e0 )
| ( op(e1,e1) = e3
& op(e3,e3) != e1 )
| ( op(e2,e2) = e3
& op(e3,e3) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f7,axiom,
~ ( e0 = op(op(e3,e3),e3)
& e1 = op(op(e3,e3),op(e3,e3))
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
~ ( e0 = op(op(e1,e1),e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
~ ( e0 = op(op(e3,e3),e3)
& e2 = op(op(e3,e3),op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
~ ( e0 = op(op(e1,e1),e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(op(e2,e2),e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f16,axiom,
~ ( e1 = op(op(e0,e0),e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(op(e2,e2),e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e0 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f20,axiom,
~ ( e2 = op(op(e0,e0),e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e3 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f22,axiom,
~ ( e2 = op(op(e0,e0),e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(op(e1,e1),e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f25,axiom,
~ ( e3 = op(op(e2,e2),e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(op(e0,e0),e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f28,axiom,
~ ( e3 = op(op(e0,e0),e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
~ ( e3 = op(op(e1,e1),e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
fof(f31,plain,
( e0 != op(op(e3,e3),e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e2 != op(e3,e3) ),
inference(ennf_transformation,[],[f7]) ).
fof(f32,plain,
( e0 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f33,plain,
( e0 != op(op(e3,e3),e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
( e0 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f40,plain,
( e1 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( e1 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f44,plain,
( e2 != op(op(e0,e0),e0)
| e1 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e3 ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
( e2 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e3 != op(op(e2,e2),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f50,plain,
( e3 != op(op(e0,e0),e0)
| e1 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f26]) ).
fof(f52,plain,
( e3 != op(op(e0,e0),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f28]) ).
fof(f53,plain,
( e3 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f71,plain,
( e0 = op(e3,e0)
| e0 = op(e2,e0)
| e0 = op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
( e1 = op(e3,e0)
| e1 = op(e2,e0)
| e1 = op(e1,e0)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
( e3 = op(e0,e3)
| e3 = op(e0,e2)
| e3 = op(e0,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e0 = op(e1,e3)
| e0 = op(e1,e2)
| e0 = op(e1,e1)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
( e1 = op(e1,e3)
| e1 = op(e1,e2)
| e1 = op(e1,e1)
| e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( e0 = op(e3,e2)
| e0 = op(e2,e2)
| e0 = op(e1,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e1 = op(e3,e2)
| e1 = op(e2,e2)
| e1 = op(e1,e2)
| e1 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e2 = op(e2,e3)
| e2 = op(e2,e2)
| e2 = op(e2,e1)
| e2 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| e3 = op(e3,e1)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f103,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f105,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f106,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
( e0 = op(e3,e3)
| op(e0,e0) != e2
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e1 = op(e3,e3)
| e2 != op(e1,e1)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 != op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( e3 != op(e1,e1)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f189,plain,
( e2 = op(e3,e3)
| e2 != op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f193,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
( e3 = op(e3,e3)
| e2 != op(e3,e3)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f209,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e1 != op(e3,e3)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f217,plain,
( e3 != op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f221,plain,
( e2 != op(e3,e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(e3,e3),e3) ),
inference(cnf_transformation,[],[f31]) ).
fof(f222,plain,
( e3 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(e1,e1),e1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f223,plain,
( e1 != op(e3,e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(e3,e3),e3) ),
inference(cnf_transformation,[],[f33]) ).
fof(f224,plain,
( e2 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(e1,e1),e1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f225,plain,
( e1 != op(e2,e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(e2,e2),e2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f230,plain,
( op(e0,e0) != e2
| e3 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f231,plain,
( e0 != op(e2,e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(op(e2,e2),e2) ),
inference(cnf_transformation,[],[f41]) ).
fof(f234,plain,
( op(e0,e0) != e3
| e1 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f236,plain,
( op(e0,e0) != e1
| e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f237,plain,
( e0 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(e1,e1),e1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f239,plain,
( e1 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(e2,e2),e2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f240,plain,
( op(e0,e0) != e2
| e1 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f242,plain,
( op(e0,e0) != e1
| e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f243,plain,
( e0 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(e1,e1),e1) ),
inference(cnf_transformation,[],[f53]) ).
fof(f245,definition,
( spl0_1
<=> e3 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f247,plain,
( e3 != op(op(e1,e1),e1)
| spl0_1 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f249,definition,
( spl0_2
<=> e2 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f250,plain,
( e2 = op(op(e1,e1),op(e1,e1))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| spl0_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,definition,
( spl0_3
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f254,plain,
( e0 = op(e1,e1)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f243,f253,f249,f245]) ).
fof(f258,definition,
( spl0_4
<=> e3 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f260,plain,
( e3 != op(op(e0,e0),e0)
| spl0_4 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f262,definition,
( spl0_5
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f264,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl0_5 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,definition,
( spl0_6
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f267,plain,
( op(e0,e0) = e1
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f269,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f242,f266,f262,f258]) ).
fof(f271,definition,
( spl0_7
<=> e3 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f273,plain,
( e3 != op(op(e2,e2),e2)
| spl0_7 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f279,definition,
( spl0_9
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f280,plain,
( e0 = op(e2,e2)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f284,definition,
( spl0_10
<=> e1 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f286,plain,
( e1 != op(op(e0,e0),op(e0,e0))
| spl0_10 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl0_11
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f289,plain,
( op(e0,e0) = e2
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f240,f288,f284,f258]) ).
fof(f293,definition,
( spl0_12
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f294,plain,
( e0 = op(op(e2,e2),op(e2,e2))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl0_12 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl0_13
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f298,plain,
( e1 = op(e2,e2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f300,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f239,f297,f293,f271]) ).
fof(f306,definition,
( spl0_15
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f307,plain,
( e2 = op(e1,e1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f311,definition,
( spl0_16
<=> e2 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f313,plain,
( e2 != op(op(e1,e1),e1)
| spl0_16 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl0_17
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f317,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl0_17 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f237,f253,f315,f311]) ).
fof(f320,definition,
( spl0_18
<=> e2 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f322,plain,
( e2 != op(op(e0,e0),e0)
| spl0_18 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl0_19
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f326,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl0_19 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f327,plain,
( ~ spl0_18
| ~ spl0_19
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f236,f266,f324,f320]) ).
fof(f333,definition,
( spl0_21
<=> e1 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f335,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| spl0_21 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f337,definition,
( spl0_22
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f338,plain,
( e0 = op(e3,e3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f342,definition,
( spl0_23
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f343,plain,
( op(e0,e0) = e3
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( ~ spl0_18
| ~ spl0_10
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f234,f342,f284,f320]) ).
fof(f351,definition,
( spl0_25
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f352,plain,
( e1 = op(e3,e3)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f356,definition,
( spl0_26
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f357,plain,
( e3 = op(e1,e1)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f361,definition,
( spl0_27
<=> e1 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f363,plain,
( e1 != op(op(e2,e2),e2)
| spl0_27 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f365,definition,
( spl0_28
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f366,plain,
( e3 = op(op(e2,e2),op(e2,e2))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl0_28 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,plain,
( ~ spl0_27
| ~ spl0_28
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f231,f279,f365,f361]) ).
fof(f370,definition,
( spl0_29
<=> e1 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f372,plain,
( e1 != op(op(e0,e0),e0)
| spl0_29 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( ~ spl0_29
| ~ spl0_19
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f230,f288,f324,f370]) ).
fof(f379,definition,
( spl0_31
<=> e2 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f381,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| spl0_31 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f385,definition,
( spl0_32
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f386,plain,
( e2 = op(e3,e3)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f390,definition,
( spl0_33
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f391,plain,
( e3 = op(e2,e2)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f395,definition,
( spl0_34
<=> e0 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f397,plain,
( e0 != op(op(e2,e2),e2)
| spl0_34 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,plain,
( ~ spl0_34
| ~ spl0_28
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f225,f297,f365,f395]) ).
fof(f400,definition,
( spl0_35
<=> e0 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f402,plain,
( e0 != op(op(e1,e1),e1)
| spl0_35 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f403,plain,
( ~ spl0_35
| ~ spl0_17
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f224,f306,f315,f400]) ).
fof(f405,definition,
( spl0_36
<=> e0 = op(op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f407,plain,
( e0 != op(op(e3,e3),e3)
| spl0_36 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f408,plain,
( ~ spl0_36
| ~ spl0_31
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f223,f351,f379,f405]) ).
fof(f409,plain,
( ~ spl0_35
| ~ spl0_2
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f222,f356,f249,f400]) ).
fof(f410,plain,
( ~ spl0_36
| ~ spl0_21
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f221,f385,f333,f405]) ).
fof(f413,definition,
( spl0_37
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f414,plain,
( e0 = op(e0,e0)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,plain,
( spl0_37
| spl0_3
| ~ spl0_11
| spl0_22 ),
inference(avatar_split_clause,[],[f157,f337,f288,f253,f413]) ).
fof(f420,plain,
( ~ spl0_37
| spl0_3
| spl0_9
| spl0_22 ),
inference(avatar_split_clause,[],[f160,f337,f279,f253,f413]) ).
fof(f421,plain,
( spl0_37
| spl0_3
| spl0_9
| spl0_22 ),
inference(avatar_split_clause,[],[f161,f337,f279,f253,f413]) ).
fof(f433,definition,
( spl0_38
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f435,plain,
( e1 = op(e1,e1)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f437,plain,
( spl0_6
| spl0_38
| ~ spl0_15
| spl0_25 ),
inference(avatar_split_clause,[],[f173,f351,f306,f433,f266]) ).
fof(f440,plain,
( ~ spl0_3
| spl0_38
| spl0_13
| spl0_25 ),
inference(avatar_split_clause,[],[f176,f351,f297,f433,f253]) ).
fof(f441,plain,
( spl0_6
| spl0_38
| spl0_13
| spl0_25 ),
inference(avatar_split_clause,[],[f177,f351,f297,f433,f266]) ).
fof(f443,plain,
( spl0_6
| ~ spl0_38
| spl0_13
| spl0_25 ),
inference(avatar_split_clause,[],[f179,f351,f297,f433,f266]) ).
fof(f448,plain,
( ~ spl0_3
| spl0_38
| spl0_13
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f184,f356,f297,f433,f253]) ).
fof(f453,definition,
( spl0_39
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f454,plain,
( e2 = op(e2,e2)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f457,plain,
( spl0_11
| spl0_15
| ~ spl0_39
| spl0_32 ),
inference(avatar_split_clause,[],[f189,f385,f453,f306,f288]) ).
fof(f460,plain,
( ~ spl0_9
| spl0_15
| spl0_39
| spl0_32 ),
inference(avatar_split_clause,[],[f192,f385,f453,f306,f279]) ).
fof(f461,plain,
( spl0_11
| spl0_15
| spl0_39
| spl0_32 ),
inference(avatar_split_clause,[],[f193,f385,f453,f306,f288]) ).
fof(f473,definition,
( spl0_40
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f475,plain,
( e3 = op(e3,e3)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f477,plain,
( spl0_23
| spl0_26
| ~ spl0_32
| spl0_40 ),
inference(avatar_split_clause,[],[f205,f473,f385,f356,f342]) ).
fof(f480,plain,
( ~ spl0_22
| spl0_26
| spl0_33
| spl0_40 ),
inference(avatar_split_clause,[],[f208,f473,f390,f356,f337]) ).
fof(f481,plain,
( spl0_23
| spl0_26
| spl0_33
| spl0_40 ),
inference(avatar_split_clause,[],[f209,f473,f390,f356,f342]) ).
fof(f483,plain,
( spl0_23
| ~ spl0_25
| spl0_33
| spl0_40 ),
inference(avatar_split_clause,[],[f211,f473,f390,f351,f342]) ).
fof(f489,plain,
( spl0_23
| spl0_26
| spl0_33
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f217,f473,f390,f356,f342]) ).
fof(f493,definition,
( spl0_41
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f495,plain,
( e0 = op(e0,e1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl0_42
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f499,plain,
( e0 = op(e0,e2)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f506,definition,
( spl0_44
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f508,plain,
( e0 = op(e1,e0)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f510,definition,
( spl0_45
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f512,plain,
( e0 = op(e2,e0)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl0_46
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f516,plain,
( e0 = op(e3,e0)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,plain,
( spl0_37
| spl0_44
| spl0_45
| spl0_46 ),
inference(avatar_split_clause,[],[f71,f514,f510,f506,f413]) ).
fof(f523,definition,
( spl0_48
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f525,plain,
( e1 = op(e0,e2)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl0_49
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f529,plain,
( e1 = op(e0,e3)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f532,definition,
( spl0_50
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f534,plain,
( e1 = op(e1,e0)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f536,definition,
( spl0_51
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f538,plain,
( e1 = op(e2,e0)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f540,definition,
( spl0_52
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f542,plain,
( e1 = op(e3,e0)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f543,plain,
( spl0_6
| spl0_50
| spl0_51
| spl0_52 ),
inference(avatar_split_clause,[],[f73,f540,f536,f532,f266]) ).
fof(f545,definition,
( spl0_53
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f547,plain,
( e2 = op(e0,e1)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f549,definition,
( spl0_54
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f551,plain,
( e2 = op(e0,e2)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f553,definition,
( spl0_55
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f555,plain,
( e2 = op(e0,e3)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f556,plain,
( spl0_11
| spl0_53
| spl0_54
| spl0_55 ),
inference(avatar_split_clause,[],[f74,f553,f549,f545,f288]) ).
fof(f558,definition,
( spl0_56
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e1,e0)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl0_57
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f564,plain,
( e2 = op(e2,e0)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl0_58
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f568,plain,
( e2 = op(e3,e0)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( spl0_11
| spl0_56
| spl0_57
| spl0_58 ),
inference(avatar_split_clause,[],[f75,f566,f562,f558,f288]) ).
fof(f571,definition,
( spl0_59
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f573,plain,
( e3 = op(e0,e1)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl0_60
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f577,plain,
( e3 = op(e0,e2)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl0_61
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f581,plain,
( e3 = op(e0,e3)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f582,plain,
( spl0_23
| spl0_59
| spl0_60
| spl0_61 ),
inference(avatar_split_clause,[],[f76,f579,f575,f571,f342]) ).
fof(f584,definition,
( spl0_62
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f586,plain,
( e3 = op(e1,e0)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f588,definition,
( spl0_63
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f590,plain,
( e3 = op(e2,e0)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,definition,
( spl0_64
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f594,plain,
( e3 = op(e3,e0)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f595,plain,
( spl0_23
| spl0_62
| spl0_63
| spl0_64 ),
inference(avatar_split_clause,[],[f77,f592,f588,f584,f342]) ).
fof(f597,definition,
( spl0_65
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f599,plain,
( e0 = op(e1,e2)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl0_66
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f603,plain,
( e0 = op(e1,e3)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f604,plain,
( spl0_44
| spl0_3
| spl0_65
| spl0_66 ),
inference(avatar_split_clause,[],[f78,f601,f597,f253,f506]) ).
fof(f606,definition,
( spl0_67
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f608,plain,
( e0 = op(e2,e1)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f610,definition,
( spl0_68
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f612,plain,
( e0 = op(e3,e1)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
( spl0_41
| spl0_3
| spl0_67
| spl0_68 ),
inference(avatar_split_clause,[],[f79,f610,f606,f253,f493]) ).
fof(f615,definition,
( spl0_69
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f617,plain,
( e1 = op(e1,e2)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl0_70
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f621,plain,
( e1 = op(e1,e3)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f622,plain,
( spl0_50
| spl0_38
| spl0_69
| spl0_70 ),
inference(avatar_split_clause,[],[f80,f619,f615,f433,f532]) ).
fof(f624,definition,
( spl0_71
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f626,plain,
( e1 = op(e2,e1)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f633,definition,
( spl0_73
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f635,plain,
( e2 = op(e1,e2)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl0_74
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f639,plain,
( e2 = op(e1,e3)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,plain,
( spl0_56
| spl0_15
| spl0_73
| spl0_74 ),
inference(avatar_split_clause,[],[f82,f637,f633,f306,f558]) ).
fof(f642,definition,
( spl0_75
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f644,plain,
( e2 = op(e2,e1)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl0_76
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f648,plain,
( e2 = op(e3,e1)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f649,plain,
( spl0_53
| spl0_15
| spl0_75
| spl0_76 ),
inference(avatar_split_clause,[],[f83,f646,f642,f306,f545]) ).
fof(f651,definition,
( spl0_77
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f653,plain,
( e3 = op(e1,e2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f655,definition,
( spl0_78
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f657,plain,
( e3 = op(e1,e3)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f658,plain,
( spl0_62
| spl0_26
| spl0_77
| spl0_78 ),
inference(avatar_split_clause,[],[f84,f655,f651,f356,f584]) ).
fof(f660,definition,
( spl0_79
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f662,plain,
( e3 = op(e2,e1)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f664,definition,
( spl0_80
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f666,plain,
( e3 = op(e3,e1)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
( spl0_59
| spl0_26
| spl0_79
| spl0_80 ),
inference(avatar_split_clause,[],[f85,f664,f660,f356,f571]) ).
fof(f669,definition,
( spl0_81
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f671,plain,
( e0 = op(e2,e3)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( spl0_45
| spl0_67
| spl0_9
| spl0_81 ),
inference(avatar_split_clause,[],[f86,f669,f279,f606,f510]) ).
fof(f674,definition,
( spl0_82
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f676,plain,
( e0 = op(e3,e2)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f677,plain,
( spl0_42
| spl0_65
| spl0_9
| spl0_82 ),
inference(avatar_split_clause,[],[f87,f674,f279,f597,f497]) ).
fof(f679,definition,
( spl0_83
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f681,plain,
( e1 = op(e2,e3)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl0_51
| spl0_71
| spl0_13
| spl0_83 ),
inference(avatar_split_clause,[],[f88,f679,f297,f624,f536]) ).
fof(f684,definition,
( spl0_84
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f686,plain,
( e1 = op(e3,e2)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f687,plain,
( spl0_48
| spl0_69
| spl0_13
| spl0_84 ),
inference(avatar_split_clause,[],[f89,f684,f297,f615,f523]) ).
fof(f689,definition,
( spl0_85
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f691,plain,
( e2 = op(e2,e3)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f692,plain,
( spl0_57
| spl0_75
| spl0_39
| spl0_85 ),
inference(avatar_split_clause,[],[f90,f689,f453,f642,f562]) ).
fof(f694,definition,
( spl0_86
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f696,plain,
( e2 = op(e3,e2)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f694]) ).
fof(f704,definition,
( spl0_88
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f706,plain,
( e3 = op(e3,e2)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f707,plain,
( spl0_60
| spl0_77
| spl0_33
| spl0_88 ),
inference(avatar_split_clause,[],[f93,f704,f390,f651,f575]) ).
fof(f708,plain,
( spl0_46
| spl0_68
| spl0_82
| spl0_22 ),
inference(avatar_split_clause,[],[f94,f337,f674,f610,f514]) ).
fof(f711,plain,
( spl0_49
| spl0_70
| spl0_83
| spl0_25 ),
inference(avatar_split_clause,[],[f97,f351,f679,f619,f527]) ).
fof(f712,plain,
( spl0_58
| spl0_76
| spl0_86
| spl0_32 ),
inference(avatar_split_clause,[],[f98,f385,f694,f646,f566]) ).
fof(f713,plain,
( spl0_55
| spl0_74
| spl0_85
| spl0_32 ),
inference(avatar_split_clause,[],[f99,f385,f689,f637,f553]) ).
fof(f714,plain,
( spl0_64
| spl0_80
| spl0_88
| spl0_40 ),
inference(avatar_split_clause,[],[f100,f473,f704,f664,f592]) ).
fof(f734,plain,
( e2 != op(e1,e0)
| ~ spl0_6
| spl0_18 ),
inference(forward_demodulation,[],[f322,f267]) ).
fof(f735,plain,
( e1 = e3
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_demodulation,[],[f343,f267]) ).
fof(f736,plain,
( e2 = e3
| ~ spl0_15
| ~ spl0_26 ),
inference(forward_demodulation,[],[f357,f307]) ).
fof(f737,plain,
( e1 != op(e0,e2)
| ~ spl0_9
| spl0_27 ),
inference(forward_demodulation,[],[f363,f280]) ).
fof(f738,plain,
( e1 = e2
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f386,f352]) ).
fof(f739,plain,
( e0 = e3
| ~ spl0_9
| ~ spl0_33 ),
inference(forward_demodulation,[],[f391,f280]) ).
fof(f740,plain,
( e0 != op(e2,e1)
| ~ spl0_15
| spl0_35 ),
inference(forward_demodulation,[],[f402,f307]) ).
fof(f741,plain,
( e0 != op(e1,e3)
| ~ spl0_25
| spl0_36 ),
inference(forward_demodulation,[],[f407,f352]) ).
fof(f742,plain,
( e0 = e2
| ~ spl0_9
| ~ spl0_39 ),
inference(forward_demodulation,[],[f454,f280]) ).
fof(f743,plain,
( e1 = e3
| ~ spl0_25
| ~ spl0_40 ),
inference(forward_demodulation,[],[f475,f352]) ).
fof(f744,plain,
( e0 = e2
| ~ spl0_44
| ~ spl0_56 ),
inference(forward_demodulation,[],[f560,f508]) ).
fof(f746,plain,
( $false
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f735,f151]) ).
fof(f747,plain,
( ~ spl0_6
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f746]) ).
fof(f748,plain,
( $false
| ~ spl0_15
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f736,f150]) ).
fof(f749,plain,
( ~ spl0_15
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f748]) ).
fof(f750,plain,
( $false
| ~ spl0_9
| spl0_27
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f737,f525]) ).
fof(f751,plain,
( ~ spl0_9
| spl0_27
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f750]) ).
fof(f752,plain,
( $false
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f738,f152]) ).
fof(f753,plain,
( ~ spl0_25
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f752]) ).
fof(f754,plain,
( $false
| ~ spl0_9
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f739,f153]) ).
fof(f755,plain,
( ~ spl0_9
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f754]) ).
fof(f760,plain,
( $false
| ~ spl0_9
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f742,f154]) ).
fof(f761,plain,
( ~ spl0_9
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f760]) ).
fof(f762,plain,
( $false
| ~ spl0_25
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f743,f151]) ).
fof(f763,plain,
( ~ spl0_25
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f762]) ).
fof(f764,plain,
( $false
| ~ spl0_44
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f744,f154]) ).
fof(f765,plain,
( ~ spl0_44
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f764]) ).
fof(f766,plain,
( e3 != op(e2,e2)
| ~ spl0_15
| spl0_17 ),
inference(forward_demodulation,[],[f317,f307]) ).
fof(f774,plain,
( e0 = e3
| ~ spl0_41
| ~ spl0_59 ),
inference(forward_demodulation,[],[f573,f495]) ).
fof(f776,plain,
( e0 = e1
| ~ spl0_82
| ~ spl0_84 ),
inference(forward_demodulation,[],[f686,f676]) ).
fof(f777,plain,
( e0 = e2
| ~ spl0_81
| ~ spl0_85 ),
inference(forward_demodulation,[],[f691,f671]) ).
fof(f781,plain,
( e0 = e3
| ~ spl0_22
| ~ spl0_40 ),
inference(forward_demodulation,[],[f475,f338]) ).
fof(f782,plain,
( $false
| ~ spl0_15
| spl0_17
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f766,f391]) ).
fof(f783,plain,
( ~ spl0_15
| spl0_17
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f782]) ).
fof(f788,plain,
( $false
| ~ spl0_41
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f774,f153]) ).
fof(f789,plain,
( ~ spl0_41
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f788]) ).
fof(f792,plain,
( $false
| ~ spl0_82
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f776,f155]) ).
fof(f793,plain,
( ~ spl0_82
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f794,plain,
( $false
| ~ spl0_81
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f777,f154]) ).
fof(f795,plain,
( ~ spl0_81
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f794]) ).
fof(f797,plain,
( $false
| ~ spl0_22
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f781,f153]) ).
fof(f798,plain,
( ~ spl0_22
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f801,plain,
( e3 != op(e1,e1)
| ~ spl0_6
| spl0_19 ),
inference(forward_demodulation,[],[f326,f267]) ).
fof(f803,plain,
( ~ spl0_67
| ~ spl0_15
| spl0_35 ),
inference(avatar_split_clause,[],[f740,f400,f306,f606]) ).
fof(f808,plain,
( e1 = e3
| ~ spl0_48
| ~ spl0_60 ),
inference(forward_demodulation,[],[f577,f525]) ).
fof(f811,plain,
( e2 = e3
| ~ spl0_86
| ~ spl0_88 ),
inference(forward_demodulation,[],[f706,f696]) ).
fof(f812,plain,
( e1 = e2
| ~ spl0_83
| ~ spl0_85 ),
inference(forward_demodulation,[],[f691,f681]) ).
fof(f815,plain,
( $false
| ~ spl0_48
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f808,f151]) ).
fof(f816,plain,
( ~ spl0_48
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f815]) ).
fof(f819,plain,
( $false
| ~ spl0_86
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f811,f150]) ).
fof(f820,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f819]) ).
fof(f821,plain,
( $false
| ~ spl0_83
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f812,f152]) ).
fof(f822,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f821]) ).
fof(f823,plain,
( e0 = e1
| ~ spl0_22
| ~ spl0_25 ),
inference(forward_demodulation,[],[f352,f338]) ).
fof(f827,plain,
( e2 = e3
| ~ spl0_55
| ~ spl0_61 ),
inference(forward_demodulation,[],[f581,f555]) ).
fof(f829,plain,
( e0 = e3
| ~ spl0_68
| ~ spl0_80 ),
inference(forward_demodulation,[],[f666,f612]) ).
fof(f831,plain,
( $false
| ~ spl0_22
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f823,f155]) ).
fof(f832,plain,
( ~ spl0_22
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f831]) ).
fof(f835,plain,
( $false
| ~ spl0_55
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f827,f150]) ).
fof(f836,plain,
( ~ spl0_55
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f835]) ).
fof(f837,plain,
( $false
| ~ spl0_68
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f829,f153]) ).
fof(f838,plain,
( ~ spl0_68
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f837]) ).
fof(f844,plain,
( e1 = e3
| ~ spl0_70
| ~ spl0_78 ),
inference(forward_demodulation,[],[f657,f621]) ).
fof(f850,plain,
( $false
| ~ spl0_70
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f844,f151]) ).
fof(f851,plain,
( ~ spl0_70
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f850]) ).
fof(f858,plain,
( e0 = e1
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_demodulation,[],[f617,f599]) ).
fof(f863,plain,
( $false
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f858,f155]) ).
fof(f864,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f863]) ).
fof(f865,plain,
( e0 = e1
| ~ spl0_66
| ~ spl0_70 ),
inference(forward_demodulation,[],[f621,f603]) ).
fof(f871,plain,
( $false
| ~ spl0_66
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f865,f155]) ).
fof(f872,plain,
( ~ spl0_66
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f871]) ).
fof(f876,plain,
( e1 = e2
| ~ spl0_69
| ~ spl0_73 ),
inference(forward_demodulation,[],[f635,f617]) ).
fof(f881,plain,
( $false
| ~ spl0_69
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f876,f152]) ).
fof(f882,plain,
( ~ spl0_69
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f881]) ).
fof(f885,plain,
( e0 = e3
| ~ spl0_46
| ~ spl0_64 ),
inference(forward_demodulation,[],[f594,f516]) ).
fof(f889,plain,
( e0 = e2
| ~ spl0_65
| ~ spl0_73 ),
inference(forward_demodulation,[],[f635,f599]) ).
fof(f891,plain,
( $false
| ~ spl0_46
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f885,f153]) ).
fof(f892,plain,
( ~ spl0_46
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f891]) ).
fof(f893,plain,
( $false
| ~ spl0_65
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f889,f154]) ).
fof(f894,plain,
( ~ spl0_65
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f893]) ).
fof(f896,plain,
( e1 = e2
| ~ spl0_84
| ~ spl0_86 ),
inference(forward_demodulation,[],[f696,f686]) ).
fof(f897,plain,
( $false
| ~ spl0_84
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f896,f152]) ).
fof(f898,plain,
( ~ spl0_84
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f897]) ).
fof(f903,plain,
( e1 = e2
| ~ spl0_15
| ~ spl0_38 ),
inference(superposition,[],[f435,f307]) ).
fof(f908,plain,
( $false
| ~ spl0_15
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f903,f152]) ).
fof(f909,plain,
( ~ spl0_15
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f908]) ).
fof(f911,plain,
( e2 = e3
| ~ spl0_33
| ~ spl0_39 ),
inference(superposition,[],[f454,f391]) ).
fof(f917,plain,
( $false
| ~ spl0_33
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f911,f150]) ).
fof(f918,plain,
( ~ spl0_33
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f917]) ).
fof(f921,plain,
( e1 = e2
| ~ spl0_51
| ~ spl0_57 ),
inference(forward_demodulation,[],[f564,f538]) ).
fof(f923,plain,
( e0 = e2
| ~ spl0_82
| ~ spl0_86 ),
inference(forward_demodulation,[],[f696,f676]) ).
fof(f927,plain,
( $false
| ~ spl0_51
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f921,f152]) ).
fof(f928,plain,
( ~ spl0_51
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f927]) ).
fof(f929,plain,
( $false
| ~ spl0_82
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f923,f154]) ).
fof(f930,plain,
( ~ spl0_82
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f929]) ).
fof(f936,plain,
( e0 = e2
| ~ spl0_45
| ~ spl0_57 ),
inference(forward_demodulation,[],[f564,f512]) ).
fof(f938,plain,
( $false
| ~ spl0_45
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f936,f154]) ).
fof(f939,plain,
( ~ spl0_45
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f938]) ).
fof(f950,plain,
( e0 = e3
| ~ spl0_42
| ~ spl0_60 ),
inference(superposition,[],[f577,f499]) ).
fof(f956,plain,
( $false
| ~ spl0_42
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f950,f153]) ).
fof(f957,plain,
( ~ spl0_42
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f956]) ).
fof(f959,plain,
( e0 = e2
| ~ spl0_41
| ~ spl0_53 ),
inference(forward_demodulation,[],[f547,f495]) ).
fof(f968,plain,
( $false
| ~ spl0_41
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f959,f154]) ).
fof(f969,plain,
( ~ spl0_41
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f968]) ).
fof(f972,plain,
( e0 = e2
| ~ spl0_42
| ~ spl0_54 ),
inference(forward_demodulation,[],[f551,f499]) ).
fof(f973,plain,
( $false
| ~ spl0_42
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f972,f154]) ).
fof(f974,plain,
( ~ spl0_42
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f973]) ).
fof(f988,plain,
( e0 = e3
| ~ spl0_44
| ~ spl0_62 ),
inference(superposition,[],[f586,f508]) ).
fof(f992,plain,
( $false
| ~ spl0_44
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f988,f153]) ).
fof(f993,plain,
( ~ spl0_44
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f995,plain,
( e1 = e3
| ~ spl0_69
| ~ spl0_77 ),
inference(forward_demodulation,[],[f653,f617]) ).
fof(f1000,plain,
( $false
| ~ spl0_69
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f995,f151]) ).
fof(f1001,plain,
( ~ spl0_69
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1000]) ).
fof(f1004,plain,
( e2 = e3
| ~ spl0_58
| ~ spl0_64 ),
inference(superposition,[],[f594,f568]) ).
fof(f1005,plain,
( e2 = e3
| ~ spl0_58
| ~ spl0_64 ),
inference(superposition,[],[f568,f594]) ).
fof(f1007,plain,
( $false
| ~ spl0_58
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1005,f150]) ).
fof(f1008,plain,
( ~ spl0_58
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1009,plain,
( $false
| ~ spl0_58
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1004,f150]) ).
fof(f1010,plain,
( ~ spl0_58
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1009]) ).
fof(f1025,plain,
( e1 = e3
| ~ spl0_52
| ~ spl0_64 ),
inference(superposition,[],[f542,f594]) ).
fof(f1026,plain,
( e1 = e3
| ~ spl0_52
| ~ spl0_64 ),
inference(superposition,[],[f594,f542]) ).
fof(f1028,plain,
( $false
| ~ spl0_52
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1026,f151]) ).
fof(f1029,plain,
( ~ spl0_52
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1028]) ).
fof(f1030,plain,
( $false
| ~ spl0_52
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1025,f151]) ).
fof(f1031,plain,
( ~ spl0_52
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1030]) ).
fof(f1032,plain,
( e0 = e1
| ~ spl0_42
| ~ spl0_48 ),
inference(forward_demodulation,[],[f525,f499]) ).
fof(f1033,plain,
( e0 = e1
| ~ spl0_44
| ~ spl0_50 ),
inference(forward_demodulation,[],[f534,f508]) ).
fof(f1034,plain,
( e1 = e2
| ~ spl0_52
| ~ spl0_58 ),
inference(forward_demodulation,[],[f568,f542]) ).
fof(f1035,plain,
( e2 = e3
| ~ spl0_57
| ~ spl0_63 ),
inference(forward_demodulation,[],[f590,f564]) ).
fof(f1038,plain,
( $false
| ~ spl0_42
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1032,f155]) ).
fof(f1039,plain,
( ~ spl0_42
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1040,plain,
( $false
| ~ spl0_44
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1033,f155]) ).
fof(f1041,plain,
( ~ spl0_44
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1042,plain,
( $false
| ~ spl0_52
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1034,f152]) ).
fof(f1043,plain,
( ~ spl0_52
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1042]) ).
fof(f1044,plain,
( $false
| ~ spl0_57
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f1035,f150]) ).
fof(f1045,plain,
( ~ spl0_57
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f1044]) ).
fof(f1055,plain,
( e0 = e3
| ~ spl0_45
| ~ spl0_63 ),
inference(forward_demodulation,[],[f590,f512]) ).
fof(f1060,plain,
( $false
| ~ spl0_45
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f1055,f153]) ).
fof(f1061,plain,
( ~ spl0_45
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f1060]) ).
fof(f1083,plain,
( e2 = e3
| ~ spl0_74
| ~ spl0_78 ),
inference(superposition,[],[f657,f639]) ).
fof(f1084,plain,
( e2 = e3
| ~ spl0_74
| ~ spl0_78 ),
inference(superposition,[],[f639,f657]) ).
fof(f1087,plain,
( $false
| ~ spl0_74
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f1084,f150]) ).
fof(f1088,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1089,plain,
( $false
| ~ spl0_74
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f1083,f150]) ).
fof(f1090,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1096,plain,
( e0 = e2
| ~ spl0_46
| ~ spl0_58 ),
inference(superposition,[],[f516,f568]) ).
fof(f1101,plain,
( $false
| ~ spl0_46
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1096,f154]) ).
fof(f1102,plain,
( ~ spl0_46
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1101]) ).
fof(f1117,plain,
( e1 = e2
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_demodulation,[],[f289,f267]) ).
fof(f1132,plain,
( $false
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1117,f152]) ).
fof(f1133,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1132]) ).
fof(f1158,plain,
( e2 = e3
| ~ spl0_76
| ~ spl0_80 ),
inference(forward_demodulation,[],[f666,f648]) ).
fof(f1162,plain,
( $false
| ~ spl0_76
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1158,f150]) ).
fof(f1163,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1162]) ).
fof(f1178,plain,
( e1 = e3
| ~ spl0_13
| ~ spl0_33 ),
inference(superposition,[],[f298,f391]) ).
fof(f1179,plain,
( e1 = e3
| ~ spl0_13
| ~ spl0_33 ),
inference(superposition,[],[f391,f298]) ).
fof(f1181,plain,
( $false
| ~ spl0_13
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1179,f151]) ).
fof(f1182,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1181]) ).
fof(f1183,plain,
( $false
| ~ spl0_13
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1178,f151]) ).
fof(f1184,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1183]) ).
fof(f1185,plain,
( e1 = e3
| ~ spl0_26
| ~ spl0_38 ),
inference(forward_demodulation,[],[f357,f435]) ).
fof(f1188,plain,
( e3 != op(e1,e1)
| ~ spl0_13
| spl0_28 ),
inference(forward_demodulation,[],[f367,f298]) ).
fof(f1189,plain,
( e3 != op(e1,e2)
| spl0_7
| ~ spl0_13 ),
inference(forward_demodulation,[],[f273,f298]) ).
fof(f1191,plain,
( $false
| ~ spl0_26
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1185,f151]) ).
fof(f1192,plain,
( ~ spl0_26
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1199,plain,
( e0 != op(e1,e1)
| spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f295,f298]) ).
fof(f1200,plain,
( $false
| ~ spl0_13
| ~ spl0_26
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1188,f357]) ).
fof(f1201,plain,
( ~ spl0_13
| ~ spl0_26
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f1200]) ).
fof(f1203,plain,
( e0 != op(e1,e2)
| ~ spl0_13
| spl0_34 ),
inference(forward_demodulation,[],[f397,f298]) ).
fof(f1233,plain,
( e0 = e2
| ~ spl0_67
| ~ spl0_75 ),
inference(superposition,[],[f608,f644]) ).
fof(f1237,plain,
( $false
| ~ spl0_67
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1233,f154]) ).
fof(f1238,plain,
( ~ spl0_67
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1237]) ).
fof(f1245,plain,
( e2 = e3
| ~ spl0_73
| ~ spl0_77 ),
inference(superposition,[],[f653,f635]) ).
fof(f1251,plain,
( $false
| ~ spl0_73
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1245,f150]) ).
fof(f1252,plain,
( ~ spl0_73
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1251]) ).
fof(f1257,plain,
( e1 = e2
| ~ spl0_70
| ~ spl0_74 ),
inference(forward_demodulation,[],[f639,f621]) ).
fof(f1265,plain,
( $false
| ~ spl0_70
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1257,f152]) ).
fof(f1266,plain,
( ~ spl0_70
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1265]) ).
fof(f1290,plain,
( e0 = e2
| ~ spl0_11
| ~ spl0_37 ),
inference(superposition,[],[f414,f289]) ).
fof(f1296,plain,
( $false
| ~ spl0_11
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f1290,f154]) ).
fof(f1297,plain,
( ~ spl0_11
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f1296]) ).
fof(f1322,plain,
( e0 != op(e3,e2)
| ~ spl0_22 ),
inference(superposition,[],[f102,f338]) ).
fof(f1323,plain,
( e0 != op(e3,e1)
| ~ spl0_22 ),
inference(superposition,[],[f103,f338]) ).
fof(f1328,plain,
( e3 != op(e3,e0)
| ~ spl0_88 ),
inference(superposition,[],[f106,f706]) ).
fof(f1338,plain,
( e1 != op(e2,e0)
| ~ spl0_13 ),
inference(superposition,[],[f112,f298]) ).
fof(f1359,plain,
( e0 != op(e1,e3)
| ~ spl0_22 ),
inference(superposition,[],[f127,f338]) ).
fof(f1370,plain,
( e1 != op(e1,e2)
| ~ spl0_13 ),
inference(superposition,[],[f134,f298]) ).
fof(f1378,plain,
( e2 != op(e1,e1)
| ~ spl0_76 ),
inference(superposition,[],[f139,f648]) ).
fof(f1400,plain,
( e1 != op(e2,e2)
| spl0_10
| ~ spl0_11 ),
inference(superposition,[],[f286,f289]) ).
fof(f1403,plain,
( e3 != op(e2,e0)
| spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f260,f289]) ).
fof(f1408,plain,
( ~ spl0_26
| ~ spl0_6
| spl0_19 ),
inference(avatar_split_clause,[],[f801,f324,f266,f356]) ).
fof(f1417,plain,
( e0 = e3
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_demodulation,[],[f653,f599]) ).
fof(f1418,plain,
( e1 = e3
| ~ spl0_71
| ~ spl0_79 ),
inference(forward_demodulation,[],[f662,f626]) ).
fof(f1432,plain,
( $false
| ~ spl0_15
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1378,f307]) ).
fof(f1433,plain,
( ~ spl0_15
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f1432]) ).
fof(f1434,plain,
( e0 = e3
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_demodulation,[],[f366,f294]) ).
fof(f1439,plain,
( e3 != op(e1,e0)
| spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f260,f267]) ).
fof(f1441,plain,
( $false
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1417,f153]) ).
fof(f1442,plain,
( ~ spl0_65
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1441]) ).
fof(f1443,plain,
( $false
| ~ spl0_71
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f1418,f151]) ).
fof(f1444,plain,
( ~ spl0_71
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f1443]) ).
fof(f1445,plain,
( $false
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1434,f153]) ).
fof(f1446,plain,
( ~ spl0_12
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f1445]) ).
fof(f1453,plain,
( e2 = e3
| ~ spl0_56
| ~ spl0_62 ),
inference(forward_demodulation,[],[f586,f560]) ).
fof(f1459,plain,
( $false
| ~ spl0_56
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f1453,f150]) ).
fof(f1460,plain,
( ~ spl0_56
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f1459]) ).
fof(f1462,plain,
( ~ spl0_56
| ~ spl0_6
| spl0_18 ),
inference(avatar_split_clause,[],[f734,f320,f266,f558]) ).
fof(f1463,plain,
( ~ spl0_62
| spl0_4
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1439,f266,f258,f584]) ).
fof(f1465,plain,
( e2 != op(e1,e1)
| spl0_5
| ~ spl0_6 ),
inference(superposition,[],[f264,f267]) ).
fof(f1467,plain,
( $false
| spl0_5
| ~ spl0_6
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1465,f307]) ).
fof(f1468,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f1467]) ).
fof(f1477,plain,
( e0 = e1
| ~ spl0_46
| ~ spl0_52 ),
inference(forward_demodulation,[],[f542,f516]) ).
fof(f1498,plain,
( e2 != op(e3,e0)
| spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f322,f343]) ).
fof(f1502,plain,
( $false
| ~ spl0_46
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f1477,f155]) ).
fof(f1503,plain,
( ~ spl0_46
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f1502]) ).
fof(f1509,plain,
( e2 != op(e1,e1)
| ~ spl0_25
| spl0_31 ),
inference(forward_demodulation,[],[f381,f352]) ).
fof(f1512,plain,
( e1 = e3
| ~ spl0_50
| ~ spl0_62 ),
inference(forward_demodulation,[],[f586,f534]) ).
fof(f1516,plain,
( $false
| ~ spl0_15
| ~ spl0_25
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f1509,f307]) ).
fof(f1517,plain,
( ~ spl0_15
| ~ spl0_25
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f1516]) ).
fof(f1518,plain,
( $false
| ~ spl0_50
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f1512,f151]) ).
fof(f1519,plain,
( ~ spl0_50
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1520,plain,
( op(e0,e0) != e3
| ~ spl0_9
| spl0_28 ),
inference(forward_demodulation,[],[f367,f280]) ).
fof(f1524,plain,
( ~ spl0_66
| ~ spl0_25
| spl0_36 ),
inference(avatar_split_clause,[],[f741,f405,f351,f601]) ).
fof(f1553,plain,
( $false
| ~ spl0_9
| ~ spl0_23
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1520,f343]) ).
fof(f1554,plain,
( ~ spl0_9
| ~ spl0_23
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f1553]) ).
fof(f1555,plain,
( e1 != op(e3,e3)
| spl0_10
| ~ spl0_23 ),
inference(forward_demodulation,[],[f286,f343]) ).
fof(f1561,plain,
( $false
| spl0_10
| ~ spl0_23
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1555,f352]) ).
fof(f1562,plain,
( spl0_10
| ~ spl0_23
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1561]) ).
fof(f1563,plain,
( e0 = e1
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_demodulation,[],[f298,f280]) ).
fof(f1570,plain,
( ~ spl0_51
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1338,f297,f536]) ).
fof(f1572,plain,
( ~ spl0_58
| spl0_18
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1498,f342,f320,f566]) ).
fof(f1594,plain,
( e0 != op(e3,e1)
| ~ spl0_26
| spl0_35 ),
inference(forward_demodulation,[],[f402,f357]) ).
fof(f1595,plain,
( $false
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1563,f155]) ).
fof(f1596,plain,
( ~ spl0_9
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1595]) ).
fof(f1602,plain,
( $false
| ~ spl0_26
| spl0_35
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f1594,f612]) ).
fof(f1603,plain,
( ~ spl0_26
| spl0_35
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f1602]) ).
fof(f1606,plain,
( e2 != op(e3,e3)
| spl0_2
| ~ spl0_26 ),
inference(forward_demodulation,[],[f251,f357]) ).
fof(f1610,plain,
( ~ spl0_68
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1323,f337,f610]) ).
fof(f1613,plain,
( e1 = e2
| ~ spl0_50
| ~ spl0_56 ),
inference(forward_demodulation,[],[f560,f534]) ).
fof(f1638,plain,
( $false
| ~ spl0_13
| spl0_34
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1203,f599]) ).
fof(f1639,plain,
( ~ spl0_13
| spl0_34
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f1638]) ).
fof(f1641,plain,
( $false
| ~ spl0_64
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1328,f594]) ).
fof(f1642,plain,
( ~ spl0_64
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1641]) ).
fof(f1651,plain,
( $false
| spl0_2
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1606,f386]) ).
fof(f1652,plain,
( spl0_2
| ~ spl0_26
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1651]) ).
fof(f1653,plain,
( $false
| ~ spl0_50
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f1613,f152]) ).
fof(f1654,plain,
( ~ spl0_50
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f1653]) ).
fof(f1656,plain,
( e2 = op(e3,e3)
| ~ spl0_2
| ~ spl0_26 ),
inference(forward_demodulation,[],[f250,f357]) ).
fof(f1658,plain,
( ~ spl0_77
| spl0_7
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1189,f297,f271,f651]) ).
fof(f1670,plain,
( $false
| ~ spl0_22
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1322,f676]) ).
fof(f1671,plain,
( ~ spl0_22
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f1670]) ).
fof(f1674,plain,
( $false
| ~ spl0_22
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1359,f603]) ).
fof(f1675,plain,
( ~ spl0_22
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f1674]) ).
fof(f1747,plain,
( e0 = e2
| ~ spl0_22
| ~ spl0_32 ),
inference(superposition,[],[f386,f338]) ).
fof(f1749,plain,
( e2 != op(e3,e1)
| ~ spl0_32 ),
inference(superposition,[],[f103,f386]) ).
fof(f1750,plain,
( e2 != op(e3,e0)
| ~ spl0_32 ),
inference(superposition,[],[f105,f386]) ).
fof(f1752,plain,
( e2 != op(e1,e3)
| ~ spl0_32 ),
inference(superposition,[],[f127,f386]) ).
fof(f1765,plain,
( $false
| ~ spl0_32
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1750,f568]) ).
fof(f1766,plain,
( ~ spl0_32
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1765]) ).
fof(f1767,plain,
( $false
| ~ spl0_22
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1747,f154]) ).
fof(f1768,plain,
( ~ spl0_22
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1767]) ).
fof(f1772,plain,
( ~ spl0_63
| spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1403,f288,f258,f588]) ).
fof(f1776,plain,
( e2 = e3
| ~ spl0_75
| ~ spl0_79 ),
inference(forward_demodulation,[],[f662,f644]) ).
fof(f1794,plain,
( e0 = e2
| ~ spl0_2
| ~ spl0_22
| ~ spl0_26 ),
inference(forward_demodulation,[],[f1656,f338]) ).
fof(f1801,plain,
( $false
| ~ spl0_3
| spl0_12
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1199,f254]) ).
fof(f1802,plain,
( ~ spl0_3
| spl0_12
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1801]) ).
fof(f1804,plain,
( $false
| ~ spl0_75
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f1776,f150]) ).
fof(f1805,plain,
( ~ spl0_75
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f1804]) ).
fof(f1806,plain,
( $false
| ~ spl0_2
| ~ spl0_22
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1794,f154]) ).
fof(f1807,plain,
( ~ spl0_2
| ~ spl0_22
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f1806]) ).
fof(f1811,plain,
( ~ spl0_13
| spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1400,f288,f284,f297]) ).
fof(f1838,plain,
( op(e0,e0) = e2
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f250,f254]) ).
fof(f1840,plain,
( e3 != op(e0,e1)
| spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f247,f254]) ).
fof(f1865,plain,
( op(e0,e0) != e2
| spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f251,f254]) ).
fof(f1868,plain,
( e0 = e2
| ~ spl0_3
| ~ spl0_15 ),
inference(forward_demodulation,[],[f307,f254]) ).
fof(f1869,plain,
( e2 != op(e0,e1)
| ~ spl0_3
| spl0_16 ),
inference(forward_demodulation,[],[f313,f254]) ).
fof(f1878,plain,
( e1 = e2
| ~ spl0_49
| ~ spl0_55 ),
inference(forward_demodulation,[],[f555,f529]) ).
fof(f1898,plain,
( $false
| ~ spl0_3
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1868,f154]) ).
fof(f1899,plain,
( ~ spl0_3
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f1898]) ).
fof(f1907,plain,
( $false
| ~ spl0_49
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f1878,f152]) ).
fof(f1908,plain,
( ~ spl0_49
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1914,plain,
( ~ spl0_59
| spl0_1
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1840,f253,f245,f571]) ).
fof(f1916,plain,
( spl0_11
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1838,f253,f249,f288]) ).
fof(f1920,plain,
( op(e0,e0) != e3
| ~ spl0_3
| spl0_17 ),
inference(forward_demodulation,[],[f317,f254]) ).
fof(f1937,plain,
( e1 != op(e2,e0)
| ~ spl0_11
| spl0_29 ),
inference(forward_demodulation,[],[f372,f289]) ).
fof(f1943,plain,
( $false
| ~ spl0_11
| spl0_29
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f1937,f538]) ).
fof(f1944,plain,
( ~ spl0_11
| spl0_29
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f1943]) ).
fof(f1946,plain,
( e3 != op(e2,e2)
| ~ spl0_11
| spl0_19 ),
inference(forward_demodulation,[],[f326,f289]) ).
fof(f1948,plain,
( $false
| ~ spl0_11
| spl0_19
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1946,f391]) ).
fof(f1949,plain,
( ~ spl0_11
| spl0_19
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1948]) ).
fof(f1957,plain,
( e2 = e3
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f343,f289]) ).
fof(f1974,plain,
( $false
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1957,f150]) ).
fof(f1975,plain,
( ~ spl0_11
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1974]) ).
fof(f1977,plain,
( ~ spl0_11
| spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1865,f253,f249,f288]) ).
fof(f1978,plain,
( ~ spl0_69
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1370,f297,f615]) ).
fof(f1990,plain,
( ~ spl0_76
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f1749,f385,f646]) ).
fof(f1992,plain,
( $false
| ~ spl0_32
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1752,f639]) ).
fof(f1993,plain,
( ~ spl0_32
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1992]) ).
fof(f1996,plain,
( e0 = e1
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_demodulation,[],[f435,f254]) ).
fof(f2000,plain,
( e2 = e3
| ~ spl0_32
| ~ spl0_40 ),
inference(forward_demodulation,[],[f475,f386]) ).
fof(f2004,plain,
( e0 = e1
| ~ spl0_81
| ~ spl0_83 ),
inference(forward_demodulation,[],[f681,f671]) ).
fof(f2016,plain,
( e0 != op(e2,e3)
| ~ spl0_32
| spl0_36 ),
inference(forward_demodulation,[],[f407,f386]) ).
fof(f2029,plain,
( $false
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1996,f155]) ).
fof(f2030,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f2029]) ).
fof(f2031,plain,
( $false
| ~ spl0_32
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2000,f150]) ).
fof(f2032,plain,
( ~ spl0_32
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f2031]) ).
fof(f2035,plain,
( $false
| ~ spl0_81
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2004,f155]) ).
fof(f2036,plain,
( ~ spl0_81
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f2035]) ).
fof(f2038,plain,
( $false
| ~ spl0_32
| spl0_36
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2016,f671]) ).
fof(f2039,plain,
( ~ spl0_32
| spl0_36
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2038]) ).
fof(f2050,plain,
( e1 != op(e2,e2)
| spl0_21
| ~ spl0_32 ),
inference(forward_demodulation,[],[f335,f386]) ).
fof(f2075,plain,
( $false
| ~ spl0_3
| spl0_16
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f1869,f547]) ).
fof(f2076,plain,
( ~ spl0_3
| spl0_16
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2080,plain,
( $false
| ~ spl0_3
| spl0_17
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1920,f343]) ).
fof(f2081,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2080]) ).
fof(f2082,plain,
( $false
| ~ spl0_13
| spl0_21
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2050,f298]) ).
fof(f2083,plain,
( ~ spl0_13
| spl0_21
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f2082]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f256]) ).
cnf(s2,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f269]) ).
cnf(s4,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f291]) ).
cnf(s5,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f300]) ).
cnf(s7,plain,
( ~ spl0_3
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f318]) ).
cnf(s8,plain,
( ~ spl0_6
| ~ spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f327]) ).
cnf(s10,plain,
( ~ spl0_10
| ~ spl0_18
| ~ spl0_23 ),
inference(sat_conversion,[],[f345]) ).
cnf(s13,plain,
( ~ spl0_9
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f368]) ).
cnf(s14,plain,
( ~ spl0_11
| ~ spl0_19
| ~ spl0_29 ),
inference(sat_conversion,[],[f373]) ).
cnf(s19,plain,
( ~ spl0_13
| ~ spl0_28
| ~ spl0_34 ),
inference(sat_conversion,[],[f398]) ).
cnf(s20,plain,
( ~ spl0_15
| ~ spl0_17
| ~ spl0_35 ),
inference(sat_conversion,[],[f403]) ).
cnf(s21,plain,
( ~ spl0_25
| ~ spl0_31
| ~ spl0_36 ),
inference(sat_conversion,[],[f408]) ).
cnf(s22,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_35 ),
inference(sat_conversion,[],[f409]) ).
cnf(s23,plain,
( ~ spl0_21
| ~ spl0_32
| ~ spl0_36 ),
inference(sat_conversion,[],[f410]) ).
cnf(s26,plain,
( spl0_3
| ~ spl0_11
| spl0_22
| spl0_37 ),
inference(sat_conversion,[],[f417]) ).
cnf(s29,plain,
( spl0_3
| spl0_9
| spl0_22
| ~ spl0_37 ),
inference(sat_conversion,[],[f420]) ).
cnf(s30,plain,
( spl0_3
| spl0_9
| spl0_22
| spl0_37 ),
inference(sat_conversion,[],[f421]) ).
cnf(s42,plain,
( spl0_6
| ~ spl0_15
| spl0_25
| spl0_38 ),
inference(sat_conversion,[],[f437]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_13
| spl0_25
| spl0_38 ),
inference(sat_conversion,[],[f440]) ).
cnf(s46,plain,
( spl0_6
| spl0_13
| spl0_25
| spl0_38 ),
inference(sat_conversion,[],[f441]) ).
cnf(s48,plain,
( spl0_6
| spl0_13
| spl0_25
| ~ spl0_38 ),
inference(sat_conversion,[],[f443]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_13
| ~ spl0_26
| spl0_38 ),
inference(sat_conversion,[],[f448]) ).
cnf(s58,plain,
( spl0_11
| spl0_15
| spl0_32
| ~ spl0_39 ),
inference(sat_conversion,[],[f457]) ).
cnf(s61,plain,
( ~ spl0_9
| spl0_15
| spl0_32
| spl0_39 ),
inference(sat_conversion,[],[f460]) ).
cnf(s62,plain,
( spl0_11
| spl0_15
| spl0_32
| spl0_39 ),
inference(sat_conversion,[],[f461]) ).
cnf(s74,plain,
( spl0_23
| spl0_26
| ~ spl0_32
| spl0_40 ),
inference(sat_conversion,[],[f477]) ).
cnf(s77,plain,
( ~ spl0_22
| spl0_26
| spl0_33
| spl0_40 ),
inference(sat_conversion,[],[f480]) ).
cnf(s78,plain,
( spl0_23
| spl0_26
| spl0_33
| spl0_40 ),
inference(sat_conversion,[],[f481]) ).
cnf(s80,plain,
( spl0_23
| ~ spl0_25
| spl0_33
| spl0_40 ),
inference(sat_conversion,[],[f483]) ).
cnf(s86,plain,
( spl0_23
| spl0_26
| spl0_33
| ~ spl0_40 ),
inference(sat_conversion,[],[f489]) ).
cnf(s90,plain,
( spl0_37
| spl0_44
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f517]) ).
cnf(s92,plain,
( spl0_6
| spl0_50
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f543]) ).
cnf(s93,plain,
( spl0_11
| spl0_53
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f556]) ).
cnf(s94,plain,
( spl0_11
| spl0_56
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f569]) ).
cnf(s95,plain,
( spl0_23
| spl0_59
| spl0_60
| spl0_61 ),
inference(sat_conversion,[],[f582]) ).
cnf(s96,plain,
( spl0_23
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f595]) ).
cnf(s97,plain,
( spl0_3
| spl0_44
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f604]) ).
cnf(s98,plain,
( spl0_3
| spl0_41
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f613]) ).
cnf(s99,plain,
( spl0_38
| spl0_50
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f622]) ).
cnf(s101,plain,
( spl0_15
| spl0_56
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f640]) ).
cnf(s102,plain,
( spl0_15
| spl0_53
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f649]) ).
cnf(s103,plain,
( spl0_26
| spl0_62
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f658]) ).
cnf(s104,plain,
( spl0_26
| spl0_59
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f667]) ).
cnf(s105,plain,
( spl0_9
| spl0_45
| spl0_67
| spl0_81 ),
inference(sat_conversion,[],[f672]) ).
cnf(s106,plain,
( spl0_9
| spl0_42
| spl0_65
| spl0_82 ),
inference(sat_conversion,[],[f677]) ).
cnf(s107,plain,
( spl0_13
| spl0_51
| spl0_71
| spl0_83 ),
inference(sat_conversion,[],[f682]) ).
cnf(s108,plain,
( spl0_13
| spl0_48
| spl0_69
| spl0_84 ),
inference(sat_conversion,[],[f687]) ).
cnf(s109,plain,
( spl0_39
| spl0_57
| spl0_75
| spl0_85 ),
inference(sat_conversion,[],[f692]) ).
cnf(s112,plain,
( spl0_33
| spl0_60
| spl0_77
| spl0_88 ),
inference(sat_conversion,[],[f707]) ).
cnf(s113,plain,
( spl0_22
| spl0_46
| spl0_68
| spl0_82 ),
inference(sat_conversion,[],[f708]) ).
cnf(s116,plain,
( spl0_25
| spl0_49
| spl0_70
| spl0_83 ),
inference(sat_conversion,[],[f711]) ).
cnf(s117,plain,
( spl0_32
| spl0_58
| spl0_76
| spl0_86 ),
inference(sat_conversion,[],[f712]) ).
cnf(s118,plain,
( spl0_32
| spl0_55
| spl0_74
| spl0_85 ),
inference(sat_conversion,[],[f713]) ).
cnf(s119,plain,
( spl0_40
| spl0_64
| spl0_80
| spl0_88 ),
inference(sat_conversion,[],[f714]) ).
cnf(s137,plain,
( ~ spl0_6
| ~ spl0_23 ),
inference(sat_conversion,[],[f747]) ).
cnf(s138,plain,
( ~ spl0_15
| ~ spl0_26 ),
inference(sat_conversion,[],[f749]) ).
cnf(s139,plain,
( ~ spl0_9
| spl0_27
| ~ spl0_48 ),
inference(sat_conversion,[],[f751]) ).
cnf(s140,plain,
( ~ spl0_25
| ~ spl0_32 ),
inference(sat_conversion,[],[f753]) ).
cnf(s141,plain,
( ~ spl0_9
| ~ spl0_33 ),
inference(sat_conversion,[],[f755]) ).
cnf(s144,plain,
( ~ spl0_9
| ~ spl0_39 ),
inference(sat_conversion,[],[f761]) ).
cnf(s145,plain,
( ~ spl0_25
| ~ spl0_40 ),
inference(sat_conversion,[],[f763]) ).
cnf(s146,plain,
( ~ spl0_44
| ~ spl0_56 ),
inference(sat_conversion,[],[f765]) ).
cnf(s148,plain,
( ~ spl0_15
| spl0_17
| ~ spl0_33 ),
inference(sat_conversion,[],[f783]) ).
cnf(s151,plain,
( ~ spl0_41
| ~ spl0_59 ),
inference(sat_conversion,[],[f789]) ).
cnf(s153,plain,
( ~ spl0_82
| ~ spl0_84 ),
inference(sat_conversion,[],[f793]) ).
cnf(s154,plain,
( ~ spl0_81
| ~ spl0_85 ),
inference(sat_conversion,[],[f795]) ).
cnf(s155,plain,
( ~ spl0_22
| ~ spl0_40 ),
inference(sat_conversion,[],[f798]) ).
cnf(s156,plain,
( ~ spl0_15
| spl0_35
| ~ spl0_67 ),
inference(sat_conversion,[],[f803]) ).
cnf(s157,plain,
( ~ spl0_48
| ~ spl0_60 ),
inference(sat_conversion,[],[f816]) ).
cnf(s159,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(sat_conversion,[],[f820]) ).
cnf(s160,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(sat_conversion,[],[f822]) ).
cnf(s161,plain,
( ~ spl0_22
| ~ spl0_25 ),
inference(sat_conversion,[],[f832]) ).
cnf(s163,plain,
( ~ spl0_55
| ~ spl0_61 ),
inference(sat_conversion,[],[f836]) ).
cnf(s164,plain,
( ~ spl0_68
| ~ spl0_80 ),
inference(sat_conversion,[],[f838]) ).
cnf(s166,plain,
( ~ spl0_70
| ~ spl0_78 ),
inference(sat_conversion,[],[f851]) ).
cnf(s169,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(sat_conversion,[],[f864]) ).
cnf(s171,plain,
( ~ spl0_66
| ~ spl0_70 ),
inference(sat_conversion,[],[f872]) ).
cnf(s172,plain,
( ~ spl0_69
| ~ spl0_73 ),
inference(sat_conversion,[],[f882]) ).
cnf(s174,plain,
( ~ spl0_46
| ~ spl0_64 ),
inference(sat_conversion,[],[f892]) ).
cnf(s175,plain,
( ~ spl0_65
| ~ spl0_73 ),
inference(sat_conversion,[],[f894]) ).
cnf(s176,plain,
( ~ spl0_84
| ~ spl0_86 ),
inference(sat_conversion,[],[f898]) ).
cnf(s178,plain,
( ~ spl0_15
| ~ spl0_38 ),
inference(sat_conversion,[],[f909]) ).
cnf(s180,plain,
( ~ spl0_33
| ~ spl0_39 ),
inference(sat_conversion,[],[f918]) ).
cnf(s181,plain,
( ~ spl0_51
| ~ spl0_57 ),
inference(sat_conversion,[],[f928]) ).
cnf(s182,plain,
( ~ spl0_82
| ~ spl0_86 ),
inference(sat_conversion,[],[f930]) ).
cnf(s184,plain,
( ~ spl0_45
| ~ spl0_57 ),
inference(sat_conversion,[],[f939]) ).
cnf(s187,plain,
( ~ spl0_42
| ~ spl0_60 ),
inference(sat_conversion,[],[f957]) ).
cnf(s189,plain,
( ~ spl0_41
| ~ spl0_53 ),
inference(sat_conversion,[],[f969]) ).
cnf(s190,plain,
( ~ spl0_42
| ~ spl0_54 ),
inference(sat_conversion,[],[f974]) ).
cnf(s193,plain,
( ~ spl0_44
| ~ spl0_62 ),
inference(sat_conversion,[],[f993]) ).
cnf(s194,plain,
( ~ spl0_69
| ~ spl0_77 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s195,plain,
( ~ spl0_58
| ~ spl0_64 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s196,plain,
( ~ spl0_58
| ~ spl0_64 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s199,plain,
( ~ spl0_52
| ~ spl0_64 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s200,plain,
( ~ spl0_52
| ~ spl0_64 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s201,plain,
( ~ spl0_42
| ~ spl0_48 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s202,plain,
( ~ spl0_44
| ~ spl0_50 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s203,plain,
( ~ spl0_52
| ~ spl0_58 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s204,plain,
( ~ spl0_57
| ~ spl0_63 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s205,plain,
( ~ spl0_45
| ~ spl0_63 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s208,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s209,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s211,plain,
( ~ spl0_46
| ~ spl0_58 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s215,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f1133]) ).
cnf(s221,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s223,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s224,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s225,plain,
( ~ spl0_26
| ~ spl0_38 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s228,plain,
( ~ spl0_13
| ~ spl0_26
| spl0_28 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s234,plain,
( ~ spl0_67
| ~ spl0_75 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s236,plain,
( ~ spl0_73
| ~ spl0_77 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s239,plain,
( ~ spl0_70
| ~ spl0_74 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s243,plain,
( ~ spl0_11
| ~ spl0_37 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s249,plain,
( ~ spl0_6
| spl0_19
| ~ spl0_26 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s253,plain,
( ~ spl0_15
| ~ spl0_76 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s254,plain,
( ~ spl0_65
| ~ spl0_77 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s255,plain,
( ~ spl0_71
| ~ spl0_79 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s256,plain,
( ~ spl0_12
| ~ spl0_28 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s258,plain,
( ~ spl0_56
| ~ spl0_62 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s259,plain,
( ~ spl0_6
| spl0_18
| ~ spl0_56 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s261,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_62 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s262,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_15 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s264,plain,
( ~ spl0_46
| ~ spl0_52 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s267,plain,
( ~ spl0_15
| ~ spl0_25
| spl0_31 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s268,plain,
( ~ spl0_50
| ~ spl0_62 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s271,plain,
( ~ spl0_25
| spl0_36
| ~ spl0_66 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s275,plain,
( ~ spl0_9
| ~ spl0_23
| spl0_28 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s276,plain,
( spl0_10
| ~ spl0_23
| ~ spl0_25 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s281,plain,
( ~ spl0_13
| ~ spl0_51 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s282,plain,
( spl0_18
| ~ spl0_23
| ~ spl0_58 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s286,plain,
( ~ spl0_9
| ~ spl0_13 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s288,plain,
( ~ spl0_26
| spl0_35
| ~ spl0_68 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s293,plain,
( ~ spl0_22
| ~ spl0_68 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s300,plain,
( ~ spl0_13
| spl0_34
| ~ spl0_65 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s301,plain,
( ~ spl0_64
| ~ spl0_88 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s303,plain,
( spl0_2
| ~ spl0_26
| ~ spl0_32 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s304,plain,
( ~ spl0_50
| ~ spl0_56 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s305,plain,
( spl0_7
| ~ spl0_13
| ~ spl0_77 ),
inference(sat_conversion,[],[f1658]) ).
cnf(s308,plain,
( ~ spl0_22
| ~ spl0_82 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s309,plain,
( ~ spl0_22
| ~ spl0_66 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s321,plain,
( ~ spl0_32
| ~ spl0_58 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s322,plain,
( ~ spl0_22
| ~ spl0_32 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s324,plain,
( spl0_4
| ~ spl0_11
| ~ spl0_63 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s325,plain,
( ~ spl0_3
| spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f1802]) ).
cnf(s326,plain,
( ~ spl0_75
| ~ spl0_79 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s327,plain,
( ~ spl0_2
| ~ spl0_22
| ~ spl0_26 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s329,plain,
( spl0_10
| ~ spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f1811]) ).
cnf(s341,plain,
( ~ spl0_3
| ~ spl0_15 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s345,plain,
( ~ spl0_49
| ~ spl0_55 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s348,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_59 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s349,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_11 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s353,plain,
( ~ spl0_11
| spl0_29
| ~ spl0_51 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s354,plain,
( ~ spl0_11
| spl0_19
| ~ spl0_33 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s359,plain,
( ~ spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s360,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_11 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s362,plain,
( ~ spl0_13
| ~ spl0_69 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s373,plain,
( ~ spl0_32
| ~ spl0_76 ),
inference(sat_conversion,[],[f1990]) ).
cnf(s374,plain,
( ~ spl0_32
| ~ spl0_74 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s377,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s378,plain,
( ~ spl0_32
| ~ spl0_40 ),
inference(sat_conversion,[],[f2032]) ).
cnf(s380,plain,
( ~ spl0_81
| ~ spl0_83 ),
inference(sat_conversion,[],[f2036]) ).
cnf(s381,plain,
( ~ spl0_32
| spl0_36
| ~ spl0_81 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s386,plain,
( ~ spl0_3
| spl0_16
| ~ spl0_53 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s388,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_23 ),
inference(sat_conversion,[],[f2081]) ).
cnf(s389,plain,
( ~ spl0_13
| spl0_21
| ~ spl0_32 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s390,plain,
( spl0_22
| spl0_9
| spl0_3 ),
inference(rat,[],[s29,s30]) ).
cnf(s391,plain,
( spl0_32
| spl0_15
| spl0_11 ),
inference(rat,[],[s58,s62]) ).
cnf(s392,plain,
( spl0_25
| spl0_13
| spl0_6 ),
inference(rat,[],[s48,s46]) ).
cnf(s393,plain,
( ~ spl0_15
| spl0_25
| spl0_6 ),
inference(rat,[],[s42,s178]) ).
cnf(s394,plain,
( ~ spl0_22
| spl0_6
| spl0_4
| spl0_3 ),
inference(rat,[],[s199,s96,s92,s193,s202,s97,s300,s19,s228,s324,s359,s77,s391,s224,s281,s393,s392,s155,s161,s309,s322]) ).
cnf(s395,plain,
( spl0_6
| spl0_4
| spl0_3 ),
inference(rat,[],[s164,s119,s113,s200,s264,s92,s181,s94,s146,s202,s97,s169,s108,s159,s176,s182,s271,s117,s139,s21,s282,s13,s253,s267,s10,s275,s276,s359,s61,s80,s140,s145,s392,s141,s144,s286,s390,s394]) ).
cnf(s396,plain,
( ~ spl0_32
| spl0_23
| spl0_2 ),
inference(rat,[],[s74,s303,s378]) ).
cnf(s397,plain,
( spl0_33
| spl0_26
| spl0_23 ),
inference(rat,[],[s78,s86]) ).
cnf(s398,plain,
( ~ spl0_81
| ~ spl0_78
| spl0_25
| spl0_32 ),
inference(rat,[],[s345,s118,s116,s154,s380,s209,s166]) ).
cnf(s399,plain,
( ~ spl0_65
| spl0_25
| spl0_32
| spl0_62
| spl0_23
| spl0_11 ),
inference(rat,[],[s195,s94,s96,s184,s205,s105,s398,s304,s99,s166,s103,s169,s254,s178,s141,s156,s20,s148,s397,s138,s391]) ).
cnf(s400,plain,
( spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s163,s95,s93,s187,s190,s106,s399,s151,s189,s98,s156,s161,s293,s308,s20,s390,s148,s141,s397,s138,s391,s396,s261,s137,s215,s395]) ).
cnf(s401,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_2 ),
inference(rat,[],[s391,s262,s396,s2,s137,s215]) ).
cnf(s402,plain,
( spl0_11
| spl0_32
| spl0_6
| spl0_3 ),
inference(rat,[],[s164,s119,s113,s200,s264,s92,s181,s94,s146,s202,s97,s169,s108,s159,s176,s182,s117,s139,s282,s13,s10,s275,s276,s397,s271,s141,s286,s21,s390,s267,s145,s161,s393,s138,s253,s391]) ).
cnf(s403,plain,
( ~ spl0_11
| spl0_6
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s392,s161,s329,s26,s4,s243]) ).
cnf(s404,plain,
( spl0_11
| spl0_3
| spl0_6 ),
inference(rat,[],[s286,s392,s390,s140,s322,s402]) ).
cnf(s405,plain,
( spl0_6
| spl0_3
| ~ spl0_4 ),
inference(rat,[],[s404,s403]) ).
cnf(s406,plain,
( spl0_3
| spl0_2 ),
inference(rat,[],[s405,s401,s400]) ).
cnf(s407,plain,
spl0_2,
inference(rat,[],[s166,s103,s99,s258,s304,s94,s184,s105,s234,s102,s305,s381,s386,s5,s23,s7,s325,s389,s286,s362,s388,s45,s396,s303,s140,s321,s373,s391,s341,s360,s377,s406]) ).
cnf(s408,plain,
( spl0_32
| ~ spl0_6 ),
inference(rat,[],[s163,s95,s93,s187,s190,s151,s189,s106,s98,s399,s156,s161,s293,s308,s20,s390,s261,s148,s141,s2,s397,s262,s138,s391,s137,s349,s215,s407]) ).
cnf(s409,plain,
( ~ spl0_64
| ~ spl0_6 ),
inference(rat,[],[s108,s153,s157,s113,s112,s174,s301,s286,s141,s390,s322,s349,s215,s288,s22,s236,s172,s101,s259,s8,s249,s138,s74,s137,s378,s374,s408,s407]) ).
cnf(s410,plain,
~ spl0_6,
inference(rat,[],[s171,s97,s99,s193,s268,s96,s409,s204,s172,s175,s94,s101,s259,s8,s249,s138,s225,s74,s321,s374,s378,s408,s349,s137,s215,s407]) ).
cnf(s411,plain,
spl0_3,
inference(rat,[],[s395,s405,s410]) ).
cnf(s412,plain,
~ spl0_38,
inference(rat,[],[s377,s411]) ).
cnf(s413,plain,
spl0_11,
inference(rat,[],[s349,s407,s411]) ).
cnf(s414,plain,
~ spl0_15,
inference(rat,[],[s341,s411]) ).
cnf(s415,plain,
~ spl0_23,
inference(rat,[],[s359,s413]) ).
cnf(s416,plain,
~ spl0_37,
inference(rat,[],[s243,s413]) ).
cnf(s418,plain,
~ spl0_22,
inference(rat,[],[s223,s45,s397,s161,s327,s411,s412,s415,s407]) ).
cnf(s419,plain,
~ spl0_13,
inference(rat,[],[s228,s256,s397,s325,s224,s415,s411]) ).
cnf(s420,plain,
~ spl0_26,
inference(rat,[],[s53,s412,s411,s419]) ).
cnf(s421,plain,
spl0_25,
inference(rat,[],[s45,s412,s411,s419]) ).
cnf(s423,plain,
spl0_33,
inference(rat,[],[s397,s415,s420]) ).
cnf(s426,plain,
~ spl0_32,
inference(rat,[],[s140,s421]) ).
cnf(s427,plain,
~ spl0_39,
inference(rat,[],[s180,s423]) ).
cnf(s428,plain,
~ spl0_9,
inference(rat,[],[s141,s423]) ).
cnf(s429,plain,
spl0_19,
inference(rat,[],[s354,s413,s423]) ).
cnf(s430,plain,
~ spl0_29,
inference(rat,[],[s14,s413,s429]) ).
cnf(s431,plain,
~ spl0_51,
inference(rat,[],[s353,s413,s430]) ).
cnf(s432,plain,
( ~ spl0_78
| ~ spl0_65 ),
inference(rat,[],[s304,s99,s101,s166,s209,s175,s169,s412,s414]) ).
cnf(s433,plain,
~ spl0_65,
inference(rat,[],[s239,s101,s99,s258,s268,s103,s432,s169,s175,s254,s414,s412,s420]) ).
cnf(s434,plain,
( ~ spl0_79
| spl0_57 ),
inference(rat,[],[s160,s107,s109,s255,s326,s419,s431,s427]) ).
cnf(s435,plain,
( ~ spl0_64
| spl0_59 ),
inference(rat,[],[s182,s113,s117,s164,s221,s104,s434,s184,s90,s202,s92,s174,s196,s200,s418,s426,s420,s416,s410,s431]) ).
cnf(s436,plain,
( ~ spl0_62
| spl0_59 ),
inference(rat,[],[s182,s113,s117,s164,s221,s104,s434,s184,s90,s203,s264,s92,s193,s268,s418,s426,s420,s416,s410,s431]) ).
cnf(s437,plain,
( spl0_82
| spl0_59 ),
inference(rat,[],[s208,s101,s103,s172,s194,s108,s176,s304,s117,s92,s201,s211,s264,s106,s113,s221,s164,s104,s434,s204,s96,s436,s435,s414,s420,s419,s426,s410,s431,s428,s433,s418,s415]) ).
cnf(s438,plain,
spl0_59,
inference(rat,[],[s202,s92,s90,s203,s211,s117,s182,s437,s221,s104,s434,s204,s205,s96,s436,s435,s410,s431,s416,s426,s420,s415]) ).
cnf(s439,plain,
~ spl0_1,
inference(rat,[],[s1,s407,s411]) ).
cnf(s443,plain,
$false,
inference(rat,[],[s348,s411,s439,s438]) ).
fof(f2084,plain,
$false,
inference(avatar_sat_refutation,[],[s443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG139+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.09/0.18 % Computer : n017.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:27:07 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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.18/0.29 % (3923100)Will run a generic schedule for satisfiability detection.
% 0.18/0.29 % (3923110)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3156710317:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.29 % (3923106)% WARNING: option uhcvi not known.
% 0.18/0.29 % (3923105)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1116768330_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.29 % (3923109)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2983519671:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.29 % (3923107)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3541900088:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.29 % (3923106)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2060040788:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.29 % (3923108)dis+10_1_sil=32000:sp=arity:random_seed=3693686777:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.29 % (3923111)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3839502367:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.29 % Detected minimum model sizes of [4]
% 0.18/0.29 % Detected maximum model sizes of [max]
% 0.18/0.29 % TRYING [4]
% 0.18/0.29 % TRYING [5]
% 0.18/0.29 % (3923110)Instruction limit reached!
% 0.18/0.29 % (3923110)------------------------------
% 0.18/0.29 % (3923110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.29 % (3923110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.29 % (3923110)CaDiCaL version: 2.1.3
% 0.18/0.29 % (3923110)Termination reason: Instruction limit
% 0.18/0.29 % (3923110)Termination phase: Saturation
% 0.18/0.29 % (3923110)Time elapsed: 0.036 s
% 0.18/0.29 % (3923110)Peak memory usage: 13 MB
% 0.18/0.29 % (3923110)Instructions burned: 133 (million)
% 0.18/0.29 % (3923109) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3923100-3923109"...
% 0.18/0.29 % TRYING [6]
% 0.18/0.29 % (3923119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2349067329:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.18/0.29 % (3923109)...printing done.
% 0.18/0.29 % (3923109)Refutation found. Thanks to Tanya!
% 0.18/0.29 % SZS status Unsatisfiable for theBenchmark
% 0.18/0.29 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.30 % (3923109)------------------------------
% 0.18/0.30 % (3923109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (3923109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (3923109)CaDiCaL version: 2.1.3
% 0.18/0.30 % (3923109)Termination reason: Refutation
% 0.18/0.30 % (3923109)Time elapsed: 0.039 s
% 0.18/0.30 % (3923109)Peak memory usage: 13 MB
% 0.18/0.30 % (3923109)Instructions burned: 72 (million)
% 0.18/0.30 % (3923100)Success in time 0.074 s
% 0.18/0.30 % Vampire exiting
%------------------------------------------------------------------------------