%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SYN551+2 : TPTP v5.0.0. Bugfixed v3.1.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 : Sun Dec 26 13:53:51 EST 2010
% Result : Theorem 1.57s
% Output : CNFRefutation 1.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 101
% Number of leaves : 3
% Syntax : Number of formulae : 241 ( 8 unt; 0 def)
% Number of atoms : 1196 (1037 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 1137 ( 182 ~; 920 |; 27 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 375 ( 12 sgn 26 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,conjecture,
( ? [X1] :
! [X2] :
( X2 = f(g(X2))
<=> X1 = X2 )
<=> ? [X1] :
! [X2] :
( X2 = g(f(X2))
<=> X1 = X2 ) ),
file('/tmp/tmpvqDG4h/sel_SYN551+2.p_1',prove_this_cute_thing) ).
fof(2,negated_conjecture,
~ ( ? [X1] :
! [X2] :
( X2 = f(g(X2))
<=> X1 = X2 )
<=> ? [X1] :
! [X2] :
( X2 = g(f(X2))
<=> X1 = X2 ) ),
inference(assume_negation,[status(cth)],[1]) ).
fof(3,negated_conjecture,
( ( ! [X1] :
? [X2] :
( ( X2 != f(g(X2))
| X1 != X2 )
& ( X2 = f(g(X2))
| X1 = X2 ) )
| ! [X1] :
? [X2] :
( ( X2 != g(f(X2))
| X1 != X2 )
& ( X2 = g(f(X2))
| X1 = X2 ) ) )
& ( ? [X1] :
! [X2] :
( ( X2 != f(g(X2))
| X1 = X2 )
& ( X1 != X2
| X2 = f(g(X2)) ) )
| ? [X1] :
! [X2] :
( ( X2 != g(f(X2))
| X1 = X2 )
& ( X1 != X2
| X2 = g(f(X2)) ) ) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(4,negated_conjecture,
( ( ! [X3] :
? [X4] :
( ( X4 != f(g(X4))
| X3 != X4 )
& ( X4 = f(g(X4))
| X3 = X4 ) )
| ! [X5] :
? [X6] :
( ( X6 != g(f(X6))
| X5 != X6 )
& ( X6 = g(f(X6))
| X5 = X6 ) ) )
& ( ? [X7] :
! [X8] :
( ( X8 != f(g(X8))
| X7 = X8 )
& ( X7 != X8
| X8 = f(g(X8)) ) )
| ? [X9] :
! [X10] :
( ( X10 != g(f(X10))
| X9 = X10 )
& ( X9 != X10
| X10 = g(f(X10)) ) ) ) ),
inference(variable_rename,[status(thm)],[3]) ).
fof(5,negated_conjecture,
( ( ! [X3] :
( ( esk1_1(X3) != f(g(esk1_1(X3)))
| X3 != esk1_1(X3) )
& ( esk1_1(X3) = f(g(esk1_1(X3)))
| X3 = esk1_1(X3) ) )
| ! [X5] :
( ( esk2_1(X5) != g(f(esk2_1(X5)))
| X5 != esk2_1(X5) )
& ( esk2_1(X5) = g(f(esk2_1(X5)))
| X5 = esk2_1(X5) ) ) )
& ( ! [X8] :
( ( X8 != f(g(X8))
| esk3_0 = X8 )
& ( esk3_0 != X8
| X8 = f(g(X8)) ) )
| ! [X10] :
( ( X10 != g(f(X10))
| esk4_0 = X10 )
& ( esk4_0 != X10
| X10 = g(f(X10)) ) ) ) ),
inference(skolemize,[status(esa)],[4]) ).
fof(6,negated_conjecture,
! [X3,X5,X8,X10] :
( ( ( ( X10 != g(f(X10))
| esk4_0 = X10 )
& ( esk4_0 != X10
| X10 = g(f(X10)) ) )
| ( ( X8 != f(g(X8))
| esk3_0 = X8 )
& ( esk3_0 != X8
| X8 = f(g(X8)) ) ) )
& ( ( ( esk2_1(X5) != g(f(esk2_1(X5)))
| X5 != esk2_1(X5) )
& ( esk2_1(X5) = g(f(esk2_1(X5)))
| X5 = esk2_1(X5) ) )
| ( ( esk1_1(X3) != f(g(esk1_1(X3)))
| X3 != esk1_1(X3) )
& ( esk1_1(X3) = f(g(esk1_1(X3)))
| X3 = esk1_1(X3) ) ) ) ),
inference(shift_quantors,[status(thm)],[5]) ).
fof(7,negated_conjecture,
! [X3,X5,X8,X10] :
( ( X8 != f(g(X8))
| esk3_0 = X8
| X10 != g(f(X10))
| esk4_0 = X10 )
& ( esk3_0 != X8
| X8 = f(g(X8))
| X10 != g(f(X10))
| esk4_0 = X10 )
& ( X8 != f(g(X8))
| esk3_0 = X8
| esk4_0 != X10
| X10 = g(f(X10)) )
& ( esk3_0 != X8
| X8 = f(g(X8))
| esk4_0 != X10
| X10 = g(f(X10)) )
& ( esk1_1(X3) != f(g(esk1_1(X3)))
| X3 != esk1_1(X3)
| esk2_1(X5) != g(f(esk2_1(X5)))
| X5 != esk2_1(X5) )
& ( esk1_1(X3) = f(g(esk1_1(X3)))
| X3 = esk1_1(X3)
| esk2_1(X5) != g(f(esk2_1(X5)))
| X5 != esk2_1(X5) )
& ( esk1_1(X3) != f(g(esk1_1(X3)))
| X3 != esk1_1(X3)
| esk2_1(X5) = g(f(esk2_1(X5)))
| X5 = esk2_1(X5) )
& ( esk1_1(X3) = f(g(esk1_1(X3)))
| X3 = esk1_1(X3)
| esk2_1(X5) = g(f(esk2_1(X5)))
| X5 = esk2_1(X5) ) ),
inference(distribute,[status(thm)],[6]) ).
cnf(8,negated_conjecture,
( X1 = esk2_1(X1)
| esk2_1(X1) = g(f(esk2_1(X1)))
| X2 = esk1_1(X2)
| esk1_1(X2) = f(g(esk1_1(X2))) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(9,negated_conjecture,
( X1 = esk2_1(X1)
| esk2_1(X1) = g(f(esk2_1(X1)))
| X2 != esk1_1(X2)
| esk1_1(X2) != f(g(esk1_1(X2))) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(10,negated_conjecture,
( X2 = esk1_1(X2)
| esk1_1(X2) = f(g(esk1_1(X2)))
| X1 != esk2_1(X1)
| esk2_1(X1) != g(f(esk2_1(X1))) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(11,negated_conjecture,
( X1 != esk2_1(X1)
| esk2_1(X1) != g(f(esk2_1(X1)))
| X2 != esk1_1(X2)
| esk1_1(X2) != f(g(esk1_1(X2))) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(12,negated_conjecture,
( X1 = g(f(X1))
| X2 = f(g(X2))
| esk4_0 != X1
| esk3_0 != X2 ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(13,negated_conjecture,
( X1 = g(f(X1))
| esk3_0 = X2
| esk4_0 != X1
| X2 != f(g(X2)) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(14,negated_conjecture,
( esk4_0 = X1
| X2 = f(g(X2))
| X1 != g(f(X1))
| esk3_0 != X2 ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(15,negated_conjecture,
( esk4_0 = X1
| esk3_0 = X2
| X1 != g(f(X1))
| X2 != f(g(X2)) ),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(16,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(X1)) = X1
| esk4_0 != X1 ),
inference(er,[status(thm)],[12,theory(equality)]) ).
cnf(17,negated_conjecture,
( g(f(X1)) = X1
| esk3_0 = esk1_1(X2)
| g(f(esk2_1(X3))) = esk2_1(X3)
| esk2_1(X3) = X3
| esk1_1(X2) = X2
| esk4_0 != X1 ),
inference(spm,[status(thm)],[13,8,theory(equality)]) ).
cnf(19,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = g(esk1_1(X2))
| g(f(esk2_1(X3))) = esk2_1(X3)
| esk2_1(X3) = X3
| esk1_1(X2) = X2
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,8,theory(equality)]) ).
cnf(20,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = esk2_1(X2)
| f(g(esk1_1(X3))) = esk1_1(X3)
| esk2_1(X2) = X2
| esk1_1(X3) = X3
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,8,theory(equality)]) ).
cnf(21,negated_conjecture,
( esk4_0 = g(esk1_1(X1))
| esk3_0 = X2
| g(f(esk2_1(X3))) = esk2_1(X3)
| esk2_1(X3) = X3
| esk1_1(X1) = X1
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,8,theory(equality)]) ).
cnf(22,negated_conjecture,
( esk4_0 = esk2_1(X1)
| esk3_0 = X2
| f(g(esk1_1(X3))) = esk1_1(X3)
| esk2_1(X1) = X1
| esk1_1(X3) = X3
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,8,theory(equality)]) ).
fof(25,plain,
( ~ epred1_0
<=> ! [X1] :
( esk2_1(X1) != X1
| g(f(esk2_1(X1))) != esk2_1(X1) ) ),
introduced(definition),
[split] ).
cnf(26,plain,
( epred1_0
| esk2_1(X1) != X1
| g(f(esk2_1(X1))) != esk2_1(X1) ),
inference(split_equiv,[status(thm)],[25]) ).
fof(27,plain,
( ~ epred2_0
<=> ! [X2] :
( esk1_1(X2) != X2
| f(g(esk1_1(X2))) != esk1_1(X2) ) ),
introduced(definition),
[split] ).
cnf(28,plain,
( epred2_0
| esk1_1(X2) != X2
| f(g(esk1_1(X2))) != esk1_1(X2) ),
inference(split_equiv,[status(thm)],[27]) ).
cnf(29,negated_conjecture,
( ~ epred2_0
| ~ epred1_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[11,25,theory(equality)]),27,theory(equality)]),
[split] ).
cnf(33,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk1_1(X1) = X1
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) != X2
| esk4_0 != esk2_1(X2) ),
inference(spm,[status(thm)],[10,16,theory(equality)]) ).
cnf(35,negated_conjecture,
( epred1_0
| f(g(esk3_0)) = esk3_0
| esk2_1(X1) != X1
| esk4_0 != esk2_1(X1) ),
inference(spm,[status(thm)],[26,16,theory(equality)]) ).
cnf(51,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1 ),
inference(er,[status(thm)],[17,theory(equality)]) ).
cnf(52,negated_conjecture,
( g(f(esk2_1(X3))) = esk2_1(X3)
| g(f(esk4_0)) = esk4_0
| esk2_1(X3) = X3
| esk1_1(X4) = X4
| esk3_0 != X4 ),
inference(ef,[status(thm)],[51,theory(equality)]) ).
cnf(53,negated_conjecture,
( g(f(esk2_1(X5))) = esk2_1(X5)
| g(f(esk4_0)) = esk4_0
| esk1_1(X6) = esk3_0
| esk2_1(X5) = X5
| X6 != esk3_0 ),
inference(ef,[status(thm)],[51,theory(equality)]) ).
cnf(55,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = esk2_1(X2)
| g(f(esk4_0)) = esk4_0
| esk1_1(X3) = esk3_0
| esk2_1(X2) = X2
| esk1_1(X3) = X3
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,51,theory(equality)]) ).
cnf(57,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk2_1(X2))) = esk2_1(X2)
| esk2_1(X2) = X2
| esk3_0 = X1
| g(f(esk2_1(X3))) = esk2_1(X3)
| g(f(esk4_0)) = esk4_0
| esk2_1(X3) = X3
| esk1_1(X1) = X1 ),
inference(spm,[status(thm)],[8,51,theory(equality)]) ).
cnf(72,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1 ),
inference(er,[status(thm)],[53,theory(equality)]) ).
cnf(73,negated_conjecture,
( g(f(X1)) = X1
| esk3_0 = f(esk2_1(X2))
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X2) = X2
| esk4_0 != X1 ),
inference(spm,[status(thm)],[13,72,theory(equality)]) ).
cnf(81,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(esk1_1(X2)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1 ),
inference(er,[status(thm)],[19,theory(equality)]) ).
cnf(121,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = esk2_1(X2)
| f(g(esk3_0)) = esk3_0
| g(esk1_1(X3)) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X3) = X3
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,81,theory(equality)]) ).
cnf(123,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| g(f(esk2_1(X2))) = esk2_1(X2)
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| g(f(esk2_1(X3))) = esk2_1(X3)
| f(g(esk3_0)) = esk3_0
| esk2_1(X3) = X3 ),
inference(spm,[status(thm)],[8,81,theory(equality)]) ).
cnf(135,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(esk2_1(X1)) = esk3_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1 ),
inference(er,[status(thm)],[73,theory(equality)]) ).
cnf(143,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[72,135,theory(equality)]) ).
cnf(147,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X2) = X2
| g(esk3_0) != X2 ),
inference(ef,[status(thm)],[143,theory(equality)]) ).
cnf(162,negated_conjecture,
( g(f(g(esk3_0))) = g(esk3_0)
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| g(esk3_0) = X1
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[72,143,theory(equality)]) ).
cnf(168,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = esk4_0
| esk1_1(X1) = X1
| esk2_1(X2) = X2 ),
inference(er,[status(thm)],[20,theory(equality)]) ).
cnf(199,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(g(esk3_0)) = g(esk3_0) ),
inference(er,[status(thm)],[147,theory(equality)]) ).
cnf(201,negated_conjecture,
( epred1_0
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| g(f(g(esk3_0))) != g(esk3_0) ),
inference(spm,[status(thm)],[26,199,theory(equality)]) ).
cnf(205,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(esk1_1(X2)) = esk4_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| esk3_0 = esk1_1(X3)
| g(f(esk2_1(X4))) = esk2_1(X4)
| esk2_1(X4) = X4
| esk1_1(X3) = X3 ),
inference(spm,[status(thm)],[21,8,theory(equality)]) ).
cnf(233,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk2_1(X2) = esk4_0
| esk1_1(X1) = X1
| esk2_1(X2) = X2
| esk3_0 = f(esk2_1(X3))
| f(g(esk1_1(X4))) = esk1_1(X4)
| esk2_1(X3) = X3
| esk1_1(X4) = X4 ),
inference(spm,[status(thm)],[22,8,theory(equality)]) ).
cnf(248,negated_conjecture,
( f(g(esk1_1(X3))) = esk1_1(X3)
| f(g(esk3_0)) = esk3_0
| esk2_1(X4) = X4
| esk1_1(X3) = X3
| esk4_0 != X4 ),
inference(ef,[status(thm)],[168,theory(equality)]) ).
cnf(249,negated_conjecture,
( f(g(esk1_1(X5))) = esk1_1(X5)
| f(g(esk3_0)) = esk3_0
| esk2_1(X6) = esk4_0
| esk1_1(X5) = X5
| X6 != esk4_0 ),
inference(ef,[status(thm)],[168,theory(equality)]) ).
cnf(253,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| g(f(esk4_0)) = esk4_0
| esk4_0 = X2
| esk1_1(X1) = X1
| f(g(esk1_1(X3))) = esk1_1(X3)
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = X2
| esk1_1(X3) = X3 ),
inference(spm,[status(thm)],[8,168,theory(equality)]) ).
cnf(283,negated_conjecture,
( g(f(g(esk3_0))) = g(esk3_0)
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1 ),
inference(csr,[status(thm)],[162,147]) ).
cnf(295,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| epred1_0
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[201,283,theory(equality)]) ).
cnf(299,negated_conjecture,
( epred1_0
| g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| g(f(X1)) != X1 ),
inference(spm,[status(thm)],[26,295,theory(equality)]) ).
cnf(441,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1 ),
inference(er,[status(thm)],[249,theory(equality)]) ).
cnf(443,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = g(esk1_1(X2))
| f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X2) = X2
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,441,theory(equality)]) ).
cnf(609,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X1)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1 ),
inference(er,[status(thm)],[443,theory(equality)]) ).
cnf(624,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1 ),
inference(spm,[status(thm)],[441,609,theory(equality)]) ).
cnf(686,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X2) = X2
| f(esk4_0) != X2 ),
inference(ef,[status(thm)],[624,theory(equality)]) ).
cnf(713,negated_conjecture,
( epred2_0
| f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| f(g(X1)) != X1
| f(esk4_0) != X1 ),
inference(spm,[status(thm)],[28,686,theory(equality)]) ).
cnf(752,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| epred2_0
| esk1_1(X1) = X1
| f(esk4_0) != esk1_1(X1) ),
inference(spm,[status(thm)],[713,441,theory(equality)]) ).
cnf(760,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(csr,[status(thm)],[752,624]) ).
cnf(762,negated_conjecture,
( epred2_0
| f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| f(g(X1)) != X1 ),
inference(spm,[status(thm)],[28,760,theory(equality)]) ).
cnf(767,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| epred2_0
| esk4_0 != X1 ),
inference(spm,[status(thm)],[762,16,theory(equality)]) ).
cnf(785,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| epred2_0 ),
inference(er,[status(thm)],[767,theory(equality)]) ).
cnf(789,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[33,785,theory(equality)]) ).
cnf(801,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = esk3_0
| esk2_1(X2) = esk4_0
| esk1_1(X1) = X1
| esk2_1(X2) = X2 ),
inference(er,[status(thm)],[55,theory(equality)]) ).
cnf(803,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = g(esk1_1(X2))
| f(g(esk3_0)) = esk3_0
| esk1_1(X2) = X2
| epred2_0
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,789,theory(equality)]) ).
cnf(851,negated_conjecture,
( epred1_0
| f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = esk4_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| g(f(X1)) != X1 ),
inference(spm,[status(thm)],[26,801,theory(equality)]) ).
cnf(981,negated_conjecture,
( g(f(esk2_1(X2))) = esk2_1(X2)
| g(f(esk2_1(X3))) = esk2_1(X3)
| f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| esk2_1(X3) = X3 ),
inference(csr,[status(thm)],[57,52]) ).
cnf(982,negated_conjecture,
( g(f(esk2_1(X4))) = esk2_1(X4)
| g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X5) = X5
| esk2_1(X4) = X4 ),
inference(ef,[status(thm)],[981,theory(equality)]) ).
cnf(1183,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X1)) = esk4_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(er,[status(thm)],[803,theory(equality)]) ).
cnf(1207,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[789,1183,theory(equality)]) ).
cnf(1211,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X2) = X2
| epred2_0
| f(esk4_0) != X2 ),
inference(ef,[status(thm)],[1207,theory(equality)]) ).
cnf(1247,negated_conjecture,
( epred2_0
| f(g(esk3_0)) = esk3_0
| f(g(X1)) != X1
| f(esk4_0) != X1 ),
inference(spm,[status(thm)],[28,1211,theory(equality)]) ).
cnf(1302,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred2_0
| esk1_1(X1) = X1
| f(esk4_0) != esk1_1(X1) ),
inference(spm,[status(thm)],[1247,789,theory(equality)]) ).
cnf(1404,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(csr,[status(thm)],[1302,1207]) ).
cnf(1406,negated_conjecture,
( epred2_0
| f(g(esk3_0)) = esk3_0
| f(g(X1)) != X1 ),
inference(spm,[status(thm)],[28,1404,theory(equality)]) ).
cnf(1412,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred2_0
| esk4_0 != X1 ),
inference(spm,[status(thm)],[1406,16,theory(equality)]) ).
cnf(1438,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred2_0 ),
inference(er,[status(thm)],[1412,theory(equality)]) ).
cnf(1439,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = g(esk3_0)
| epred2_0
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,1438,theory(equality)]) ).
cnf(1440,negated_conjecture,
( esk4_0 = g(esk3_0)
| esk3_0 = X1
| epred2_0
| f(g(X1)) != X1 ),
inference(spm,[status(thm)],[15,1438,theory(equality)]) ).
cnf(1569,negated_conjecture,
( epred2_0
| g(esk3_0) = esk4_0
| esk1_1(X1) != X1
| esk3_0 != esk1_1(X1) ),
inference(spm,[status(thm)],[28,1439,theory(equality)]) ).
cnf(1584,negated_conjecture,
( g(esk3_0) = esk4_0
| esk3_0 = esk1_1(X1)
| epred2_0
| g(f(esk2_1(X2))) = esk2_1(X2)
| esk2_1(X2) = X2
| esk1_1(X1) = X1 ),
inference(spm,[status(thm)],[1440,8,theory(equality)]) ).
cnf(1768,negated_conjecture,
( g(f(esk2_1(X3))) = esk2_1(X3)
| g(esk3_0) = esk4_0
| esk1_1(X4) = X4
| esk2_1(X3) = X3
| epred2_0
| esk3_0 != X4 ),
inference(ef,[status(thm)],[1584,theory(equality)]) ).
cnf(1826,negated_conjecture,
( g(esk3_0) = esk4_0
| esk3_0 = f(esk2_1(X1))
| epred2_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[1440,1584,theory(equality)]) ).
cnf(1831,negated_conjecture,
( f(esk2_1(X3)) = esk3_0
| g(esk3_0) = esk4_0
| esk2_1(X3) = X3
| esk1_1(X4) = X4
| epred2_0
| esk3_0 != X4 ),
inference(ef,[status(thm)],[1826,theory(equality)]) ).
cnf(1901,negated_conjecture,
( f(esk2_1(X1)) = esk3_0
| g(esk3_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(er,[status(thm)],[1831,theory(equality)]) ).
cnf(2049,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(esk3_0) = esk4_0
| esk2_1(X1) = X1
| esk1_1(esk3_0) = esk3_0
| epred2_0 ),
inference(er,[status(thm)],[1768,theory(equality)]) ).
cnf(2080,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| esk1_1(esk3_0) = esk3_0
| g(esk3_0) = esk4_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[2049,1901,theory(equality)]) ).
cnf(2114,negated_conjecture,
( g(esk3_0) = esk4_0
| epred2_0
| esk2_1(X1) = g(esk3_0)
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[1569,2080,theory(equality)]) ).
cnf(2120,negated_conjecture,
( g(esk3_0) = esk4_0
| esk2_1(X2) = X2
| epred2_0
| g(esk3_0) != X2 ),
inference(ef,[status(thm)],[2114,theory(equality)]) ).
cnf(2182,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk1_1(X1) = X1
| g(esk3_0) = esk4_0
| epred2_0
| g(f(X2)) != X2
| g(esk3_0) != X2 ),
inference(spm,[status(thm)],[10,2120,theory(equality)]) ).
cnf(2859,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X1)) = esk4_0
| esk2_1(X2) = esk4_0
| esk1_1(X1) = X1
| esk2_1(X2) = X2 ),
inference(er,[status(thm)],[121,theory(equality)]) ).
cnf(2872,negated_conjecture,
( epred1_0
| f(g(esk3_0)) = esk3_0
| g(esk1_1(X2)) = esk4_0
| esk2_1(X1) = esk4_0
| esk1_1(X2) = X2
| g(f(X1)) != X1 ),
inference(spm,[status(thm)],[26,2859,theory(equality)]) ).
cnf(2953,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X1)) = esk4_0
| esk2_1(esk2_1(X2)) = esk4_0
| esk1_1(X1) = X1
| epred1_0
| g(esk1_1(X3)) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X3) = X3 ),
inference(spm,[status(thm)],[2872,81,theory(equality)]) ).
cnf(2993,negated_conjecture,
( g(f(esk2_1(X4))) = esk2_1(X4)
| f(g(esk3_0)) = esk3_0
| esk1_1(X5) = f(esk4_0)
| esk2_1(X4) = X4
| esk1_1(X5) = X5 ),
inference(ef,[status(thm)],[123,theory(equality)]) ).
cnf(3667,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| g(esk3_0) = esk4_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[2182,1438,theory(equality)]) ).
cnf(3710,negated_conjecture,
( g(esk3_0) = esk4_0
| esk3_0 = esk1_1(X1)
| epred2_0
| esk1_1(X1) = X1 ),
inference(spm,[status(thm)],[1440,3667,theory(equality)]) ).
cnf(3723,negated_conjecture,
( g(esk3_0) = esk4_0
| esk1_1(X2) = X2
| epred2_0
| esk3_0 != X2 ),
inference(ef,[status(thm)],[3710,theory(equality)]) ).
cnf(3762,negated_conjecture,
( g(esk3_0) = esk4_0
| epred2_0
| X1 != esk3_0 ),
inference(spm,[status(thm)],[1569,3723,theory(equality)]) ).
cnf(3764,negated_conjecture,
( g(esk3_0) = esk4_0
| epred2_0 ),
inference(er,[status(thm)],[3762,theory(equality)]) ).
cnf(3769,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[283,3764,theory(equality)]) ).
cnf(3772,negated_conjecture,
( f(esk4_0) = esk3_0
| epred2_0 ),
inference(spm,[status(thm)],[1438,3764,theory(equality)]) ).
cnf(3801,negated_conjecture,
( epred2_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1
| f(g(esk3_0)) != esk3_0 ),
inference(spm,[status(thm)],[28,3769,theory(equality)]) ).
cnf(3807,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(csr,[status(thm)],[3801,1438]) ).
cnf(3808,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk1_1(X1) = X1
| g(f(esk4_0)) = esk4_0
| epred2_0
| g(f(X2)) != X2 ),
inference(spm,[status(thm)],[10,3807,theory(equality)]) ).
cnf(3976,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| g(f(esk4_0)) = esk4_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[3808,1438,theory(equality)]) ).
cnf(3985,negated_conjecture,
( g(f(X1)) = X1
| esk3_0 = esk1_1(X2)
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = X2
| epred2_0
| esk4_0 != X1 ),
inference(spm,[status(thm)],[13,3976,theory(equality)]) ).
cnf(4180,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(X1) = esk3_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(er,[status(thm)],[3985,theory(equality)]) ).
cnf(4182,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(X3) = esk3_0
| epred2_0
| X3 != esk3_0 ),
inference(ef,[status(thm)],[4180,theory(equality)]) ).
cnf(4222,negated_conjecture,
( epred2_0
| g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) != esk3_0
| esk3_0 != X1 ),
inference(spm,[status(thm)],[28,4182,theory(equality)]) ).
cnf(4270,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| epred2_0
| esk3_0 != X1 ),
inference(csr,[status(thm)],[4222,1438]) ).
cnf(4271,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| epred2_0 ),
inference(er,[status(thm)],[4270,theory(equality)]) ).
cnf(4337,negated_conjecture,
( g(f(esk2_1(X5))) = esk2_1(X5)
| g(esk1_1(X6)) = esk4_0
| esk1_1(X7) = esk3_0
| esk1_1(X7) = X7
| esk2_1(X5) = X5
| esk1_1(X6) = X6 ),
inference(ef,[status(thm)],[205,theory(equality)]) ).
cnf(4649,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = esk3_0
| esk2_1(esk2_1(X2)) = esk4_0
| esk1_1(X1) = X1
| epred1_0
| esk2_1(X2) = X2
| esk1_1(X3) = X3 ),
inference(spm,[status(thm)],[851,982,theory(equality)]) ).
cnf(4925,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(esk2_1(X11)) = esk4_0
| esk1_1(X12) = esk3_0
| esk2_1(X11) = X11
| esk1_1(X12) = X12
| epred1_0 ),
inference(ef,[status(thm)],[4649,theory(equality)]) ).
cnf(5006,negated_conjecture,
( f(g(esk1_1(X5))) = esk1_1(X5)
| f(esk2_1(X6)) = esk3_0
| esk2_1(X7) = esk4_0
| esk1_1(X5) = X5
| esk2_1(X6) = X6
| esk2_1(X7) = X7 ),
inference(ef,[status(thm)],[233,theory(equality)]) ).
cnf(5386,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| esk4_0 != esk2_1(X1) ),
inference(spm,[status(thm)],[35,4925,theory(equality)]) ).
cnf(5545,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| epred1_0 ),
inference(csr,[status(thm)],[5386,801]) ).
cnf(5555,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = esk3_0
| esk1_1(X2) = X2
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,5545,theory(equality)]) ).
cnf(5650,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = esk3_0
| esk1_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[5555,theory(equality)]) ).
cnf(5651,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = X2
| epred1_0
| esk3_0 != X2 ),
inference(ef,[status(thm)],[5650,theory(equality)]) ).
cnf(5741,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| f(g(esk1_1(X3))) = esk1_1(X3)
| g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X3) = X3
| esk2_1(X2) = X2
| esk1_1(X1) = X1 ),
inference(csr,[status(thm)],[253,248]) ).
cnf(5742,negated_conjecture,
( f(g(esk1_1(X4))) = esk1_1(X4)
| f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X4) = X4
| esk2_1(X5) = X5 ),
inference(ef,[status(thm)],[5741,theory(equality)]) ).
cnf(5858,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X2) = X2
| esk3_0 = X1
| esk1_1(X1) = X1
| epred1_0 ),
inference(spm,[status(thm)],[5742,5650,theory(equality)]) ).
cnf(5865,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| epred1_0 ),
inference(csr,[status(thm)],[5858,5651]) ).
cnf(5870,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(f(esk4_0)) = esk4_0
| esk1_1(X2) = X2
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,5865,theory(equality)]) ).
cnf(5879,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[5870,theory(equality)]) ).
cnf(5880,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| epred1_0
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[9,5879,theory(equality)]) ).
cnf(5940,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk2_1(X1) = X1
| epred1_0
| esk4_0 != X2 ),
inference(spm,[status(thm)],[5880,16,theory(equality)]) ).
cnf(6207,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[5940,theory(equality)]) ).
cnf(6212,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = esk2_1(X2)
| g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = X2
| epred1_0
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,6207,theory(equality)]) ).
cnf(6288,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = esk4_0
| esk2_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[6212,theory(equality)]) ).
cnf(6289,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = X2
| epred1_0
| esk4_0 != X2 ),
inference(ef,[status(thm)],[6288,theory(equality)]) ).
cnf(6320,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(f(esk4_0)) = esk4_0
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,6289,theory(equality)]) ).
cnf(6322,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| f(g(esk3_0)) = esk3_0
| epred1_0 ),
inference(er,[status(thm)],[6320,theory(equality)]) ).
cnf(6401,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk2_1(X5)) = esk4_0
| g(esk1_1(X4)) = esk4_0
| esk1_1(X4) = X4
| esk2_1(X5) = X5
| epred1_0 ),
inference(ef,[status(thm)],[2953,theory(equality)]) ).
cnf(6563,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(esk1_1(X2)) = esk4_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2
| esk4_0 != esk2_1(X1) ),
inference(spm,[status(thm)],[35,6401,theory(equality)]) ).
cnf(6619,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X2)) = esk4_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2
| epred1_0 ),
inference(csr,[status(thm)],[6563,2859]) ).
cnf(6626,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| g(esk1_1(X2)) = esk4_0
| esk1_1(X2) = X2
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,6619,theory(equality)]) ).
cnf(6651,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| g(esk1_1(X1)) = esk4_0
| esk1_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[6626,theory(equality)]) ).
cnf(6660,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| epred1_0 ),
inference(spm,[status(thm)],[168,6651,theory(equality)]) ).
cnf(6697,negated_conjecture,
( epred1_0
| f(g(esk3_0)) = esk3_0
| esk1_1(X2) = f(esk4_0)
| esk2_1(X1) = esk4_0
| esk1_1(X2) = X2
| g(f(X1)) != X1 ),
inference(spm,[status(thm)],[26,6660,theory(equality)]) ).
cnf(6918,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X1) = f(esk4_0)
| esk2_1(esk2_1(X2)) = esk4_0
| esk1_1(X1) = X1
| epred1_0
| esk1_1(X3) = f(esk4_0)
| esk1_1(X3) = X3
| esk2_1(X2) = X2 ),
inference(spm,[status(thm)],[6697,2993,theory(equality)]) ).
cnf(9264,negated_conjecture,
( g(f(esk2_1(X4))) = esk2_1(X4)
| g(esk1_1(X5)) = esk4_0
| esk1_1(X5) = X5
| esk2_1(X4) = X4
| esk1_1(X6) = X6
| esk3_0 != X6 ),
inference(ef,[status(thm)],[4337,theory(equality)]) ).
cnf(9279,negated_conjecture,
( epred2_0
| g(f(esk2_1(X2))) = esk2_1(X2)
| g(esk1_1(X3)) = esk4_0
| esk1_1(X1) = esk3_0
| esk1_1(X3) = X3
| esk2_1(X2) = X2
| f(g(X1)) != X1 ),
inference(spm,[status(thm)],[28,4337,theory(equality)]) ).
cnf(9374,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(esk2_1(X5)) = esk4_0
| esk1_1(X4) = f(esk4_0)
| esk2_1(X5) = X5
| esk1_1(X4) = X4
| epred1_0 ),
inference(ef,[status(thm)],[6918,theory(equality)]) ).
cnf(9498,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| esk1_1(X2) = f(esk4_0)
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| esk4_0 != esk2_1(X1) ),
inference(spm,[status(thm)],[35,9374,theory(equality)]) ).
cnf(9580,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X2) = f(esk4_0)
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| epred1_0 ),
inference(csr,[status(thm)],[9498,6660]) ).
cnf(9590,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| esk1_1(X2) = f(esk4_0)
| esk1_1(X2) = X2
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,9580,theory(equality)]) ).
cnf(9627,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X1) = f(esk4_0)
| esk1_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[9590,theory(equality)]) ).
cnf(9628,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk1_1(X2) = X2
| epred1_0
| f(esk4_0) != X2 ),
inference(ef,[status(thm)],[9627,theory(equality)]) ).
cnf(9694,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| f(g(esk3_0)) = esk3_0
| epred1_0
| f(g(X2)) != X2
| f(esk4_0) != X2 ),
inference(spm,[status(thm)],[9,9628,theory(equality)]) ).
cnf(9870,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| f(g(esk3_0)) = esk3_0
| esk2_1(X1) = X1
| epred1_0 ),
inference(spm,[status(thm)],[9694,6322,theory(equality)]) ).
cnf(9881,negated_conjecture,
( f(g(X1)) = X1
| esk4_0 = esk2_1(X2)
| f(g(esk3_0)) = esk3_0
| esk2_1(X2) = X2
| epred1_0
| esk3_0 != X1 ),
inference(spm,[status(thm)],[14,9870,theory(equality)]) ).
cnf(9920,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(X1) = esk4_0
| esk2_1(X1) = X1
| epred1_0 ),
inference(er,[status(thm)],[9881,theory(equality)]) ).
cnf(9925,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| esk2_1(X2) = X2
| epred1_0
| esk4_0 != X2 ),
inference(ef,[status(thm)],[9920,theory(equality)]) ).
cnf(9962,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0
| X1 != esk4_0 ),
inference(spm,[status(thm)],[35,9925,theory(equality)]) ).
cnf(9966,negated_conjecture,
( f(g(esk3_0)) = esk3_0
| epred1_0 ),
inference(er,[status(thm)],[9962,theory(equality)]) ).
cnf(9968,negated_conjecture,
( esk4_0 = g(esk3_0)
| esk3_0 = X1
| epred1_0
| f(g(X1)) != X1 ),
inference(spm,[status(thm)],[15,9966,theory(equality)]) ).
cnf(9969,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| epred1_0 ),
inference(spm,[status(thm)],[299,9966,theory(equality)]) ).
cnf(9981,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| g(f(esk4_0)) = esk4_0
| epred1_0
| f(g(esk3_0)) != esk3_0 ),
inference(spm,[status(thm)],[9,9969,theory(equality)]) ).
cnf(10262,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1
| epred1_0 ),
inference(csr,[status(thm)],[9981,9966]) ).
cnf(10294,negated_conjecture,
( g(esk3_0) = esk4_0
| esk3_0 = f(esk2_1(X1))
| epred1_0
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[9968,10262,theory(equality)]) ).
cnf(10329,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| g(f(esk4_0)) = esk4_0
| esk2_1(X1) = X1
| epred1_0
| g(esk3_0) = esk4_0 ),
inference(spm,[status(thm)],[10262,10294,theory(equality)]) ).
cnf(10330,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| g(esk3_0) = esk4_0
| esk2_1(X2) = X2
| epred1_0
| g(esk3_0) != X2 ),
inference(ef,[status(thm)],[10329,theory(equality)]) ).
cnf(10369,negated_conjecture,
( epred1_0
| g(f(esk4_0)) = esk4_0
| g(esk3_0) = esk4_0
| g(f(X1)) != X1
| g(esk3_0) != X1 ),
inference(spm,[status(thm)],[26,10330,theory(equality)]) ).
cnf(10469,negated_conjecture,
( g(f(esk4_0)) = esk4_0
| g(esk3_0) = esk4_0
| epred1_0 ),
inference(spm,[status(thm)],[10369,9966,theory(equality)]) ).
cnf(10495,negated_conjecture,
( g(esk3_0) = esk4_0
| esk3_0 = f(esk4_0)
| epred1_0 ),
inference(spm,[status(thm)],[9968,10469,theory(equality)]) ).
cnf(10512,negated_conjecture,
( f(esk4_0) = esk3_0
| epred1_0 ),
inference(spm,[status(thm)],[9966,10495,theory(equality)]) ).
cnf(10524,negated_conjecture,
( g(esk3_0) = esk4_0
| epred1_0 ),
inference(spm,[status(thm)],[10469,10512,theory(equality)]) ).
cnf(11764,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(esk1_1(X2)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2
| epred2_0 ),
inference(spm,[status(thm)],[9279,1438,theory(equality)]) ).
cnf(11791,negated_conjecture,
( esk4_0 = esk2_1(X1)
| esk3_0 = X2
| g(esk1_1(X3)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X3) = X3
| esk2_1(X1) = X1
| epred2_0
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,11764,theory(equality)]) ).
cnf(12412,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X2) = esk4_0
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| esk3_0 = f(esk2_1(X3))
| epred2_0
| g(esk1_1(X4)) = esk4_0
| esk1_1(X4) = X4
| esk2_1(X3) = X3 ),
inference(spm,[status(thm)],[11791,11764,theory(equality)]) ).
cnf(12825,negated_conjecture,
( f(esk2_1(X6)) = esk3_0
| g(esk1_1(X5)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X7) = esk4_0
| esk2_1(X6) = X6
| esk1_1(X5) = X5
| esk2_1(X7) = X7
| epred2_0 ),
inference(ef,[status(thm)],[12412,theory(equality)]) ).
cnf(13014,negated_conjecture,
( g(esk1_1(X4)) = esk4_0
| f(esk2_1(X5)) = esk3_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X6) = X6
| esk1_1(X4) = X4
| esk2_1(X5) = X5
| epred2_0
| esk4_0 != X6 ),
inference(ef,[status(thm)],[12825,theory(equality)]) ).
cnf(13112,negated_conjecture,
( f(esk2_1(X1)) = esk3_0
| g(esk1_1(X2)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2
| esk2_1(esk4_0) = esk4_0
| epred2_0 ),
inference(er,[status(thm)],[13014,theory(equality)]) ).
cnf(13393,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| g(esk1_1(X2)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2 ),
inference(er,[status(thm)],[9264,theory(equality)]) ).
cnf(13512,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| g(esk1_1(X2)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X2) = X2
| esk2_1(X1) = X1
| g(esk1_1(X3)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X3) = X3
| epred2_0 ),
inference(spm,[status(thm)],[13393,13112,theory(equality)]) ).
cnf(14327,negated_conjecture,
( g(esk1_1(X4)) = esk4_0
| esk2_1(X5) = g(esk3_0)
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X4) = X4
| esk2_1(X5) = X5
| epred2_0 ),
inference(ef,[status(thm)],[13512,theory(equality)]) ).
cnf(14446,negated_conjecture,
( g(esk1_1(X4)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X3) = X3
| esk1_1(X4) = X4
| epred2_0
| g(esk3_0) != X3 ),
inference(ef,[status(thm)],[14327,theory(equality)]) ).
cnf(14524,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X1) = X1
| esk2_1(g(esk3_0)) = g(esk3_0)
| epred2_0 ),
inference(er,[status(thm)],[14446,theory(equality)]) ).
cnf(14543,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| g(esk1_1(X1)) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[14524,3764,theory(equality)]) ).
cnf(14575,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| g(f(esk2_1(X2))) = esk2_1(X2)
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| epred2_0 ),
inference(spm,[status(thm)],[8,14543,theory(equality)]) ).
cnf(14649,negated_conjecture,
( f(g(esk1_1(X7))) = esk1_1(X7)
| f(esk2_1(X8)) = esk3_0
| esk2_1(X9) = esk4_0
| esk2_1(X8) = X8
| esk1_1(X7) = X7
| X9 != esk4_0 ),
inference(ef,[status(thm)],[5006,theory(equality)]) ).
cnf(14771,negated_conjecture,
( g(f(esk2_1(X3))) = esk2_1(X3)
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X4) = X4
| esk2_1(X3) = X3
| epred2_0
| f(esk4_0) != X4 ),
inference(ef,[status(thm)],[14575,theory(equality)]) ).
cnf(14853,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1
| esk1_1(X2) = X2
| epred2_0
| esk3_0 != X2 ),
inference(spm,[status(thm)],[14771,3772,theory(equality)]) ).
cnf(14912,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(er,[status(thm)],[14853,theory(equality)]) ).
cnf(14915,negated_conjecture,
( esk4_0 = esk2_1(X1)
| esk3_0 = X2
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1
| epred2_0
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,14912,theory(equality)]) ).
cnf(15024,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = esk4_0
| esk2_1(X1) = X1
| esk3_0 = f(esk2_1(X2))
| epred2_0
| esk2_1(X2) = X2 ),
inference(spm,[status(thm)],[14915,14912,theory(equality)]) ).
cnf(15038,negated_conjecture,
( f(esk2_1(X3)) = esk3_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X3) = X3
| esk2_1(X4) = X4
| epred2_0
| esk4_0 != X4 ),
inference(ef,[status(thm)],[15024,theory(equality)]) ).
cnf(15115,negated_conjecture,
( f(esk2_1(X1)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(er,[status(thm)],[15038,theory(equality)]) ).
cnf(15150,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1
| epred2_0 ),
inference(spm,[status(thm)],[14912,15115,theory(equality)]) ).
cnf(15151,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk2_1(X2) = X2
| epred2_0
| g(esk3_0) != X2 ),
inference(ef,[status(thm)],[15150,theory(equality)]) ).
cnf(15195,negated_conjecture,
( esk1_1(esk3_0) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(g(esk3_0)) = g(esk3_0)
| epred2_0 ),
inference(er,[status(thm)],[15151,theory(equality)]) ).
cnf(15200,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| epred2_0 ),
inference(spm,[status(thm)],[15195,3764,theory(equality)]) ).
cnf(15209,negated_conjecture,
( epred2_0
| esk2_1(esk4_0) = esk4_0
| f(g(esk3_0)) != esk3_0 ),
inference(spm,[status(thm)],[28,15200,theory(equality)]) ).
cnf(15212,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| epred2_0 ),
inference(csr,[status(thm)],[15209,1438]) ).
cnf(15213,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk1_1(X1) = X1
| epred2_0
| g(f(esk4_0)) != esk4_0 ),
inference(spm,[status(thm)],[10,15212,theory(equality)]) ).
cnf(15217,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk1_1(X1) = X1
| epred2_0 ),
inference(csr,[status(thm)],[15213,4271]) ).
cnf(15220,negated_conjecture,
( esk4_0 = g(esk1_1(X1))
| esk3_0 = X2
| esk1_1(X1) = X1
| epred2_0
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,15217,theory(equality)]) ).
cnf(15310,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk1_1(X1) = X1
| esk3_0 = esk1_1(X2)
| epred2_0
| esk1_1(X2) = X2 ),
inference(spm,[status(thm)],[15220,15217,theory(equality)]) ).
cnf(15313,negated_conjecture,
( g(esk1_1(X3)) = esk4_0
| esk1_1(X4) = X4
| esk1_1(X3) = X3
| epred2_0
| esk3_0 != X4 ),
inference(ef,[status(thm)],[15310,theory(equality)]) ).
cnf(15394,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk1_1(X1) = X1
| esk1_1(esk3_0) = esk3_0
| epred2_0 ),
inference(er,[status(thm)],[15313,theory(equality)]) ).
cnf(15435,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| esk1_1(X1) = X1
| epred2_0
| esk1_1(esk3_0) = esk3_0 ),
inference(spm,[status(thm)],[15217,15394,theory(equality)]) ).
cnf(15438,negated_conjecture,
( esk1_1(esk3_0) = esk3_0
| epred2_0
| f(esk4_0) != esk3_0 ),
inference(ef,[status(thm)],[15435,theory(equality)]) ).
cnf(15492,negated_conjecture,
( esk1_1(esk3_0) = esk3_0
| epred2_0 ),
inference(csr,[status(thm)],[15438,3772]) ).
cnf(15494,negated_conjecture,
( epred2_0
| f(g(esk3_0)) != esk3_0 ),
inference(spm,[status(thm)],[28,15492,theory(equality)]) ).
cnf(15497,negated_conjecture,
epred2_0,
inference(csr,[status(thm)],[15494,1438]) ).
cnf(15515,negated_conjecture,
( $false
| ~ epred1_0 ),
inference(rw,[status(thm)],[29,15497,theory(equality)]) ).
cnf(15516,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[15515,theory(equality)]) ).
cnf(15527,negated_conjecture,
f(esk4_0) = esk3_0,
inference(sr,[status(thm)],[10512,15516,theory(equality)]) ).
cnf(15528,negated_conjecture,
g(esk3_0) = esk4_0,
inference(sr,[status(thm)],[10524,15516,theory(equality)]) ).
cnf(15704,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| f(esk2_1(X2)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| esk2_1(X2) = X2 ),
inference(er,[status(thm)],[14649,theory(equality)]) ).
cnf(15710,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| g(esk3_0) = esk2_1(X2)
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| f(g(esk1_1(X3))) = esk1_1(X3)
| esk2_1(esk4_0) = esk4_0
| esk1_1(X3) = X3 ),
inference(spm,[status(thm)],[8,15704,theory(equality)]) ).
cnf(15724,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk4_0 = esk2_1(X2)
| esk2_1(X2) = X2
| esk1_1(X1) = X1
| f(g(esk1_1(X3))) = esk1_1(X3)
| esk2_1(esk4_0) = esk4_0
| esk1_1(X3) = X3 ),
inference(rw,[status(thm)],[15710,15528,theory(equality)]) ).
cnf(15764,negated_conjecture,
( f(g(esk1_1(X4))) = esk1_1(X4)
| esk2_1(esk4_0) = esk4_0
| esk2_1(X5) = esk4_0
| esk1_1(X4) = X4
| esk2_1(X5) = X5 ),
inference(ef,[status(thm)],[15724,theory(equality)]) ).
cnf(15815,negated_conjecture,
( f(g(esk1_1(X5))) = esk1_1(X5)
| esk2_1(esk4_0) = esk4_0
| esk2_1(X6) = esk4_0
| esk1_1(X5) = X5
| X6 != esk4_0 ),
inference(ef,[status(thm)],[15764,theory(equality)]) ).
cnf(15849,negated_conjecture,
( f(g(esk1_1(X1))) = esk1_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1 ),
inference(er,[status(thm)],[15815,theory(equality)]) ).
cnf(15852,negated_conjecture,
( esk4_0 = g(esk1_1(X1))
| esk3_0 = X2
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,15849,theory(equality)]) ).
cnf(15877,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| esk3_0 = esk1_1(X2)
| esk1_1(X2) = X2 ),
inference(spm,[status(thm)],[15852,15849,theory(equality)]) ).
cnf(15881,negated_conjecture,
( g(esk1_1(X5)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(X6) = esk3_0
| esk1_1(X5) = X5
| X6 != esk3_0 ),
inference(ef,[status(thm)],[15877,theory(equality)]) ).
cnf(15918,negated_conjecture,
( g(esk1_1(X1)) = esk4_0
| esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0
| esk1_1(X1) = X1 ),
inference(er,[status(thm)],[15881,theory(equality)]) ).
cnf(15926,negated_conjecture,
( f(esk4_0) = esk1_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| esk1_1(esk3_0) = esk3_0 ),
inference(spm,[status(thm)],[15849,15918,theory(equality)]) ).
cnf(15936,negated_conjecture,
( esk3_0 = esk1_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk1_1(X1) = X1
| esk1_1(esk3_0) = esk3_0 ),
inference(rw,[status(thm)],[15926,15527,theory(equality)]) ).
cnf(15939,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| esk1_1(esk3_0) = esk3_0 ),
inference(ef,[status(thm)],[15936,theory(equality)]) ).
cnf(15966,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| esk2_1(esk4_0) = esk4_0
| f(g(esk3_0)) != esk3_0 ),
inference(spm,[status(thm)],[9,15939,theory(equality)]) ).
cnf(15967,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| esk2_1(esk4_0) = esk4_0
| $false ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[15966,15528,theory(equality)]),15527,theory(equality)]) ).
cnf(15968,negated_conjecture,
( g(f(esk2_1(X1))) = esk2_1(X1)
| esk2_1(X1) = X1
| esk2_1(esk4_0) = esk4_0 ),
inference(cn,[status(thm)],[15967,theory(equality)]) ).
cnf(15972,negated_conjecture,
( esk4_0 = esk2_1(X1)
| esk3_0 = X2
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1
| f(g(X2)) != X2 ),
inference(spm,[status(thm)],[15,15968,theory(equality)]) ).
cnf(16249,negated_conjecture,
( esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = esk4_0
| esk2_1(X1) = X1
| esk3_0 = f(esk2_1(X2))
| esk2_1(X2) = X2 ),
inference(spm,[status(thm)],[15972,15968,theory(equality)]) ).
cnf(16257,negated_conjecture,
( f(esk2_1(X5)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X6) = esk4_0
| esk2_1(X5) = X5
| X6 != esk4_0 ),
inference(ef,[status(thm)],[16249,theory(equality)]) ).
cnf(16302,negated_conjecture,
( f(esk2_1(X1)) = esk3_0
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1 ),
inference(er,[status(thm)],[16257,theory(equality)]) ).
cnf(16312,negated_conjecture,
( g(esk3_0) = esk2_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1 ),
inference(spm,[status(thm)],[15968,16302,theory(equality)]) ).
cnf(16322,negated_conjecture,
( esk4_0 = esk2_1(X1)
| esk2_1(esk4_0) = esk4_0
| esk2_1(X1) = X1 ),
inference(rw,[status(thm)],[16312,15528,theory(equality)]) ).
cnf(16406,negated_conjecture,
esk2_1(esk4_0) = esk4_0,
inference(ef,[status(thm)],[16322,theory(equality)]) ).
cnf(16446,negated_conjecture,
( epred1_0
| g(f(esk4_0)) != esk4_0 ),
inference(spm,[status(thm)],[26,16406,theory(equality)]) ).
cnf(16458,negated_conjecture,
( epred1_0
| $false ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[16446,15527,theory(equality)]),15528,theory(equality)]) ).
cnf(16459,negated_conjecture,
epred1_0,
inference(cn,[status(thm)],[16458,theory(equality)]) ).
cnf(16460,negated_conjecture,
$false,
inference(sr,[status(thm)],[16459,15516,theory(equality)]) ).
cnf(16461,negated_conjecture,
$false,
16460,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SYN/SYN551+2.p
% --creating new selector for []
% -running prover on /tmp/tmpvqDG4h/sel_SYN551+2.p_1 with time limit 29
% -prover status Theorem
% Problem SYN551+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SYN/SYN551+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SYN/SYN551+2.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------