%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG023+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 03:38:08 EST 2010
% Result : Unsatisfiable 3.85s
% Output : CNFRefutation 3.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 11
% Syntax : Number of formulae : 158 ( 39 unt; 0 def)
% Number of atoms : 880 ( 778 equ)
% Maximal formula atoms : 256 ( 5 avg)
% Number of connectives : 917 ( 195 ~; 480 |; 241 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 2 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(7,axiom,
~ ( e2 = op(e0,e0)
& e1 = op(e3,e0) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax27) ).
fof(10,axiom,
~ ( e1 = op(e3,e3)
& e2 = op(e0,e3) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax20) ).
fof(13,axiom,
( op(op(e0,e0),e0) = op(e0,op(e0,e0))
& op(op(e0,e0),e1) = op(e0,op(e0,e1))
& op(op(e0,e0),e2) = op(e0,op(e0,e2))
& op(op(e0,e0),e3) = op(e0,op(e0,e3))
& op(op(e0,e1),e0) = op(e0,op(e1,e0))
& op(op(e0,e1),e1) = op(e0,op(e1,e1))
& op(op(e0,e1),e2) = op(e0,op(e1,e2))
& op(op(e0,e1),e3) = op(e0,op(e1,e3))
& op(op(e0,e2),e0) = op(e0,op(e2,e0))
& op(op(e0,e2),e1) = op(e0,op(e2,e1))
& op(op(e0,e2),e2) = op(e0,op(e2,e2))
& op(op(e0,e2),e3) = op(e0,op(e2,e3))
& op(op(e0,e3),e0) = op(e0,op(e3,e0))
& op(op(e0,e3),e1) = op(e0,op(e3,e1))
& op(op(e0,e3),e2) = op(e0,op(e3,e2))
& op(op(e0,e3),e3) = op(e0,op(e3,e3))
& op(op(e1,e0),e0) = op(e1,op(e0,e0))
& op(op(e1,e0),e1) = op(e1,op(e0,e1))
& op(op(e1,e0),e2) = op(e1,op(e0,e2))
& op(op(e1,e0),e3) = op(e1,op(e0,e3))
& op(op(e1,e1),e0) = op(e1,op(e1,e0))
& op(op(e1,e1),e1) = op(e1,op(e1,e1))
& op(op(e1,e1),e2) = op(e1,op(e1,e2))
& op(op(e1,e1),e3) = op(e1,op(e1,e3))
& op(op(e1,e2),e0) = op(e1,op(e2,e0))
& op(op(e1,e2),e1) = op(e1,op(e2,e1))
& op(op(e1,e2),e2) = op(e1,op(e2,e2))
& op(op(e1,e2),e3) = op(e1,op(e2,e3))
& op(op(e1,e3),e0) = op(e1,op(e3,e0))
& op(op(e1,e3),e1) = op(e1,op(e3,e1))
& op(op(e1,e3),e2) = op(e1,op(e3,e2))
& op(op(e1,e3),e3) = op(e1,op(e3,e3))
& op(op(e2,e0),e0) = op(e2,op(e0,e0))
& op(op(e2,e0),e1) = op(e2,op(e0,e1))
& op(op(e2,e0),e2) = op(e2,op(e0,e2))
& op(op(e2,e0),e3) = op(e2,op(e0,e3))
& op(op(e2,e1),e0) = op(e2,op(e1,e0))
& op(op(e2,e1),e1) = op(e2,op(e1,e1))
& op(op(e2,e1),e2) = op(e2,op(e1,e2))
& op(op(e2,e1),e3) = op(e2,op(e1,e3))
& op(op(e2,e2),e0) = op(e2,op(e2,e0))
& op(op(e2,e2),e1) = op(e2,op(e2,e1))
& op(op(e2,e2),e2) = op(e2,op(e2,e2))
& op(op(e2,e2),e3) = op(e2,op(e2,e3))
& op(op(e2,e3),e0) = op(e2,op(e3,e0))
& op(op(e2,e3),e1) = op(e2,op(e3,e1))
& op(op(e2,e3),e2) = op(e2,op(e3,e2))
& op(op(e2,e3),e3) = op(e2,op(e3,e3))
& op(op(e3,e0),e0) = op(e3,op(e0,e0))
& op(op(e3,e0),e1) = op(e3,op(e0,e1))
& op(op(e3,e0),e2) = op(e3,op(e0,e2))
& op(op(e3,e0),e3) = op(e3,op(e0,e3))
& op(op(e3,e1),e0) = op(e3,op(e1,e0))
& op(op(e3,e1),e1) = op(e3,op(e1,e1))
& op(op(e3,e1),e2) = op(e3,op(e1,e2))
& op(op(e3,e1),e3) = op(e3,op(e1,e3))
& op(op(e3,e2),e0) = op(e3,op(e2,e0))
& op(op(e3,e2),e1) = op(e3,op(e2,e1))
& op(op(e3,e2),e2) = op(e3,op(e2,e2))
& op(op(e3,e2),e3) = op(e3,op(e2,e3))
& op(op(e3,e3),e0) = op(e3,op(e3,e0))
& op(op(e3,e3),e1) = op(e3,op(e3,e1))
& op(op(e3,e3),e2) = op(e3,op(e3,e2))
& op(op(e3,e3),e3) = op(e3,op(e3,e3)) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax2) ).
fof(14,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax3) ).
fof(15,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('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax1) ).
fof(21,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('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax9) ).
fof(25,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(e2,e1) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax17) ).
fof(26,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax10) ).
fof(27,axiom,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax11) ).
fof(35,axiom,
~ ( e3 = op(e1,e1)
& e0 = op(e2,e1) ),
file('/tmp/tmpuu3GqC/sel_ALG023+1.p_1',ax31) ).
fof(37,plain,
( epred1_0
=> ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 ) ) ),
introduced(definition) ).
fof(38,plain,
( epred1_0
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
inference(apply_def,[status(esa)],[27,37,theory(equality)]) ).
fof(51,plain,
( e2 != op(e0,e0)
| e1 != op(e3,e0) ),
inference(fof_nnf,[status(thm)],[7]) ).
cnf(52,plain,
( e1 != op(e3,e0)
| e2 != op(e0,e0) ),
inference(split_conjunct,[status(thm)],[51]) ).
fof(57,plain,
( e1 != op(e3,e3)
| e2 != op(e0,e3) ),
inference(fof_nnf,[status(thm)],[10]) ).
cnf(58,plain,
( e2 != op(e0,e3)
| e1 != op(e3,e3) ),
inference(split_conjunct,[status(thm)],[57]) ).
cnf(85,plain,
op(op(e2,e2),e1) = op(e2,op(e2,e1)),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(127,plain,
( unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(split_conjunct,[status(thm)],[14]) ).
cnf(128,plain,
op(e3,unit) = e3,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(129,plain,
op(unit,e3) = e3,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(130,plain,
op(e2,unit) = e2,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(132,plain,
op(e1,unit) = e1,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(133,plain,
op(unit,e1) = e1,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(134,plain,
op(e0,unit) = e0,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(135,plain,
op(unit,e0) = e0,
inference(split_conjunct,[status(thm)],[14]) ).
cnf(139,plain,
( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 ),
inference(split_conjunct,[status(thm)],[15]) ).
cnf(142,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(split_conjunct,[status(thm)],[15]) ).
cnf(148,plain,
( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(split_conjunct,[status(thm)],[15]) ).
cnf(193,plain,
op(e3,e1) != op(e3,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(195,plain,
op(e3,e0) != op(e3,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(196,plain,
op(e3,e0) != op(e3,e2),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(198,plain,
op(e2,e2) != op(e2,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(200,plain,
op(e2,e1) != op(e2,e2),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(203,plain,
op(e2,e0) != op(e2,e1),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(205,plain,
op(e1,e1) != op(e1,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(206,plain,
op(e1,e1) != op(e1,e2),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(211,plain,
op(e0,e1) != op(e0,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(213,plain,
op(e0,e0) != op(e0,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(214,plain,
op(e0,e0) != op(e0,e2),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(219,plain,
op(e0,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(221,plain,
op(e0,e3) != op(e1,e3),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(228,plain,
op(e2,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(232,plain,
op(e0,e1) != op(e2,e1),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(234,plain,
op(e2,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(237,plain,
op(e0,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[21]) ).
fof(246,plain,
( e0 != op(e1,e1)
| e3 != op(e2,e1) ),
inference(fof_nnf,[status(thm)],[25]) ).
cnf(247,plain,
( e3 != op(e2,e1)
| e0 != op(e1,e1) ),
inference(split_conjunct,[status(thm)],[246]) ).
cnf(250,plain,
e1 != e2,
inference(split_conjunct,[status(thm)],[26]) ).
cnf(252,plain,
e0 != e2,
inference(split_conjunct,[status(thm)],[26]) ).
cnf(253,plain,
e0 != e1,
inference(split_conjunct,[status(thm)],[26]) ).
fof(254,plain,
( ( op(e0,e0) = e3
| epred1_0 )
& ( op(e1,e1) = e3
| epred1_0 )
& ( op(e2,e2) = e3
| epred1_0 )
& ( op(e3,e3) = e3
| epred1_0 ) ),
inference(distribute,[status(thm)],[38]) ).
cnf(255,plain,
( epred1_0
| op(e3,e3) = e3 ),
inference(split_conjunct,[status(thm)],[254]) ).
cnf(256,plain,
( epred1_0
| op(e2,e2) = e3 ),
inference(split_conjunct,[status(thm)],[254]) ).
cnf(257,plain,
( epred1_0
| op(e1,e1) = e3 ),
inference(split_conjunct,[status(thm)],[254]) ).
fof(273,plain,
( e3 != op(e1,e1)
| e0 != op(e2,e1) ),
inference(fof_nnf,[status(thm)],[35]) ).
cnf(274,plain,
( e0 != op(e2,e1)
| e3 != op(e1,e1) ),
inference(split_conjunct,[status(thm)],[273]) ).
fof(275,plain,
( ~ epred1_0
| ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 ) ),
inference(fof_nnf,[status(thm)],[37]) ).
fof(276,plain,
( ( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e0,e0) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e1,e1) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e2,e2) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0
| ~ epred1_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0
| ~ epred1_0 ) ),
inference(distribute,[status(thm)],[275]) ).
cnf(308,plain,
( op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(309,plain,
( op(e1,e1) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(311,plain,
( op(e1,e1) = e0
| op(e3,e3) = e1
| op(e1,e1) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(324,plain,
( op(e1,e1) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(328,plain,
( op(e0,e0) = e0
| op(e3,e3) = e1
| op(e0,e0) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(336,plain,
( op(e0,e0) = e0
| op(e1,e1) = e1
| op(e0,e0) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(338,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e2,e2) = e2
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(346,plain,
( op(e1,e3) = e1
| unit = e0
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[132,127,theory(equality)]) ).
cnf(347,plain,
( op(e2,e3) = e2
| unit = e0
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[130,127,theory(equality)]) ).
cnf(348,plain,
( op(e0,e3) = e0
| unit = e0
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[134,127,theory(equality)]) ).
cnf(353,plain,
( epred1_0
| e3 != op(e3,e1) ),
inference(spm,[status(thm)],[193,255,theory(equality)]) ).
cnf(359,plain,
( epred1_0
| e3 != op(e2,e1) ),
inference(spm,[status(thm)],[200,256,theory(equality)]) ).
cnf(417,plain,
( epred1_0
| op(e2,e1) != e0 ),
inference(spm,[status(thm)],[274,257,theory(equality)]) ).
cnf(427,plain,
( op(e3,e1) = op(e2,op(e2,e1))
| epred1_0 ),
inference(spm,[status(thm)],[85,256,theory(equality)]) ).
cnf(485,plain,
( op(e3,e0) = e0
| op(e3,e0) = e2
| op(e3,e0) = e1
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[196,139,theory(equality)]) ).
cnf(582,plain,
( op(e0,e3) = e0
| op(e0,e3) = e2
| op(e0,e3) = e1
| e3 != op(e1,e3) ),
inference(spm,[status(thm)],[221,148,theory(equality)]) ).
cnf(623,plain,
( epred1_0
| op(e2,e1) = e0
| op(e2,e1) = e2
| op(e2,e1) = e1 ),
inference(spm,[status(thm)],[359,142,theory(equality)]) ).
cnf(705,plain,
( unit = e1
| unit = e2
| unit = e0
| e1 != op(e1,e1) ),
inference(spm,[status(thm)],[205,346,theory(equality)]) ).
cnf(715,plain,
( unit = e1
| unit = e2
| unit = e0
| e2 != op(e2,e2) ),
inference(spm,[status(thm)],[198,347,theory(equality)]) ).
cnf(726,plain,
( unit = e1
| unit = e2
| unit = e0
| e0 != op(e0,e0) ),
inference(spm,[status(thm)],[213,348,theory(equality)]) ).
cnf(1612,plain,
( op(e2,e1) = e1
| op(e2,e1) = e2
| epred1_0 ),
inference(csr,[status(thm)],[623,417]) ).
cnf(1622,plain,
( op(e2,e2) = op(e3,e1)
| epred1_0
| op(e2,e1) = e1 ),
inference(spm,[status(thm)],[427,1612,theory(equality)]) ).
cnf(1637,plain,
( epred1_0
| op(e2,e1) = e1
| op(e2,e2) != e3 ),
inference(spm,[status(thm)],[353,1622,theory(equality)]) ).
cnf(1697,plain,
( op(e2,e1) = e1
| epred1_0 ),
inference(csr,[status(thm)],[1637,256]) ).
cnf(1706,plain,
( op(e2,e1) = op(e3,e1)
| epred1_0 ),
inference(spm,[status(thm)],[427,1697,theory(equality)]) ).
cnf(1710,plain,
epred1_0,
inference(sr,[status(thm)],[1706,228,theory(equality)]) ).
cnf(1790,plain,
( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0
| $false ),
inference(rw,[status(thm)],[308,1710,theory(equality)]) ).
cnf(1791,plain,
( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cn,[status(thm)],[1790,theory(equality)]) ).
cnf(1792,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e2,e2) = e2
| $false ),
inference(rw,[status(thm)],[338,1710,theory(equality)]) ).
cnf(1793,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e2,e2) = e2 ),
inference(cn,[status(thm)],[1792,theory(equality)]) ).
cnf(1804,plain,
( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0
| $false ),
inference(rw,[status(thm)],[324,1710,theory(equality)]) ).
cnf(1805,plain,
( op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cn,[status(thm)],[1804,theory(equality)]) ).
cnf(1824,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e1,e1) = e1
| $false ),
inference(rw,[status(thm)],[336,1710,theory(equality)]) ).
cnf(1825,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e1,e1) = e1 ),
inference(cn,[status(thm)],[1824,theory(equality)]) ).
cnf(1884,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e3,e3) = e1
| $false ),
inference(rw,[status(thm)],[328,1710,theory(equality)]) ).
cnf(1885,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e3,e3) = e1 ),
inference(cn,[status(thm)],[1884,theory(equality)]) ).
cnf(1900,plain,
( op(e1,e1) = e0
| op(e1,e1) = e2
| op(e3,e3) = e1
| $false ),
inference(rw,[status(thm)],[311,1710,theory(equality)]) ).
cnf(1901,plain,
( op(e1,e1) = e0
| op(e1,e1) = e2
| op(e3,e3) = e1 ),
inference(cn,[status(thm)],[1900,theory(equality)]) ).
cnf(1912,plain,
( op(e1,e1) = e0
| op(e3,e3) = e2
| op(e3,e3) = e1
| $false ),
inference(rw,[status(thm)],[309,1710,theory(equality)]) ).
cnf(1913,plain,
( op(e1,e1) = e0
| op(e3,e3) = e2
| op(e3,e3) = e1 ),
inference(cn,[status(thm)],[1912,theory(equality)]) ).
cnf(1960,plain,
( unit = e0
| unit = e2
| unit = e1
| op(e2,e2) = e2
| op(e0,e0) = e1 ),
inference(spm,[status(thm)],[726,1793,theory(equality)]) ).
cnf(2226,plain,
( op(e1,e1) = e1
| op(e0,e0) = e2
| e0 != op(e0,e2) ),
inference(spm,[status(thm)],[214,1825,theory(equality)]) ).
cnf(3210,plain,
( op(e0,e0) = e2
| op(e0,e0) = e0
| e1 != op(e3,e0) ),
inference(spm,[status(thm)],[195,1885,theory(equality)]) ).
cnf(3773,plain,
( op(e1,e1) = e2
| op(e1,e1) = e0
| e1 != op(e0,e3) ),
inference(spm,[status(thm)],[219,1901,theory(equality)]) ).
cnf(4192,plain,
( op(e3,e3) = e1
| op(e1,e1) = e0
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[219,1913,theory(equality)]) ).
cnf(4867,plain,
( op(e0,e0) = e1
| unit = e0
| unit = e2
| unit = e1 ),
inference(csr,[status(thm)],[1960,715]) ).
cnf(4882,plain,
( op(e1,e1) = e1
| e1 = e2
| e1 = e0
| unit = e1
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[1825,4867,theory(equality)]) ).
cnf(4894,plain,
( op(e1,e1) = e1
| e0 = e1
| unit = e1
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[4882,250,theory(equality)]) ).
cnf(4895,plain,
( op(e1,e1) = e1
| unit = e1
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[4894,253,theory(equality)]) ).
cnf(4957,plain,
( unit = e0
| unit = e2
| unit = e1 ),
inference(csr,[status(thm)],[4895,705]) ).
cnf(4963,plain,
( op(e2,e0) = e2
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[130,4957,theory(equality)]) ).
cnf(4964,plain,
( op(e0,e0) = e0
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[134,4957,theory(equality)]) ).
cnf(4966,plain,
( op(e0,e1) = e1
| unit = e2
| unit = e1 ),
inference(spm,[status(thm)],[133,4957,theory(equality)]) ).
cnf(5048,plain,
( unit = e1
| unit = e2
| e2 != op(e2,e1) ),
inference(spm,[status(thm)],[203,4963,theory(equality)]) ).
cnf(5080,plain,
( op(e2,e2) = e0
| e0 = e1
| e0 = e2
| unit = e1
| unit = e2 ),
inference(spm,[status(thm)],[1791,4964,theory(equality)]) ).
cnf(5083,plain,
( op(e1,e1) = e0
| e0 = e1
| e0 = e2
| unit = e1
| unit = e2 ),
inference(spm,[status(thm)],[1805,4964,theory(equality)]) ).
cnf(5091,plain,
( op(e2,e2) = e0
| e0 = e2
| unit = e1
| unit = e2 ),
inference(sr,[status(thm)],[5080,253,theory(equality)]) ).
cnf(5092,plain,
( op(e2,e2) = e0
| unit = e1
| unit = e2 ),
inference(sr,[status(thm)],[5091,252,theory(equality)]) ).
cnf(5095,plain,
( op(e1,e1) = e0
| e0 = e2
| unit = e1
| unit = e2 ),
inference(sr,[status(thm)],[5083,253,theory(equality)]) ).
cnf(5096,plain,
( op(e1,e1) = e0
| unit = e1
| unit = e2 ),
inference(sr,[status(thm)],[5095,252,theory(equality)]) ).
cnf(5161,plain,
( unit = e1
| unit = e2
| e1 != op(e2,e1) ),
inference(spm,[status(thm)],[232,4966,theory(equality)]) ).
cnf(5250,plain,
( unit = e2
| unit = e1
| e0 != op(e2,e1) ),
inference(spm,[status(thm)],[200,5092,theory(equality)]) ).
cnf(5269,plain,
( unit = e2
| unit = e1
| op(e2,e1) != e3 ),
inference(spm,[status(thm)],[247,5096,theory(equality)]) ).
cnf(5407,plain,
( unit = e1
| unit = e2
| op(e2,e1) = e0
| op(e2,e1) = e2
| op(e2,e1) = e1 ),
inference(spm,[status(thm)],[5269,142,theory(equality)]) ).
cnf(7035,plain,
( op(e0,e0) = e0
| op(e3,e0) != e1 ),
inference(csr,[status(thm)],[3210,52]) ).
cnf(8795,plain,
( op(e1,e1) = e0
| op(e0,e3) != e2 ),
inference(csr,[status(thm)],[4192,58]) ).
cnf(26527,plain,
( op(e2,e1) = e0
| op(e2,e1) = e2
| unit = e1
| unit = e2 ),
inference(csr,[status(thm)],[5407,5161]) ).
cnf(26528,plain,
( op(e2,e1) = e0
| unit = e1
| unit = e2 ),
inference(csr,[status(thm)],[26527,5048]) ).
cnf(26529,plain,
( unit = e1
| unit = e2 ),
inference(csr,[status(thm)],[26528,5250]) ).
cnf(26532,plain,
( op(e3,e2) = e3
| unit = e1 ),
inference(spm,[status(thm)],[128,26529,theory(equality)]) ).
cnf(26533,plain,
( op(e1,e2) = e1
| unit = e1 ),
inference(spm,[status(thm)],[132,26529,theory(equality)]) ).
cnf(26535,plain,
( op(e0,e2) = e0
| unit = e1 ),
inference(spm,[status(thm)],[134,26529,theory(equality)]) ).
cnf(26539,plain,
( op(e2,e0) = e0
| unit = e1 ),
inference(spm,[status(thm)],[135,26529,theory(equality)]) ).
cnf(26671,plain,
( op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e0
| unit = e1 ),
inference(spm,[status(thm)],[485,26532,theory(equality)]) ).
cnf(26720,plain,
( unit = e1
| e1 != op(e1,e1) ),
inference(spm,[status(thm)],[206,26533,theory(equality)]) ).
cnf(26842,plain,
( op(e0,e0) = e2
| op(e1,e1) = e1
| unit = e1 ),
inference(spm,[status(thm)],[2226,26535,theory(equality)]) ).
cnf(27376,plain,
( op(e0,e0) = e2
| unit = e1 ),
inference(csr,[status(thm)],[26842,26720]) ).
cnf(34526,plain,
( op(e3,e0) = e2
| op(e3,e0) = e1
| unit = e1
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[234,26671,theory(equality)]) ).
cnf(34612,plain,
( op(e3,e0) = e2
| op(e3,e0) = e1
| unit = e1 ),
inference(csr,[status(thm)],[34526,26539]) ).
cnf(34622,plain,
( op(e3,e0) = e1
| unit = e1
| e2 != op(e0,e0) ),
inference(spm,[status(thm)],[237,34612,theory(equality)]) ).
cnf(34697,plain,
( op(e3,e0) = e1
| unit = e1 ),
inference(csr,[status(thm)],[34622,27376]) ).
cnf(34724,plain,
( op(e0,e0) = e0
| unit = e1 ),
inference(spm,[status(thm)],[7035,34697,theory(equality)]) ).
cnf(34804,plain,
( e0 = e2
| unit = e1 ),
inference(spm,[status(thm)],[27376,34724,theory(equality)]) ).
cnf(34829,plain,
unit = e1,
inference(sr,[status(thm)],[34804,252,theory(equality)]) ).
cnf(34841,plain,
op(e1,e1) = e1,
inference(rw,[status(thm)],[133,34829,theory(equality)]) ).
cnf(34842,plain,
op(e1,e3) = e3,
inference(rw,[status(thm)],[129,34829,theory(equality)]) ).
cnf(34843,plain,
op(e0,e1) = e0,
inference(rw,[status(thm)],[134,34829,theory(equality)]) ).
cnf(36431,plain,
( e1 = e0
| op(e0,e3) != e2 ),
inference(rw,[status(thm)],[8795,34841,theory(equality)]) ).
cnf(36432,plain,
op(e0,e3) != e2,
inference(sr,[status(thm)],[36431,253,theory(equality)]) ).
cnf(36449,plain,
( e1 = e0
| op(e1,e1) = e2
| op(e0,e3) != e1 ),
inference(rw,[status(thm)],[3773,34841,theory(equality)]) ).
cnf(36450,plain,
( e1 = e0
| e1 = e2
| op(e0,e3) != e1 ),
inference(rw,[status(thm)],[36449,34841,theory(equality)]) ).
cnf(36451,plain,
( e2 = e1
| op(e0,e3) != e1 ),
inference(sr,[status(thm)],[36450,253,theory(equality)]) ).
cnf(36452,plain,
op(e0,e3) != e1,
inference(sr,[status(thm)],[36451,250,theory(equality)]) ).
cnf(36786,plain,
( op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e0
| $false ),
inference(rw,[status(thm)],[582,34842,theory(equality)]) ).
cnf(36787,plain,
( op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e0 ),
inference(cn,[status(thm)],[36786,theory(equality)]) ).
cnf(36881,plain,
op(e0,e3) != e0,
inference(rw,[status(thm)],[211,34843,theory(equality)]) ).
cnf(38299,plain,
( op(e0,e3) = e2
| op(e0,e3) = e0 ),
inference(sr,[status(thm)],[36787,36452,theory(equality)]) ).
cnf(38300,plain,
op(e0,e3) = e0,
inference(sr,[status(thm)],[38299,36432,theory(equality)]) ).
cnf(38301,plain,
$false,
inference(sr,[status(thm)],[38300,36881,theory(equality)]) ).
cnf(38302,plain,
$false,
38301,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG023+1.p
% --creating new selector for []
% -running prover on /tmp/tmpuu3GqC/sel_ALG023+1.p_1 with time limit 29
% -prover status Unsatisfiable
% Problem ALG023+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG023+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG023+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Unsatisfiable
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------