%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:23:43 AM UTC 2026
% Result : Unsatisfiable 0.21s 0.32s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 57
% Syntax : Number of formulae : 580 ( 58 unt; 46 def)
% Number of atoms : 1678 ( 582 equ)
% Maximal formula atoms : 64 ( 2 avg)
% Number of connectives : 1828 ( 730 ~; 916 |; 139 &)
% ( 43 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 47 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(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
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/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op(op(e0,e0),e0) = e0
& op(op(e0,e1),e0) = e1
& op(op(e0,e2),e0) = e2
& op(op(e0,e3),e0) = e3
& op(op(e1,e0),e1) = e0
& op(op(e1,e1),e1) = e1
& op(op(e1,e2),e1) = e2
& op(op(e1,e3),e1) = e3
& op(op(e2,e0),e2) = e0
& op(op(e2,e1),e2) = e1
& op(op(e2,e2),e2) = e2
& op(op(e2,e3),e2) = e3
& op(op(e3,e0),e3) = e0
& op(op(e3,e1),e3) = e1
& op(op(e3,e2),e3) = e2
& op(op(e3,e3),e3) = e3
& ( ( op(e0,op(e0,e0)) = op(e0,e0)
& op(e0,op(e1,e0)) = op(e1,e0)
& op(e0,op(e2,e0)) = op(e2,e0)
& op(e0,op(e3,e0)) = op(e3,e0) )
| ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f8,axiom,
~ ( e0 = op(op(e1,e2),op(e1,e2))
& e3 = op(e1,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f12,axiom,
~ ( e1 = op(op(e2,e0),op(e2,e0))
& e3 = op(e2,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e1 = op(op(e0,e2),op(e0,e2))
& e3 = op(e0,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f18,axiom,
~ ( e2 = op(op(e1,e0),op(e1,e0))
& e3 = op(e1,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f24,axiom,
~ ( e3 = op(op(e1,e0),op(e1,e0))
& e2 = op(e1,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f27,axiom,
~ ( e3 = op(op(e2,e1),op(e2,e1))
& e0 = op(e2,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
~ ( e3 = op(op(e0,e2),op(e0,e2))
& e1 = op(e0,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f32,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| e3 != op(e1,e2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f36,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| e3 != op(e2,e0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( e1 != op(op(e0,e2),op(e0,e2))
| e3 != op(e0,e2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f42,plain,
( e2 != op(op(e1,e0),op(e1,e0))
| e3 != op(e1,e0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f48,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| e2 != op(e1,e0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f51,plain,
( e3 != op(op(e2,e1),op(e2,e1))
| e0 != op(e2,e1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f52,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| e1 != op(e0,e2) ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,definition,
( ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,plain,
( op(op(e0,e0),e0) = e0
& op(op(e0,e1),e0) = e1
& op(op(e0,e2),e0) = e2
& op(op(e0,e3),e0) = e3
& op(op(e1,e0),e1) = e0
& op(op(e1,e1),e1) = e1
& op(op(e1,e2),e1) = e2
& op(op(e1,e3),e1) = e3
& op(op(e2,e0),e2) = e0
& op(op(e2,e1),e2) = e1
& op(op(e2,e2),e2) = e2
& op(op(e2,e3),e2) = e3
& op(op(e3,e0),e3) = e0
& op(op(e3,e1),e3) = e1
& op(op(e3,e2),e3) = e2
& op(op(e3,e3),e3) = e3
& ( ( op(e0,op(e0,e0)) = op(e0,e0)
& op(e0,op(e1,e0)) = op(e1,e0)
& op(e0,op(e2,e0)) = op(e2,e0)
& op(e0,op(e3,e0)) = op(e3,e0) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f5,f56,f55,f54]) ).
fof(f58,plain,
( ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f59,plain,
( ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f60,plain,
( ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f61,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f62,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f109,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f113,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f158,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
( op(e3,e1) = op(e1,op(e3,e1))
| ~ sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f164,plain,
( op(e2,e1) = op(e1,op(e2,e1))
| ~ sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f167,plain,
( op(e3,e2) = op(e2,op(e3,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f168,plain,
( op(e2,e2) = op(e2,op(e2,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f169,plain,
( op(e1,e2) = op(e2,op(e1,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f171,plain,
( op(e3,e3) = op(e3,op(e3,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f172,plain,
( op(e2,e3) = op(e3,op(e2,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f173,plain,
( op(e1,e3) = op(e3,op(e1,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f174,plain,
( op(e0,e3) = op(e3,op(e0,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f175,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f177,plain,
( op(e1,e0) = op(e0,op(e1,e0))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f179,plain,
e3 = op(op(e3,e3),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f180,plain,
e2 = op(op(e3,e2),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f181,plain,
e1 = op(op(e3,e1),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f182,plain,
e0 = op(op(e3,e0),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f183,plain,
e3 = op(op(e2,e3),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f185,plain,
e1 = op(op(e2,e1),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f186,plain,
e0 = op(op(e2,e0),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f187,plain,
e3 = op(op(e1,e3),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f188,plain,
e2 = op(op(e1,e2),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f190,plain,
e0 = op(op(e1,e0),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f191,plain,
e3 = op(op(e0,e3),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f192,plain,
e2 = op(op(e0,e2),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f193,plain,
e1 = op(op(e0,e1),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f197,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| e3 != op(e1,e2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f201,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| e3 != op(e2,e0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f203,plain,
( e1 != op(op(e0,e2),op(e0,e2))
| e3 != op(e0,e2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f207,plain,
( e2 != op(op(e1,e0),op(e1,e0))
| e3 != op(e1,e0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f213,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| e2 != op(e1,e0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f216,plain,
( e3 != op(op(e2,e1),op(e2,e1))
| e0 != op(e2,e1) ),
inference(cnf_transformation,[],[f51]) ).
fof(f217,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| e1 != op(e0,e2) ),
inference(cnf_transformation,[],[f52]) ).
fof(f220,definition,
( spl3_1
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f222,plain,
( e3 != op(e2,e1)
| spl3_1 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f229,definition,
( spl3_3
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f230,plain,
( e2 = op(e3,e1)
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f231,plain,
( e2 != op(e3,e1)
| spl3_3 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f238,definition,
( spl3_5
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f239,plain,
( e3 = op(e1,e2)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( e3 != op(e1,e2)
| spl3_5 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl3_6
<=> e0 = op(op(e1,e2),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f244,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| spl3_6 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f245,plain,
( ~ spl3_5
| ~ spl3_6 ),
inference(avatar_split_clause,[],[f197,f242,f238]) ).
fof(f247,definition,
( spl3_7
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f248,plain,
( e1 = op(e3,e2)
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( e1 != op(e3,e2)
| spl3_7 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f256,definition,
( spl3_9
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f257,plain,
( e2 = op(e1,e3)
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( e2 != op(e1,e3)
| spl3_9 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f265,definition,
( spl3_11
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition]) ).
fof(f266,plain,
( e1 = op(e2,e3)
| ~ spl3_11 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f267,plain,
( e1 != op(e2,e3)
| spl3_11 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f274,definition,
( spl3_13
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f275,plain,
( e3 = op(e2,e0)
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f276,plain,
( e3 != op(e2,e0)
| spl3_13 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f278,definition,
( spl3_14
<=> e1 = op(op(e2,e0),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_14])],[avatar_definition]) ).
fof(f280,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| spl3_14 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,plain,
( ~ spl3_13
| ~ spl3_14 ),
inference(avatar_split_clause,[],[f201,f278,f274]) ).
fof(f283,definition,
( spl3_15
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f284,plain,
( e2 = op(e3,e0)
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f285,plain,
( e2 != op(e3,e0)
| spl3_15 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f292,definition,
( spl3_17
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f293,plain,
( e3 = op(e0,e2)
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( e3 != op(e0,e2)
| spl3_17 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f296,definition,
( spl3_18
<=> e1 = op(op(e0,e2),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f298,plain,
( e1 != op(op(e0,e2),op(e0,e2))
| spl3_18 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f299,plain,
( ~ spl3_17
| ~ spl3_18 ),
inference(avatar_split_clause,[],[f203,f296,f292]) ).
fof(f301,definition,
( spl3_19
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f302,plain,
( e0 = op(e3,e2)
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( e0 != op(e3,e2)
| spl3_19 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f310,definition,
( spl3_21
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f311,plain,
( e2 = op(e0,e3)
| ~ spl3_21 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f312,plain,
( e2 != op(e0,e3)
| spl3_21 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f319,definition,
( spl3_23
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition]) ).
fof(f320,plain,
( e0 = op(e2,e3)
| ~ spl3_23 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( e0 != op(e2,e3)
| spl3_23 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f328,definition,
( spl3_25
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_25])],[avatar_definition]) ).
fof(f329,plain,
( e3 = op(e1,e0)
| ~ spl3_25 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f330,plain,
( e3 != op(e1,e0)
| spl3_25 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f332,definition,
( spl3_26
<=> e2 = op(op(e1,e0),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_26])],[avatar_definition]) ).
fof(f334,plain,
( e2 != op(op(e1,e0),op(e1,e0))
| spl3_26 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,plain,
( ~ spl3_25
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f207,f332,f328]) ).
fof(f337,definition,
( spl3_27
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f338,plain,
( e1 = op(e3,e0)
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f339,plain,
( e1 != op(e3,e0)
| spl3_27 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f355,definition,
( spl3_31
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f356,plain,
( e0 = op(e3,e1)
| ~ spl3_31 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f357,plain,
( e0 != op(e3,e1)
| spl3_31 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f364,definition,
( spl3_33
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition]) ).
fof(f365,plain,
( e1 = op(e0,e3)
| ~ spl3_33 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( e1 != op(e0,e3)
| spl3_33 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f382,definition,
( spl3_37
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f384,plain,
( e2 != op(e1,e0)
| spl3_37 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f386,definition,
( spl3_38
<=> e3 = op(op(e1,e0),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_38])],[avatar_definition]) ).
fof(f388,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| spl3_38 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f389,plain,
( ~ spl3_37
| ~ spl3_38 ),
inference(avatar_split_clause,[],[f213,f386,f382]) ).
fof(f409,definition,
( spl3_43
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_43])],[avatar_definition]) ).
fof(f410,plain,
( e0 = op(e2,e1)
| ~ spl3_43 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f411,plain,
( e0 != op(e2,e1)
| spl3_43 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl3_44
<=> e3 = op(op(e2,e1),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_44])],[avatar_definition]) ).
fof(f415,plain,
( e3 != op(op(e2,e1),op(e2,e1))
| spl3_44 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,plain,
( ~ spl3_43
| ~ spl3_44 ),
inference(avatar_split_clause,[],[f216,f413,f409]) ).
fof(f418,definition,
( spl3_45
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f419,plain,
( e1 = op(e0,e2)
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( e1 != op(e0,e2)
| spl3_45 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f422,definition,
( spl3_46
<=> e3 = op(op(e0,e2),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_46])],[avatar_definition]) ).
fof(f424,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| spl3_46 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f425,plain,
( ~ spl3_45
| ~ spl3_46 ),
inference(avatar_split_clause,[],[f217,f422,f418]) ).
fof(f436,definition,
( spl3_49
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition]) ).
fof(f437,plain,
( sP2
| ~ spl3_49 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f438,plain,
( ~ sP2
| spl3_49 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f440,definition,
( spl3_50
<=> op(e3,e1) = op(e1,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_50])],[avatar_definition]) ).
fof(f441,plain,
( op(e3,e1) != op(e1,op(e3,e1))
| spl3_50 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f442,plain,
( op(e3,e1) = op(e1,op(e3,e1))
| ~ spl3_50 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f443,plain,
( ~ spl3_49
| spl3_50 ),
inference(avatar_split_clause,[],[f163,f440,f436]) ).
fof(f445,definition,
( spl3_51
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f447,plain,
( ~ sP1
| spl3_51 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f449,definition,
( spl3_52
<=> op(e3,e2) = op(e2,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f451,plain,
( op(e3,e2) = op(e2,op(e3,e2))
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f452,plain,
( ~ spl3_51
| spl3_52 ),
inference(avatar_split_clause,[],[f167,f449,f445]) ).
fof(f454,definition,
( spl3_53
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl3_53])],[avatar_definition]) ).
fof(f455,plain,
( sP0
| ~ spl3_53 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f456,plain,
( ~ sP0
| spl3_53 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f458,definition,
( spl3_54
<=> op(e3,e3) = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_54])],[avatar_definition]) ).
fof(f460,plain,
( op(e3,e3) = op(e3,op(e3,e3))
| ~ spl3_54 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f461,plain,
( ~ spl3_53
| spl3_54 ),
inference(avatar_split_clause,[],[f171,f458,f454]) ).
fof(f462,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP1
| sP0
| spl3_49 ),
inference(forward_subsumption_resolution,[],[f175,f438]) ).
fof(f463,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP0
| spl3_49
| spl3_51 ),
inference(forward_subsumption_resolution,[],[f462,f447]) ).
fof(f464,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f463,f456]) ).
fof(f468,plain,
( op(e1,e0) = op(e0,op(e1,e0))
| sP1
| sP0
| spl3_49 ),
inference(forward_subsumption_resolution,[],[f177,f438]) ).
fof(f469,plain,
( op(e1,e0) = op(e0,op(e1,e0))
| sP0
| spl3_49
| spl3_51 ),
inference(forward_subsumption_resolution,[],[f468,f447]) ).
fof(f470,plain,
( op(e1,e0) = op(e0,op(e1,e0))
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f469,f456]) ).
fof(f475,definition,
( spl3_55
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_55])],[avatar_definition]) ).
fof(f477,plain,
( e3 = op(e3,e3)
| ~ spl3_55 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl3_56
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition]) ).
fof(f480,plain,
( e2 != op(e3,e3)
| spl3_56 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f481,plain,
( e2 = op(e3,e3)
| ~ spl3_56 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f483,definition,
( spl3_57
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_57])],[avatar_definition]) ).
fof(f484,plain,
( e1 != op(e3,e3)
| spl3_57 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( e1 = op(e3,e3)
| ~ spl3_57 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f487,definition,
( spl3_58
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_58])],[avatar_definition]) ).
fof(f489,plain,
( e0 = op(e3,e3)
| ~ spl3_58 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f490,plain,
( spl3_55
| spl3_56
| spl3_57
| spl3_58 ),
inference(avatar_split_clause,[],[f61,f487,f483,f479,f475]) ).
fof(f492,plain,
( e3 != op(e3,e1)
| ~ spl3_55 ),
inference(superposition,[],[f110,f477]) ).
fof(f493,plain,
( e3 != op(e3,e0)
| ~ spl3_55 ),
inference(superposition,[],[f112,f477]) ).
fof(f496,plain,
( e3 != op(e0,e3)
| ~ spl3_55 ),
inference(superposition,[],[f136,f477]) ).
fof(f498,plain,
( e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl3_19 ),
inference(forward_subsumption_resolution,[],[f62,f303]) ).
fof(f499,plain,
( e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl3_7
| spl3_19 ),
inference(forward_subsumption_resolution,[],[f498,f249]) ).
fof(f525,plain,
( e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1)
| spl3_31 ),
inference(forward_subsumption_resolution,[],[f63,f357]) ).
fof(f526,plain,
( e1 = op(e3,e1)
| e3 = op(e3,e1)
| spl3_3
| spl3_31 ),
inference(forward_subsumption_resolution,[],[f525,f231]) ).
fof(f527,plain,
( e1 = op(e3,e1)
| spl3_3
| spl3_31
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f526,f492]) ).
fof(f528,plain,
( e1 != op(e3,e0)
| spl3_3
| spl3_31
| ~ spl3_55 ),
inference(superposition,[],[f114,f527]) ).
fof(f548,plain,
( e0 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f64,f339]) ).
fof(f549,plain,
( e0 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_15
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f548,f285]) ).
fof(f550,plain,
( e0 = op(e3,e0)
| spl3_15
| spl3_27
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f549,f493]) ).
fof(f553,plain,
( e0 != op(e0,e0)
| spl3_15
| spl3_27
| ~ spl3_55 ),
inference(superposition,[],[f154,f550]) ).
fof(f557,plain,
( e0 = op(e0,e0)
| spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(superposition,[],[f464,f550]) ).
fof(f566,plain,
( $false
| spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f557,f553]) ).
fof(f567,plain,
( spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(avatar_contradiction_clause,[],[f566]) ).
fof(f570,plain,
( ~ spl3_27
| spl3_3
| spl3_31
| ~ spl3_55 ),
inference(avatar_split_clause,[],[f528,f475,f355,f229,f337]) ).
fof(f588,plain,
( e1 = op(e0,e3)
| ~ spl3_31 ),
inference(superposition,[],[f181,f356]) ).
fof(f593,plain,
( $false
| ~ spl3_31
| spl3_33 ),
inference(forward_subsumption_resolution,[],[f588,f366]) ).
fof(f594,plain,
( ~ spl3_31
| spl3_33 ),
inference(avatar_contradiction_clause,[],[f593]) ).
fof(f599,plain,
( e3 = op(e1,e0)
| ~ spl3_33 ),
inference(superposition,[],[f191,f365]) ).
fof(f603,plain,
( $false
| spl3_25
| ~ spl3_33 ),
inference(forward_subsumption_resolution,[],[f599,f330]) ).
fof(f604,plain,
( spl3_25
| ~ spl3_33 ),
inference(avatar_contradiction_clause,[],[f603]) ).
fof(f609,plain,
( e3 = op(e0,e3)
| ~ spl3_25
| spl3_49
| spl3_51
| spl3_53 ),
inference(superposition,[],[f470,f329]) ).
fof(f611,plain,
( $false
| ~ spl3_25
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f609,f496]) ).
fof(f612,plain,
( ~ spl3_25
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(avatar_contradiction_clause,[],[f611]) ).
fof(f616,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| sP0
| spl3_51 ),
inference(forward_subsumption_resolution,[],[f175,f447]) ).
fof(f620,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f616,f456]) ).
fof(f626,plain,
( e2 != op(e3,e3)
| ~ spl3_25
| spl3_26 ),
inference(superposition,[],[f334,f329]) ).
fof(f632,plain,
( e0 != op(e0,e1)
| ~ spl3_31 ),
inference(superposition,[],[f148,f356]) ).
fof(f675,plain,
( e0 = op(e1,e0)
| ~ spl3_31
| ~ spl3_50 ),
inference(forward_demodulation,[],[f442,f356]) ).
fof(f678,plain,
( e0 = op(e0,e1)
| ~ spl3_31
| ~ spl3_50 ),
inference(superposition,[],[f190,f675]) ).
fof(f684,plain,
( $false
| ~ spl3_31
| ~ spl3_50 ),
inference(forward_subsumption_resolution,[],[f678,f632]) ).
fof(f685,plain,
( ~ spl3_31
| ~ spl3_50 ),
inference(avatar_contradiction_clause,[],[f684]) ).
fof(f690,plain,
( ~ spl3_56
| ~ spl3_25
| spl3_26 ),
inference(avatar_split_clause,[],[f626,f332,f328,f479]) ).
fof(f692,plain,
( e0 != op(e3,e1)
| ~ spl3_58 ),
inference(superposition,[],[f110,f489]) ).
fof(f704,plain,
( $false
| ~ spl3_31
| ~ spl3_58 ),
inference(forward_subsumption_resolution,[],[f692,f356]) ).
fof(f705,plain,
( ~ spl3_31
| ~ spl3_58 ),
inference(avatar_contradiction_clause,[],[f704]) ).
fof(f709,plain,
( e1 != op(e3,e1)
| ~ spl3_57 ),
inference(superposition,[],[f110,f485]) ).
fof(f710,plain,
( e1 != op(e3,e0)
| ~ spl3_57 ),
inference(superposition,[],[f112,f485]) ).
fof(f714,plain,
( e3 = op(e1,e3)
| ~ spl3_57 ),
inference(superposition,[],[f179,f485]) ).
fof(f722,plain,
( $false
| ~ spl3_27
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f710,f338]) ).
fof(f723,plain,
( ~ spl3_27
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f722]) ).
fof(f727,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e3 = op(e3,e1)
| spl3_3 ),
inference(forward_subsumption_resolution,[],[f63,f231]) ).
fof(f728,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_15 ),
inference(forward_subsumption_resolution,[],[f64,f285]) ).
fof(f735,plain,
( e3 = op(e3,e1)
| ~ spl3_57 ),
inference(superposition,[],[f187,f714]) ).
fof(f740,plain,
( e3 != op(e3,e0)
| ~ spl3_57 ),
inference(superposition,[],[f114,f735]) ).
fof(f741,plain,
( e3 != op(e2,e1)
| ~ spl3_57 ),
inference(superposition,[],[f145,f735]) ).
fof(f749,plain,
( e3 != op(e1,e3)
| spl3_50
| ~ spl3_57 ),
inference(superposition,[],[f441,f735]) ).
fof(f751,plain,
( $false
| spl3_50
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f749,f714]) ).
fof(f752,plain,
( spl3_50
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f751]) ).
fof(f755,definition,
( spl3_59
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_59])],[avatar_definition]) ).
fof(f757,plain,
( e3 = op(e3,e2)
| ~ spl3_59 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f759,definition,
( spl3_60
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_60])],[avatar_definition]) ).
fof(f760,plain,
( e2 != op(e3,e2)
| spl3_60 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f761,plain,
( e2 = op(e3,e2)
| ~ spl3_60 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f762,plain,
( spl3_59
| spl3_60
| spl3_7
| spl3_19 ),
inference(avatar_split_clause,[],[f499,f301,f247,f759,f755]) ).
fof(f763,plain,
( e3 != op(e3,e1)
| ~ spl3_59 ),
inference(superposition,[],[f111,f757]) ).
fof(f768,plain,
( e2 = op(e3,e3)
| ~ spl3_59 ),
inference(superposition,[],[f180,f757]) ).
fof(f771,plain,
( $false
| spl3_56
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f768,f480]) ).
fof(f772,plain,
( spl3_56
| ~ spl3_59 ),
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f773,plain,
( $false
| ~ spl3_57
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f763,f735]) ).
fof(f774,plain,
( ~ spl3_57
| ~ spl3_59 ),
inference(avatar_contradiction_clause,[],[f773]) ).
fof(f780,plain,
( e2 = op(e2,e3)
| ~ spl3_60 ),
inference(superposition,[],[f180,f761]) ).
fof(f785,plain,
( e2 != op(e2,e1)
| ~ spl3_60 ),
inference(superposition,[],[f116,f780]) ).
fof(f798,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f620,f438]) ).
fof(f802,plain,
( e0 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_15
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f728,f339]) ).
fof(f803,plain,
( e0 = op(e3,e0)
| spl3_15
| spl3_27
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f802,f740]) ).
fof(f806,plain,
( e0 != op(e0,e0)
| spl3_15
| spl3_27
| ~ spl3_57 ),
inference(superposition,[],[f154,f803]) ).
fof(f807,plain,
( e0 = op(e0,e3)
| spl3_15
| spl3_27
| ~ spl3_57 ),
inference(superposition,[],[f182,f803]) ).
fof(f813,plain,
( e0 = op(e0,e0)
| spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_57 ),
inference(superposition,[],[f798,f803]) ).
fof(f817,plain,
( op(e0,e0) = e3
| spl3_15
| spl3_27
| ~ spl3_57 ),
inference(superposition,[],[f191,f807]) ).
fof(f822,plain,
( $false
| spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f813,f806]) ).
fof(f823,plain,
( spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f830,plain,
( op(e2,e1) = op(e1,op(e2,e1))
| ~ spl3_49 ),
inference(forward_subsumption_resolution,[],[f164,f437]) ).
fof(f833,plain,
( e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| spl3_43 ),
inference(forward_subsumption_resolution,[],[f67,f411]) ).
fof(f834,plain,
( e1 = op(e2,e1)
| e3 = op(e2,e1)
| spl3_43
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f833,f785]) ).
fof(f835,plain,
( e1 = op(e2,e1)
| spl3_1
| spl3_43
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f834,f222]) ).
fof(f837,plain,
( e1 != op(e1,e1)
| spl3_1
| spl3_43
| ~ spl3_60 ),
inference(superposition,[],[f147,f835]) ).
fof(f843,plain,
( e1 = op(e1,e1)
| spl3_1
| spl3_43
| ~ spl3_49
| ~ spl3_60 ),
inference(superposition,[],[f830,f835]) ).
fof(f851,plain,
( $false
| spl3_1
| spl3_43
| ~ spl3_49
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f843,f837]) ).
fof(f852,plain,
( spl3_1
| spl3_43
| ~ spl3_49
| ~ spl3_60 ),
inference(avatar_contradiction_clause,[],[f851]) ).
fof(f863,plain,
( e2 = op(e0,e3)
| ~ spl3_19 ),
inference(superposition,[],[f180,f302]) ).
fof(f868,plain,
( $false
| ~ spl3_19
| spl3_21 ),
inference(forward_subsumption_resolution,[],[f863,f312]) ).
fof(f869,plain,
( ~ spl3_19
| spl3_21 ),
inference(avatar_contradiction_clause,[],[f868]) ).
fof(f872,plain,
( ~ spl3_1
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f741,f483,f220]) ).
fof(f876,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| spl3_1 ),
inference(forward_subsumption_resolution,[],[f67,f222]) ).
fof(f880,plain,
( e1 = op(e0,e2)
| ~ spl3_43 ),
inference(superposition,[],[f185,f410]) ).
fof(f883,plain,
( op(e0,e0) != e3
| ~ spl3_43
| spl3_44 ),
inference(superposition,[],[f415,f410]) ).
fof(f887,plain,
( $false
| spl3_15
| spl3_27
| ~ spl3_43
| spl3_44
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f883,f817]) ).
fof(f888,plain,
( spl3_15
| spl3_27
| ~ spl3_43
| spl3_44
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f887]) ).
fof(f889,plain,
( $false
| ~ spl3_43
| spl3_45 ),
inference(forward_subsumption_resolution,[],[f880,f420]) ).
fof(f890,plain,
( ~ spl3_43
| spl3_45 ),
inference(avatar_contradiction_clause,[],[f889]) ).
fof(f896,plain,
( e0 = op(e2,e3)
| ~ spl3_15 ),
inference(superposition,[],[f182,f284]) ).
fof(f901,plain,
( $false
| ~ spl3_15
| spl3_23 ),
inference(forward_subsumption_resolution,[],[f896,f321]) ).
fof(f902,plain,
( ~ spl3_15
| spl3_23 ),
inference(avatar_contradiction_clause,[],[f901]) ).
fof(f905,plain,
( e0 != op(e2,e1)
| ~ spl3_23 ),
inference(superposition,[],[f116,f320]) ).
fof(f909,plain,
( e3 = op(e0,e2)
| ~ spl3_23 ),
inference(superposition,[],[f183,f320]) ).
fof(f912,plain,
( $false
| spl3_17
| ~ spl3_23 ),
inference(forward_subsumption_resolution,[],[f909,f294]) ).
fof(f913,plain,
( spl3_17
| ~ spl3_23 ),
inference(avatar_contradiction_clause,[],[f912]) ).
fof(f914,plain,
( $false
| ~ spl3_23
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f905,f410]) ).
fof(f915,plain,
( ~ spl3_23
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f914]) ).
fof(f921,plain,
( e1 != op(e3,e3)
| ~ spl3_17
| spl3_18 ),
inference(superposition,[],[f298,f293]) ).
fof(f923,plain,
( $false
| ~ spl3_17
| spl3_18
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f921,f485]) ).
fof(f924,plain,
( ~ spl3_17
| spl3_18
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f923]) ).
fof(f925,plain,
( e1 = op(e3,e1)
| ~ spl3_54
| ~ spl3_57 ),
inference(forward_demodulation,[],[f460,f485]) ).
fof(f927,plain,
( $false
| ~ spl3_54
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f925,f709]) ).
fof(f928,plain,
( ~ spl3_54
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f927]) ).
fof(f934,plain,
( e3 = op(e2,e0)
| ~ spl3_21 ),
inference(superposition,[],[f191,f311]) ).
fof(f939,plain,
( $false
| spl3_13
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f934,f276]) ).
fof(f940,plain,
( spl3_13
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f939]) ).
fof(f944,plain,
( e1 != op(e3,e3)
| ~ spl3_13
| spl3_14 ),
inference(superposition,[],[f280,f275]) ).
fof(f946,plain,
( $false
| ~ spl3_13
| spl3_14
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f944,f485]) ).
fof(f947,plain,
( ~ spl3_13
| spl3_14
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f946]) ).
fof(f952,plain,
( e2 = op(e1,e0)
| ~ spl3_45 ),
inference(superposition,[],[f192,f419]) ).
fof(f956,plain,
( $false
| spl3_37
| ~ spl3_45 ),
inference(forward_subsumption_resolution,[],[f952,f384]) ).
fof(f957,plain,
( spl3_37
| ~ spl3_45 ),
inference(avatar_contradiction_clause,[],[f956]) ).
fof(f958,plain,
( e2 != op(e3,e1)
| ~ spl3_60 ),
inference(superposition,[],[f111,f761]) ).
fof(f960,plain,
( e2 != op(e2,e2)
| ~ spl3_60 ),
inference(superposition,[],[f139,f761]) ).
fof(f963,plain,
( e2 = op(e2,e3)
| ~ spl3_60 ),
inference(superposition,[],[f180,f761]) ).
fof(f970,plain,
( e2 != op(e2,e1)
| ~ spl3_60 ),
inference(superposition,[],[f116,f963]) ).
fof(f974,plain,
( e3 = op(e2,e2)
| ~ spl3_60 ),
inference(superposition,[],[f183,f963]) ).
fof(f978,plain,
( e3 != op(e2,e1)
| ~ spl3_60 ),
inference(superposition,[],[f117,f974]) ).
fof(f986,plain,
( e2 = op(e2,e2)
| ~ spl3_52
| ~ spl3_60 ),
inference(forward_demodulation,[],[f451,f761]) ).
fof(f987,plain,
( $false
| ~ spl3_52
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f986,f960]) ).
fof(f988,plain,
( ~ spl3_52
| ~ spl3_60 ),
inference(avatar_contradiction_clause,[],[f987]) ).
fof(f990,plain,
( e1 = op(e3,e1)
| e3 = op(e3,e1)
| spl3_3
| spl3_31 ),
inference(forward_subsumption_resolution,[],[f727,f357]) ).
fof(f1042,definition,
( spl3_61
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_61])],[avatar_definition]) ).
fof(f1044,plain,
( e3 = op(e3,e1)
| ~ spl3_61 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1046,definition,
( spl3_62
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_62])],[avatar_definition]) ).
fof(f1047,plain,
( e1 != op(e3,e1)
| spl3_62 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1048,plain,
( e1 = op(e3,e1)
| ~ spl3_62 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1049,plain,
( spl3_61
| spl3_62
| spl3_3
| spl3_31 ),
inference(avatar_split_clause,[],[f990,f355,f229,f1046,f1042]) ).
fof(f1054,plain,
( e1 = op(e3,e3)
| ~ spl3_61 ),
inference(superposition,[],[f181,f1044]) ).
fof(f1062,plain,
( $false
| spl3_57
| ~ spl3_61 ),
inference(forward_subsumption_resolution,[],[f1054,f484]) ).
fof(f1063,plain,
( spl3_57
| ~ spl3_61 ),
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1067,plain,
( e1 != op(e2,e1)
| ~ spl3_62 ),
inference(superposition,[],[f145,f1048]) ).
fof(f1068,plain,
( e1 != op(e1,e1)
| ~ spl3_62 ),
inference(superposition,[],[f146,f1048]) ).
fof(f1075,plain,
( e1 = op(e1,e1)
| ~ spl3_50
| ~ spl3_62 ),
inference(superposition,[],[f442,f1048]) ).
fof(f1085,plain,
( $false
| ~ spl3_50
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1075,f1068]) ).
fof(f1086,plain,
( ~ spl3_50
| ~ spl3_62 ),
inference(avatar_contradiction_clause,[],[f1085]) ).
fof(f1094,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP1
| sP0
| spl3_49 ),
inference(forward_subsumption_resolution,[],[f175,f438]) ).
fof(f1095,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP0
| spl3_49
| spl3_51 ),
inference(forward_subsumption_resolution,[],[f1094,f447]) ).
fof(f1107,plain,
( e1 = op(e2,e1)
| e2 = op(e2,e1)
| spl3_1
| spl3_43 ),
inference(forward_subsumption_resolution,[],[f876,f411]) ).
fof(f1108,plain,
( e2 = op(e2,e1)
| spl3_1
| spl3_43
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1107,f1067]) ).
fof(f1109,plain,
( $false
| spl3_1
| spl3_43
| ~ spl3_60
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1108,f970]) ).
fof(f1110,plain,
( spl3_1
| spl3_43
| ~ spl3_60
| ~ spl3_62 ),
inference(avatar_contradiction_clause,[],[f1109]) ).
fof(f1114,plain,
( ~ spl3_3
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f958,f759,f229]) ).
fof(f1128,plain,
( ~ spl3_1
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f978,f759,f220]) ).
fof(f1151,plain,
( e3 != op(e1,e1)
| ~ spl3_45
| spl3_46 ),
inference(superposition,[],[f424,f419]) ).
fof(f1153,plain,
( e2 != op(e3,e1)
| ~ spl3_56 ),
inference(superposition,[],[f110,f481]) ).
fof(f1178,plain,
( e1 = op(e1,e3)
| ~ spl3_62 ),
inference(superposition,[],[f181,f1048]) ).
fof(f1211,plain,
( e3 = op(e1,e1)
| ~ spl3_62 ),
inference(superposition,[],[f187,f1178]) ).
fof(f1216,plain,
( $false
| ~ spl3_45
| spl3_46
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1211,f1151]) ).
fof(f1217,plain,
( ~ spl3_45
| spl3_46
| ~ spl3_62 ),
inference(avatar_contradiction_clause,[],[f1216]) ).
fof(f1219,plain,
( ~ spl3_3
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1153,f479,f229]) ).
fof(f1226,plain,
( e1 = op(e2,e3)
| ~ spl3_3 ),
inference(superposition,[],[f181,f230]) ).
fof(f1233,plain,
( $false
| ~ spl3_3
| spl3_11 ),
inference(forward_subsumption_resolution,[],[f1226,f267]) ).
fof(f1234,plain,
( ~ spl3_3
| spl3_11 ),
inference(avatar_contradiction_clause,[],[f1233]) ).
fof(f1242,plain,
( e2 = op(e1,e3)
| ~ spl3_7 ),
inference(superposition,[],[f180,f248]) ).
fof(f1248,plain,
( $false
| ~ spl3_7
| spl3_9 ),
inference(forward_subsumption_resolution,[],[f1242,f258]) ).
fof(f1249,plain,
( ~ spl3_7
| spl3_9 ),
inference(avatar_contradiction_clause,[],[f1248]) ).
fof(f1259,plain,
( e3 = op(e1,e2)
| ~ spl3_11 ),
inference(superposition,[],[f183,f266]) ).
fof(f1263,plain,
( $false
| spl3_5
| ~ spl3_11 ),
inference(forward_subsumption_resolution,[],[f1259,f240]) ).
fof(f1264,plain,
( spl3_5
| ~ spl3_11 ),
inference(avatar_contradiction_clause,[],[f1263]) ).
fof(f1270,plain,
( e0 != op(e3,e3)
| ~ spl3_5
| spl3_6 ),
inference(superposition,[],[f244,f239]) ).
fof(f1273,plain,
( ~ spl3_58
| ~ spl3_5
| spl3_6 ),
inference(avatar_split_clause,[],[f1270,f242,f238,f487]) ).
fof(f1297,plain,
( e0 != op(e3,e2)
| ~ spl3_58 ),
inference(superposition,[],[f109,f489]) ).
fof(f1310,plain,
( $false
| ~ spl3_19
| ~ spl3_58 ),
inference(forward_subsumption_resolution,[],[f1297,f302]) ).
fof(f1311,plain,
( ~ spl3_19
| ~ spl3_58 ),
inference(avatar_contradiction_clause,[],[f1310]) ).
fof(f1314,plain,
( e1 != op(e3,e1)
| ~ spl3_7 ),
inference(superposition,[],[f111,f248]) ).
fof(f1325,plain,
( ~ spl3_62
| ~ spl3_7 ),
inference(avatar_split_clause,[],[f1314,f247,f1046]) ).
fof(f1344,plain,
( e0 != op(e0,e2)
| ~ spl3_19 ),
inference(superposition,[],[f142,f302]) ).
fof(f1351,plain,
( e2 != op(e0,e2)
| ~ spl3_21 ),
inference(superposition,[],[f127,f311]) ).
fof(f1396,plain,
( e0 = op(e2,e0)
| ~ spl3_19
| ~ spl3_52 ),
inference(forward_demodulation,[],[f451,f302]) ).
fof(f1400,plain,
( e0 = op(e0,e2)
| ~ spl3_19
| ~ spl3_52 ),
inference(superposition,[],[f186,f1396]) ).
fof(f1406,plain,
( $false
| ~ spl3_19
| ~ spl3_52 ),
inference(forward_subsumption_resolution,[],[f1400,f1344]) ).
fof(f1407,plain,
( ~ spl3_19
| ~ spl3_52 ),
inference(avatar_contradiction_clause,[],[f1406]) ).
fof(f1416,plain,
( op(e0,e3) = op(e3,op(e0,e3))
| ~ spl3_53 ),
inference(forward_subsumption_resolution,[],[f174,f455]) ).
fof(f1417,plain,
( e2 = op(e3,e2)
| ~ spl3_21
| ~ spl3_53 ),
inference(forward_demodulation,[],[f1416,f311]) ).
fof(f1418,plain,
( $false
| ~ spl3_21
| ~ spl3_53
| spl3_60 ),
inference(forward_subsumption_resolution,[],[f1417,f760]) ).
fof(f1419,plain,
( ~ spl3_21
| ~ spl3_53
| spl3_60 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1460,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1095,f456]) ).
fof(f1461,plain,
( e2 = op(e0,e2)
| ~ spl3_15
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_demodulation,[],[f1460,f284]) ).
fof(f1462,plain,
( $false
| ~ spl3_15
| ~ spl3_21
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1461,f1351]) ).
fof(f1463,plain,
( ~ spl3_15
| ~ spl3_21
| spl3_49
| spl3_51
| spl3_53 ),
inference(avatar_contradiction_clause,[],[f1462]) ).
fof(f1464,plain,
( e0 = op(e3,e0)
| ~ sP0
| ~ spl3_23 ),
inference(forward_demodulation,[],[f172,f320]) ).
fof(f1467,plain,
( e0 = e2
| ~ sP0
| ~ spl3_15
| ~ spl3_23 ),
inference(forward_demodulation,[],[f1464,f284]) ).
fof(f1470,plain,
( ~ sP0
| ~ spl3_15
| ~ spl3_23 ),
inference(forward_subsumption_resolution,[],[f1467,f161]) ).
fof(f1472,plain,
( ~ spl3_53
| ~ spl3_15
| ~ spl3_23 ),
inference(avatar_split_clause,[],[f1470,f319,f283,f454]) ).
fof(f1490,plain,
( e3 = op(e2,e1)
| ~ spl3_9 ),
inference(superposition,[],[f187,f257]) ).
fof(f1499,plain,
( e3 != op(e3,e3)
| ~ spl3_25
| spl3_38 ),
inference(superposition,[],[f388,f329]) ).
fof(f1500,plain,
( $false
| ~ spl3_25
| spl3_38
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f1499,f477]) ).
fof(f1501,plain,
( ~ spl3_25
| spl3_38
| ~ spl3_55 ),
inference(avatar_contradiction_clause,[],[f1500]) ).
fof(f1527,plain,
( spl3_1
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f1490,f256,f220]) ).
fof(f1540,plain,
( op(e1,e3) = op(e3,op(e1,e3))
| ~ spl3_53 ),
inference(forward_subsumption_resolution,[],[f173,f455]) ).
fof(f1541,plain,
( e2 = op(e3,e2)
| ~ spl3_9
| ~ spl3_53 ),
inference(forward_demodulation,[],[f1540,f257]) ).
fof(f1542,plain,
( $false
| ~ spl3_9
| ~ spl3_53
| spl3_60 ),
inference(forward_subsumption_resolution,[],[f1541,f760]) ).
fof(f1543,plain,
( ~ spl3_9
| ~ spl3_53
| spl3_60 ),
inference(avatar_contradiction_clause,[],[f1542]) ).
fof(f1550,plain,
( e1 != op(e1,e2)
| ~ spl3_7 ),
inference(superposition,[],[f140,f248]) ).
fof(f1593,plain,
( e1 = op(e2,e1)
| ~ spl3_7
| ~ spl3_52 ),
inference(forward_demodulation,[],[f451,f248]) ).
fof(f1598,plain,
( e1 = op(e1,e2)
| ~ spl3_7
| ~ spl3_52 ),
inference(superposition,[],[f185,f1593]) ).
fof(f1604,plain,
( $false
| ~ spl3_7
| ~ spl3_52 ),
inference(forward_subsumption_resolution,[],[f1598,f1550]) ).
fof(f1605,plain,
( ~ spl3_7
| ~ spl3_52 ),
inference(avatar_contradiction_clause,[],[f1604]) ).
fof(f1620,plain,
( e2 != op(e3,e0)
| ~ spl3_3 ),
inference(superposition,[],[f114,f230]) ).
fof(f1621,plain,
( e2 != op(e2,e1)
| ~ spl3_3 ),
inference(superposition,[],[f145,f230]) ).
fof(f1632,plain,
( ~ spl3_15
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f1620,f229,f283]) ).
fof(f1635,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| sP0
| spl3_51 ),
inference(forward_subsumption_resolution,[],[f175,f447]) ).
fof(f1642,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1635,f456]) ).
fof(f1690,plain,
( e1 != op(e1,e0)
| ~ spl3_27 ),
inference(superposition,[],[f152,f338]) ).
fof(f1716,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1642,f438]) ).
fof(f1717,plain,
( e1 = op(e0,e1)
| ~ spl3_27
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_demodulation,[],[f1716,f338]) ).
fof(f1720,plain,
( e1 = op(e1,e0)
| ~ spl3_27
| spl3_49
| spl3_51
| spl3_53 ),
inference(superposition,[],[f193,f1717]) ).
fof(f1726,plain,
( $false
| ~ spl3_27
| spl3_49
| spl3_51
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1720,f1690]) ).
fof(f1727,plain,
( ~ spl3_27
| spl3_49
| spl3_51
| spl3_53 ),
inference(avatar_contradiction_clause,[],[f1726]) ).
fof(f1730,plain,
( e2 = op(e1,e2)
| ~ spl3_3
| ~ spl3_50 ),
inference(forward_demodulation,[],[f442,f230]) ).
fof(f1741,plain,
( e2 = op(e2,e1)
| ~ spl3_3
| ~ spl3_50 ),
inference(superposition,[],[f188,f1730]) ).
fof(f1747,plain,
( $false
| ~ spl3_3
| ~ spl3_50 ),
inference(forward_subsumption_resolution,[],[f1741,f1621]) ).
fof(f1748,plain,
( ~ spl3_3
| ~ spl3_50 ),
inference(avatar_contradiction_clause,[],[f1747]) ).
fof(f1753,plain,
( e0 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f64,f339]) ).
fof(f1754,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| sP1
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f175,f456]) ).
fof(f1758,plain,
( e3 = op(e2,e3)
| ~ sP1
| ~ spl3_5 ),
inference(forward_demodulation,[],[f169,f239]) ).
fof(f1760,plain,
( e1 = e3
| ~ sP1
| ~ spl3_5
| ~ spl3_11 ),
inference(forward_demodulation,[],[f1758,f266]) ).
fof(f1761,plain,
( ~ sP1
| ~ spl3_5
| ~ spl3_11 ),
inference(forward_subsumption_resolution,[],[f1760,f158]) ).
fof(f1762,plain,
( ~ spl3_51
| ~ spl3_5
| ~ spl3_11 ),
inference(avatar_split_clause,[],[f1761,f265,f238,f445]) ).
fof(f1791,plain,
( e2 != op(e3,e0)
| ~ spl3_56 ),
inference(superposition,[],[f112,f481]) ).
fof(f1794,plain,
( e2 != op(e0,e3)
| ~ spl3_56 ),
inference(superposition,[],[f136,f481]) ).
fof(f1795,plain,
( e3 = op(e2,e3)
| ~ spl3_56 ),
inference(superposition,[],[f179,f481]) ).
fof(f1801,plain,
( $false
| ~ spl3_15
| ~ spl3_56 ),
inference(forward_subsumption_resolution,[],[f1791,f284]) ).
fof(f1802,plain,
( ~ spl3_15
| ~ spl3_56 ),
inference(avatar_contradiction_clause,[],[f1801]) ).
fof(f1806,plain,
( e3 != op(e3,e0)
| ~ spl3_59 ),
inference(superposition,[],[f113,f757]) ).
fof(f1816,plain,
( e1 != op(e3,e0)
| ~ spl3_62 ),
inference(superposition,[],[f114,f1048]) ).
fof(f1817,plain,
( e1 != op(e2,e1)
| ~ spl3_62 ),
inference(superposition,[],[f145,f1048]) ).
fof(f1828,plain,
( e3 != op(e2,e1)
| ~ spl3_56 ),
inference(superposition,[],[f116,f1795]) ).
fof(f1855,plain,
( e2 = op(e3,e2)
| ~ spl3_54
| ~ spl3_56 ),
inference(forward_demodulation,[],[f460,f481]) ).
fof(f1856,plain,
( $false
| ~ spl3_54
| ~ spl3_56
| spl3_60 ),
inference(forward_subsumption_resolution,[],[f1855,f760]) ).
fof(f1857,plain,
( ~ spl3_54
| ~ spl3_56
| spl3_60 ),
inference(avatar_contradiction_clause,[],[f1856]) ).
fof(f1860,definition,
( spl3_63
<=> op(e2,e2) = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_63])],[avatar_definition]) ).
fof(f1862,plain,
( op(e2,e2) = op(e2,op(e2,e2))
| ~ spl3_63 ),
inference(avatar_component_clause,[],[f1860]) ).
fof(f1863,plain,
( ~ spl3_51
| spl3_63 ),
inference(avatar_split_clause,[],[f168,f1860,f445]) ).
fof(f1874,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP1
| spl3_49
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1754,f438]) ).
fof(f1876,definition,
( spl3_66
<=> op(e3,e0) = op(e0,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_66])],[avatar_definition]) ).
fof(f1878,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| ~ spl3_66 ),
inference(avatar_component_clause,[],[f1876]) ).
fof(f1879,plain,
( spl3_51
| spl3_66
| spl3_49
| spl3_53 ),
inference(avatar_split_clause,[],[f1874,f454,f436,f1876,f445]) ).
fof(f1880,plain,
( e0 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_15
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f1753,f285]) ).
fof(f1881,plain,
( e0 = op(e3,e0)
| spl3_15
| spl3_27
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f1880,f1806]) ).
fof(f1884,plain,
( e0 != op(e0,e0)
| spl3_15
| spl3_27
| ~ spl3_59 ),
inference(superposition,[],[f154,f1881]) ).
fof(f1910,definition,
( spl3_68
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f1911,plain,
( e1 != op(e2,e2)
| spl3_68 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1912,plain,
( e1 = op(e2,e2)
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1925,plain,
( e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| spl3_43 ),
inference(forward_subsumption_resolution,[],[f67,f411]) ).
fof(f1926,plain,
( e2 = op(e2,e1)
| e3 = op(e2,e1)
| spl3_43
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1925,f1817]) ).
fof(f1947,plain,
( e1 = op(e2,e1)
| ~ spl3_63
| ~ spl3_68 ),
inference(superposition,[],[f1862,f1912]) ).
fof(f1950,plain,
( $false
| ~ spl3_62
| ~ spl3_63
| ~ spl3_68 ),
inference(forward_subsumption_resolution,[],[f1947,f1817]) ).
fof(f1951,plain,
( ~ spl3_62
| ~ spl3_63
| ~ spl3_68 ),
inference(avatar_contradiction_clause,[],[f1950]) ).
fof(f1952,plain,
( ~ spl3_1
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1828,f479,f220]) ).
fof(f1953,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e3 = op(e3,e0)
| spl3_15 ),
inference(forward_subsumption_resolution,[],[f64,f285]) ).
fof(f1954,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| spl3_15
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f1953,f1806]) ).
fof(f1955,plain,
( ~ spl3_27
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1816,f1046,f337]) ).
fof(f1988,plain,
( e2 = op(e2,e1)
| spl3_1
| spl3_43
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1926,f222]) ).
fof(f1992,plain,
( e1 = op(e2,e2)
| spl3_1
| spl3_43
| ~ spl3_62 ),
inference(superposition,[],[f185,f1988]) ).
fof(f2002,plain,
( $false
| spl3_1
| spl3_43
| ~ spl3_62
| spl3_68 ),
inference(forward_subsumption_resolution,[],[f1992,f1911]) ).
fof(f2003,plain,
( spl3_1
| spl3_43
| ~ spl3_62
| spl3_68 ),
inference(avatar_contradiction_clause,[],[f2002]) ).
fof(f2028,plain,
( e0 = op(e3,e0)
| spl3_15
| spl3_27
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f1954,f339]) ).
fof(f2038,plain,
( e0 = op(e0,e0)
| spl3_15
| spl3_27
| ~ spl3_59
| ~ spl3_66 ),
inference(superposition,[],[f1878,f2028]) ).
fof(f2039,plain,
( $false
| spl3_15
| spl3_27
| ~ spl3_59
| ~ spl3_66 ),
inference(global_subsumption,[],[f2038,f1884]) ).
fof(f2040,plain,
( spl3_15
| spl3_27
| ~ spl3_59
| ~ spl3_66 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2044,plain,
( ~ spl3_21
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1794,f479,f310]) ).
fof(f2138,plain,
( op(e0,e3) = op(e3,op(e0,e3))
| ~ spl3_53 ),
inference(forward_subsumption_resolution,[],[f174,f455]) ).
fof(f2139,plain,
( e1 = op(e3,e1)
| ~ spl3_33
| ~ spl3_53 ),
inference(forward_demodulation,[],[f2138,f365]) ).
fof(f2140,plain,
( $false
| ~ spl3_33
| ~ spl3_53
| spl3_62 ),
inference(forward_subsumption_resolution,[],[f2139,f1047]) ).
fof(f2141,plain,
( ~ spl3_33
| ~ spl3_53
| spl3_62 ),
inference(avatar_contradiction_clause,[],[f2140]) ).
cnf(s222,plain,
( ~ spl3_5
| ~ spl3_6 ),
inference(sat_conversion,[],[f245]) ).
cnf(s238,plain,
( ~ spl3_13
| ~ spl3_14 ),
inference(sat_conversion,[],[f281]) ).
cnf(s246,plain,
( ~ spl3_17
| ~ spl3_18 ),
inference(sat_conversion,[],[f299]) ).
cnf(s262,plain,
( ~ spl3_25
| ~ spl3_26 ),
inference(sat_conversion,[],[f335]) ).
cnf(s287,plain,
( ~ spl3_37
| ~ spl3_38 ),
inference(sat_conversion,[],[f389]) ).
cnf(s299,plain,
( ~ spl3_43
| ~ spl3_44 ),
inference(sat_conversion,[],[f416]) ).
cnf(s303,plain,
( ~ spl3_45
| ~ spl3_46 ),
inference(sat_conversion,[],[f425]) ).
cnf(s326,plain,
( ~ spl3_49
| spl3_50 ),
inference(sat_conversion,[],[f443]) ).
cnf(s330,plain,
( ~ spl3_51
| spl3_52 ),
inference(sat_conversion,[],[f452]) ).
cnf(s334,plain,
( ~ spl3_53
| spl3_54 ),
inference(sat_conversion,[],[f461]) ).
cnf(s346,plain,
( spl3_55
| spl3_56
| spl3_57
| spl3_58 ),
inference(sat_conversion,[],[f490]) ).
cnf(s409,plain,
( spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(sat_conversion,[],[f567]) ).
cnf(s415,plain,
( spl3_3
| ~ spl3_27
| spl3_31
| ~ spl3_55 ),
inference(sat_conversion,[],[f570]) ).
cnf(s446,plain,
( ~ spl3_31
| spl3_33 ),
inference(sat_conversion,[],[f594]) ).
cnf(s458,plain,
( spl3_25
| ~ spl3_33 ),
inference(sat_conversion,[],[f604]) ).
cnf(s466,plain,
( ~ spl3_25
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_55 ),
inference(sat_conversion,[],[f612]) ).
cnf(s538,plain,
( ~ spl3_31
| ~ spl3_50 ),
inference(sat_conversion,[],[f685]) ).
cnf(s549,plain,
( ~ spl3_25
| spl3_26
| ~ spl3_56 ),
inference(sat_conversion,[],[f690]) ).
cnf(s554,plain,
( ~ spl3_31
| ~ spl3_58 ),
inference(sat_conversion,[],[f705]) ).
cnf(s561,plain,
( ~ spl3_27
| ~ spl3_57 ),
inference(sat_conversion,[],[f723]) ).
cnf(s595,plain,
( spl3_50
| ~ spl3_57 ),
inference(sat_conversion,[],[f752]) ).
cnf(s599,plain,
( spl3_7
| spl3_19
| spl3_59
| spl3_60 ),
inference(sat_conversion,[],[f762]) ).
cnf(s602,plain,
( spl3_56
| ~ spl3_59 ),
inference(sat_conversion,[],[f772]) ).
cnf(s604,plain,
( ~ spl3_57
| ~ spl3_59 ),
inference(sat_conversion,[],[f774]) ).
cnf(s651,plain,
( spl3_15
| spl3_27
| spl3_49
| spl3_51
| spl3_53
| ~ spl3_57 ),
inference(sat_conversion,[],[f823]) ).
cnf(s680,plain,
( spl3_1
| spl3_43
| ~ spl3_49
| ~ spl3_60 ),
inference(sat_conversion,[],[f852]) ).
cnf(s691,plain,
( ~ spl3_19
| spl3_21 ),
inference(sat_conversion,[],[f869]) ).
cnf(s702,plain,
( ~ spl3_1
| ~ spl3_57 ),
inference(sat_conversion,[],[f872]) ).
cnf(s724,plain,
( spl3_15
| spl3_27
| ~ spl3_43
| spl3_44
| ~ spl3_57 ),
inference(sat_conversion,[],[f888]) ).
cnf(s725,plain,
( ~ spl3_43
| spl3_45 ),
inference(sat_conversion,[],[f890]) ).
cnf(s744,plain,
( ~ spl3_15
| spl3_23 ),
inference(sat_conversion,[],[f902]) ).
cnf(s760,plain,
( spl3_17
| ~ spl3_23 ),
inference(sat_conversion,[],[f913]) ).
cnf(s762,plain,
( ~ spl3_23
| ~ spl3_43 ),
inference(sat_conversion,[],[f915]) ).
cnf(s784,plain,
( ~ spl3_17
| spl3_18
| ~ spl3_57 ),
inference(sat_conversion,[],[f924]) ).
cnf(s802,plain,
( ~ spl3_54
| ~ spl3_57 ),
inference(sat_conversion,[],[f928]) ).
cnf(s824,plain,
( spl3_13
| ~ spl3_21 ),
inference(sat_conversion,[],[f940]) ).
cnf(s836,plain,
( ~ spl3_13
| spl3_14
| ~ spl3_57 ),
inference(sat_conversion,[],[f947]) ).
cnf(s845,plain,
( spl3_37
| ~ spl3_45 ),
inference(sat_conversion,[],[f957]) ).
cnf(s869,plain,
( ~ spl3_52
| ~ spl3_60 ),
inference(sat_conversion,[],[f988]) ).
cnf(s902,plain,
( spl3_3
| spl3_31
| spl3_61
| spl3_62 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s907,plain,
( spl3_57
| ~ spl3_61 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s932,plain,
( ~ spl3_50
| ~ spl3_62 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s940,plain,
( spl3_1
| spl3_43
| ~ spl3_60
| ~ spl3_62 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s949,plain,
( ~ spl3_3
| ~ spl3_60 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s976,plain,
( ~ spl3_1
| ~ spl3_60 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s1056,plain,
( ~ spl3_45
| spl3_46
| ~ spl3_62 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s1064,plain,
( ~ spl3_3
| ~ spl3_56 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s1079,plain,
( ~ spl3_3
| spl3_11 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s1092,plain,
( ~ spl3_7
| spl3_9 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s1103,plain,
( spl3_5
| ~ spl3_11 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s1115,plain,
( ~ spl3_5
| spl3_6
| ~ spl3_58 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s1155,plain,
( ~ spl3_19
| ~ spl3_58 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s1182,plain,
( ~ spl3_7
| ~ spl3_62 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s1262,plain,
( ~ spl3_19
| ~ spl3_52 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s1267,plain,
( ~ spl3_21
| ~ spl3_53
| spl3_60 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s1282,plain,
( ~ spl3_15
| ~ spl3_21
| spl3_49
| spl3_51
| spl3_53 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s1311,plain,
( ~ spl3_15
| ~ spl3_23
| ~ spl3_53 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s1352,plain,
( ~ spl3_25
| spl3_38
| ~ spl3_55 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s1381,plain,
( spl3_1
| ~ spl3_9 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s1389,plain,
( ~ spl3_9
| ~ spl3_53
| spl3_60 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s1474,plain,
( ~ spl3_7
| ~ spl3_52 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s1511,plain,
( ~ spl3_3
| ~ spl3_15 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s1600,plain,
( ~ spl3_27
| spl3_49
| spl3_51
| spl3_53 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s1621,plain,
( ~ spl3_3
| ~ spl3_50 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s1652,plain,
( ~ spl3_5
| ~ spl3_11
| ~ spl3_51 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s1694,plain,
( ~ spl3_15
| ~ spl3_56 ),
inference(sat_conversion,[],[f1802]) ).
cnf(s1739,plain,
( ~ spl3_54
| ~ spl3_56
| spl3_60 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s1741,plain,
( ~ spl3_51
| spl3_63 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s1754,plain,
( spl3_49
| spl3_51
| spl3_53
| spl3_66 ),
inference(sat_conversion,[],[f1879]) ).
cnf(s1802,plain,
( ~ spl3_62
| ~ spl3_63
| ~ spl3_68 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s1811,plain,
( ~ spl3_1
| ~ spl3_56 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s1824,plain,
( ~ spl3_27
| ~ spl3_62 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s1855,plain,
( spl3_1
| spl3_43
| ~ spl3_62
| spl3_68 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s1875,plain,
( spl3_15
| spl3_27
| ~ spl3_59
| ~ spl3_66 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s1894,plain,
( ~ spl3_21
| ~ spl3_56 ),
inference(sat_conversion,[],[f2044]) ).
cnf(s1991,plain,
( ~ spl3_33
| ~ spl3_53
| spl3_62 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s1992,plain,
( ~ spl3_62
| spl3_49
| spl3_43
| spl3_27
| spl3_15
| spl3_19
| spl3_1 ),
inference(rat,[],[s334,s1754,s1739,s1875,s602,s1741,s599,s1802,s940,s1855,s1092,s1381]) ).
cnf(s1993,plain,
( spl3_49
| spl3_43
| spl3_27
| spl3_31
| spl3_15
| spl3_19
| spl3_3
| spl3_1 ),
inference(rat,[],[s330,s869,s651,s599,s334,s604,s802,s907,s902,s1992,s1092,s1381]) ).
cnf(s1994,plain,
( spl3_43
| spl3_27
| spl3_31
| spl3_15
| spl3_19
| spl3_3
| spl3_1 ),
inference(rat,[],[s907,s604,s902,s599,s932,s680,s326,s1993,s1092,s1381]) ).
cnf(s1995,plain,
( spl3_27
| spl3_31
| spl3_1
| spl3_15
| spl3_19
| spl3_3 ),
inference(rat,[],[s902,s907,s1056,s724,s303,s299,s725,s1994]) ).
cnf(s1996,plain,
( spl3_31
| spl3_15
| spl3_1
| spl3_3
| spl3_19 ),
inference(rat,[],[s907,s902,s561,s1824,s1995]) ).
cnf(s1997,plain,
( ~ spl3_31
| spl3_19
| spl3_1 ),
inference(rat,[],[s940,s1991,s725,s466,s845,s330,s287,s869,s1352,s599,s346,s602,s549,s262,s458,s326,s595,s446,s538,s554,s1092,s1381]) ).
cnf(s1998,plain,
( spl3_19
| spl3_3
| spl3_1 ),
inference(rat,[],[s907,s784,s902,s246,s940,s599,s760,s762,s602,s744,s1694,s1996,s1997,s1092,s1381]) ).
cnf(s1999,plain,
( ~ spl3_60
| ~ spl3_62
| spl3_1 ),
inference(rat,[],[s1056,s303,s725,s940]) ).
cnf(s2000,plain,
( spl3_31
| spl3_15
| spl3_3
| spl3_1 ),
inference(rat,[],[s1999,s1267,s409,s326,s932,s415,s902,s330,s1262,s907,s346,s836,s238,s824,s1155,s1894,s691,s1998]) ).
cnf(s2001,plain,
( ~ spl3_31
| ~ spl3_19
| spl3_1 ),
inference(rat,[],[s1999,s1991,s1267,s466,s458,s326,s446,s538,s330,s1262,s346,s836,s238,s824,s1155,s1894,s691]) ).
cnf(s2002,plain,
( spl3_3
| spl3_1 ),
inference(rat,[],[s1282,s1267,s326,s1999,s932,s2000,s902,s2001,s907,s836,s238,s824,s330,s691,s1262,s1998]) ).
cnf(s2003,plain,
( spl3_53
| ~ spl3_55
| spl3_51
| spl3_15
| spl3_49 ),
inference(rat,[],[s1600,s409]) ).
cnf(s2004,plain,
spl3_1,
inference(rat,[],[s2003,s1267,s346,s691,s1115,s599,s222,s1652,s602,s1103,s326,s595,s949,s1064,s1079,s1511,s1621,s2002,s1092,s1381]) ).
cnf(s2005,plain,
~ spl3_56,
inference(rat,[],[s1811,s2004]) ).
cnf(s2007,plain,
~ spl3_60,
inference(rat,[],[s976,s2004]) ).
cnf(s2008,plain,
~ spl3_57,
inference(rat,[],[s702,s2004]) ).
cnf(s2010,plain,
~ spl3_59,
inference(rat,[],[s602,s2005]) ).
cnf(s2012,plain,
~ spl3_61,
inference(rat,[],[s907,s2008]) ).
cnf(s2014,plain,
( ~ spl3_62
| spl3_15 ),
inference(rat,[],[s2003,s1267,s346,s330,s691,s1155,s1262,s326,s599,s932,s1182,s2007,s2008,s2005,s2010]) ).
cnf(s2015,plain,
( ~ spl3_31
| ~ spl3_7
| spl3_15 ),
inference(rat,[],[s2003,s326,s346,s538,s554,s330,s1474,s1389,s1092,s2008,s2005,s2007]) ).
cnf(s2016,plain,
( ~ spl3_7
| spl3_15 ),
inference(rat,[],[s1115,s346,s222,s2003,s1103,s326,s1079,s1621,s902,s2015,s1389,s330,s1092,s1474,s2014,s2008,s2005,s2012,s2007]) ).
cnf(s2017,plain,
spl3_15,
inference(rat,[],[s902,s538,s1621,s326,s2003,s1267,s346,s330,s691,s1155,s1262,s599,s2016,s2014,s2012,s2007,s2008,s2005,s2010]) ).
cnf(s2018,plain,
~ spl3_3,
inference(rat,[],[s1511,s2017]) ).
cnf(s2019,plain,
spl3_23,
inference(rat,[],[s744,s2017]) ).
cnf(s2021,plain,
~ spl3_53,
inference(rat,[],[s1311,s2017,s2019]) ).
cnf(s2030,plain,
~ spl3_62,
inference(rat,[],[s1282,s330,s691,s1262,s326,s599,s932,s1182,s2021,s2017,s2007,s2010]) ).
cnf(s2031,plain,
spl3_31,
inference(rat,[],[s902,s2012,s2018,s2030]) ).
cnf(s2032,plain,
~ spl3_58,
inference(rat,[],[s554,s2031]) ).
cnf(s2033,plain,
~ spl3_50,
inference(rat,[],[s538,s2031]) ).
cnf(s2034,plain,
spl3_33,
inference(rat,[],[s446,s2031]) ).
cnf(s2036,plain,
spl3_55,
inference(rat,[],[s346,s2005,s2008,s2032]) ).
cnf(s2037,plain,
~ spl3_49,
inference(rat,[],[s326,s2033]) ).
cnf(s2038,plain,
spl3_25,
inference(rat,[],[s458,s2034]) ).
cnf(s2043,plain,
spl3_51,
inference(rat,[],[s466,s2021,s2036,s2037,s2038]) ).
cnf(s2048,plain,
spl3_52,
inference(rat,[],[s330,s2043]) ).
cnf(s2049,plain,
~ spl3_7,
inference(rat,[],[s1474,s2048]) ).
cnf(s2050,plain,
~ spl3_19,
inference(rat,[],[s1262,s2048]) ).
cnf(s2051,plain,
$false,
inference(rat,[],[s599,s2010,s2007,s2049,s2050]) ).
fof(f2142,plain,
$false,
inference(avatar_sat_refutation,[],[s2051]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:35:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.32 % (2935097)Will run a generic schedule for satisfiability detection.
% 0.21/0.32 % (2935108)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1829190938:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.32 % (2935107)% WARNING: option uhcvi not known.
% 0.21/0.32 % (2935110)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2863157594:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.32 % (2935111)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3979221454:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.32 % (2935112)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3374758776:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.32 % (2935109)dis+10_1_sil=32000:sp=arity:random_seed=3744367866:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.32 % (2935106)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2426140070_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.32 % (2935107)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=781609674:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.32 % Detected minimum model sizes of [4]
% 0.21/0.32 % Detected maximum model sizes of [max]
% 0.21/0.32 % TRYING [4]
% 0.21/0.32 % TRYING [5]
% 0.21/0.32 % (2935108) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2935097-2935108"...
% 0.21/0.32 % TRYING [6]
% 0.21/0.32 % (2935108)...printing done.
% 0.21/0.32 % (2935108)Refutation found. Thanks to Tanya!
% 0.21/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.21/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.32 % (2935108)------------------------------
% 0.21/0.32 % (2935108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.32 % (2935108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.32 % (2935108)CaDiCaL version: 2.1.3
% 0.21/0.32 % (2935108)Termination reason: Refutation
% 0.21/0.32 % (2935108)Time elapsed: 0.048 s
% 0.21/0.32 % (2935108)Peak memory usage: 13 MB
% 0.21/0.32 % (2935108)Instructions burned: 115 (million)
% 0.21/0.32 % (2935097)Success in time 0.079 s
% 0.21/0.32 % Vampire exiting
%------------------------------------------------------------------------------