%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : COM003+3 : TPTP v5.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art04.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 05:44:13 EST 2010
% Result : Theorem 73.30s
% Output : CNFRefutation 73.30s
% Verified :
% SZS Type : None (MakeTreeStats ran out of CPU time)
% Syntax : Number of formulae : 496
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1] :
( ( program(X1)
& ! [X2] :
( program(X2)
=> ! [X3] : decides(X1,X2,X3) ) )
=> ! [X2,X3] :
( ( ( program(X2)
& halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,good) ) )
& ( ( program(X2)
& ~ halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,bad) ) ) ) ),
file('/tmp/tmpYKn8_K/sel_COM003+3.p_2',p2) ).
fof(2,axiom,
! [X1] :
( ( program(X1)
& ! [X2,X3] :
( ( ( program(X2)
& halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,good) ) )
& ( ( program(X2)
& ~ halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,bad) ) ) ) )
=> ? [X4] :
( program(X4)
& ! [X2] :
( ( ( program(X2)
& halts3(X1,X2,X2)
& outputs(X1,good) )
=> ~ halts2(X4,X2) )
& ( ( program(X2)
& halts3(X1,X2,X2)
& outputs(X1,bad) )
=> ( halts2(X4,X2)
& outputs(X4,bad) ) ) ) ) ),
file('/tmp/tmpYKn8_K/sel_COM003+3.p_2',p3) ).
fof(3,conjecture,
~ ? [X5] :
( algorithm(X5)
& ! [X6] :
( program(X6)
=> ! [X7] : decides(X5,X6,X7) ) ),
file('/tmp/tmpYKn8_K/sel_COM003+3.p_2',prove_this) ).
fof(4,axiom,
( ? [X8] :
( algorithm(X8)
& ! [X2] :
( program(X2)
=> ! [X3] : decides(X8,X2,X3) ) )
=> ? [X1] :
( program(X1)
& ! [X2] :
( program(X2)
=> ! [X3] : decides(X1,X2,X3) ) ) ),
file('/tmp/tmpYKn8_K/sel_COM003+3.p_2',p1) ).
fof(5,negated_conjecture,
~ ~ ? [X5] :
( algorithm(X5)
& ! [X6] :
( program(X6)
=> ! [X7] : decides(X5,X6,X7) ) ),
inference(assume_negation,[status(cth)],[3]) ).
fof(6,plain,
! [X1] :
( ( program(X1)
& ! [X2] :
( program(X2)
=> ! [X3] : decides(X1,X2,X3) ) )
=> ! [X2,X3] :
( ( ( program(X2)
& halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,good) ) )
& ( ( program(X2)
& ~ halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,bad) ) ) ) ),
inference(fof_simplification,[status(thm)],[1,theory(equality)]) ).
fof(7,plain,
! [X1] :
( ( program(X1)
& ! [X2,X3] :
( ( ( program(X2)
& halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,good) ) )
& ( ( program(X2)
& ~ halts2(X2,X3) )
=> ( halts3(X1,X2,X3)
& outputs(X1,bad) ) ) ) )
=> ? [X4] :
( program(X4)
& ! [X2] :
( ( ( program(X2)
& halts3(X1,X2,X2)
& outputs(X1,good) )
=> ~ halts2(X4,X2) )
& ( ( program(X2)
& halts3(X1,X2,X2)
& outputs(X1,bad) )
=> ( halts2(X4,X2)
& outputs(X4,bad) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[2,theory(equality)]) ).
fof(8,plain,
! [X1] :
( ~ program(X1)
| ? [X2] :
( program(X2)
& ? [X3] : ~ decides(X1,X2,X3) )
| ! [X2,X3] :
( ( ~ program(X2)
| ~ halts2(X2,X3)
| ( halts3(X1,X2,X3)
& outputs(X1,good) ) )
& ( ~ program(X2)
| halts2(X2,X3)
| ( halts3(X1,X2,X3)
& outputs(X1,bad) ) ) ) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(9,plain,
! [X4] :
( ~ program(X4)
| ? [X5] :
( program(X5)
& ? [X6] : ~ decides(X4,X5,X6) )
| ! [X7,X8] :
( ( ~ program(X7)
| ~ halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,good) ) )
& ( ~ program(X7)
| halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,bad) ) ) ) ),
inference(variable_rename,[status(thm)],[8]) ).
fof(10,plain,
! [X4] :
( ~ program(X4)
| ( program(esk1_1(X4))
& ~ decides(X4,esk1_1(X4),esk2_1(X4)) )
| ! [X7,X8] :
( ( ~ program(X7)
| ~ halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,good) ) )
& ( ~ program(X7)
| halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,bad) ) ) ) ),
inference(skolemize,[status(esa)],[9]) ).
fof(11,plain,
! [X4,X7,X8] :
( ( ( ~ program(X7)
| ~ halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,good) ) )
& ( ~ program(X7)
| halts2(X7,X8)
| ( halts3(X4,X7,X8)
& outputs(X4,bad) ) ) )
| ~ program(X4)
| ( program(esk1_1(X4))
& ~ decides(X4,esk1_1(X4),esk2_1(X4)) ) ),
inference(shift_quantors,[status(thm)],[10]) ).
fof(12,plain,
! [X4,X7,X8] :
( ( program(esk1_1(X4))
| ~ program(X4)
| halts3(X4,X7,X8)
| ~ program(X7)
| ~ halts2(X7,X8) )
& ( ~ decides(X4,esk1_1(X4),esk2_1(X4))
| ~ program(X4)
| halts3(X4,X7,X8)
| ~ program(X7)
| ~ halts2(X7,X8) )
& ( program(esk1_1(X4))
| ~ program(X4)
| outputs(X4,good)
| ~ program(X7)
| ~ halts2(X7,X8) )
& ( ~ decides(X4,esk1_1(X4),esk2_1(X4))
| ~ program(X4)
| outputs(X4,good)
| ~ program(X7)
| ~ halts2(X7,X8) )
& ( program(esk1_1(X4))
| ~ program(X4)
| halts3(X4,X7,X8)
| ~ program(X7)
| halts2(X7,X8) )
& ( ~ decides(X4,esk1_1(X4),esk2_1(X4))
| ~ program(X4)
| halts3(X4,X7,X8)
| ~ program(X7)
| halts2(X7,X8) )
& ( program(esk1_1(X4))
| ~ program(X4)
| outputs(X4,bad)
| ~ program(X7)
| halts2(X7,X8) )
& ( ~ decides(X4,esk1_1(X4),esk2_1(X4))
| ~ program(X4)
| outputs(X4,bad)
| ~ program(X7)
| halts2(X7,X8) ) ),
inference(distribute,[status(thm)],[11]) ).
cnf(13,plain,
( halts2(X1,X2)
| outputs(X3,bad)
| ~ program(X1)
| ~ program(X3)
| ~ decides(X3,esk1_1(X3),esk2_1(X3)) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(14,plain,
( halts2(X1,X2)
| outputs(X3,bad)
| program(esk1_1(X3))
| ~ program(X1)
| ~ program(X3) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(15,plain,
( halts2(X1,X2)
| halts3(X3,X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ decides(X3,esk1_1(X3),esk2_1(X3)) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(16,plain,
( halts2(X1,X2)
| halts3(X3,X1,X2)
| program(esk1_1(X3))
| ~ program(X1)
| ~ program(X3) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(17,plain,
( outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ decides(X3,esk1_1(X3),esk2_1(X3)) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(18,plain,
( outputs(X3,good)
| program(esk1_1(X3))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(19,plain,
( halts3(X3,X1,X2)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ decides(X3,esk1_1(X3),esk2_1(X3)) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(20,plain,
( halts3(X3,X1,X2)
| program(esk1_1(X3))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3) ),
inference(split_conjunct,[status(thm)],[12]) ).
fof(21,plain,
! [X1] :
( ~ program(X1)
| ? [X2,X3] :
( ( program(X2)
& halts2(X2,X3)
& ( ~ halts3(X1,X2,X3)
| ~ outputs(X1,good) ) )
| ( program(X2)
& ~ halts2(X2,X3)
& ( ~ halts3(X1,X2,X3)
| ~ outputs(X1,bad) ) ) )
| ? [X4] :
( program(X4)
& ! [X2] :
( ( ~ program(X2)
| ~ halts3(X1,X2,X2)
| ~ outputs(X1,good)
| ~ halts2(X4,X2) )
& ( ~ program(X2)
| ~ halts3(X1,X2,X2)
| ~ outputs(X1,bad)
| ( halts2(X4,X2)
& outputs(X4,bad) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(22,plain,
! [X5] :
( ~ program(X5)
| ? [X6,X7] :
( ( program(X6)
& halts2(X6,X7)
& ( ~ halts3(X5,X6,X7)
| ~ outputs(X5,good) ) )
| ( program(X6)
& ~ halts2(X6,X7)
& ( ~ halts3(X5,X6,X7)
| ~ outputs(X5,bad) ) ) )
| ? [X8] :
( program(X8)
& ! [X9] :
( ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(X8,X9) )
& ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad)
| ( halts2(X8,X9)
& outputs(X8,bad) ) ) ) ) ),
inference(variable_rename,[status(thm)],[21]) ).
fof(23,plain,
! [X5] :
( ~ program(X5)
| ( program(esk3_1(X5))
& halts2(esk3_1(X5),esk4_1(X5))
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good) ) )
| ( program(esk3_1(X5))
& ~ halts2(esk3_1(X5),esk4_1(X5))
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad) ) )
| ( program(esk5_1(X5))
& ! [X9] :
( ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad)
| ( halts2(esk5_1(X5),X9)
& outputs(esk5_1(X5),bad) ) ) ) ) ),
inference(skolemize,[status(esa)],[22]) ).
fof(24,plain,
! [X5,X9] :
( ( ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad)
| ( halts2(esk5_1(X5),X9)
& outputs(esk5_1(X5),bad) ) )
& program(esk5_1(X5)) )
| ~ program(X5)
| ( program(esk3_1(X5))
& halts2(esk3_1(X5),esk4_1(X5))
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good) ) )
| ( program(esk3_1(X5))
& ~ halts2(esk3_1(X5),esk4_1(X5))
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad) ) ) ),
inference(shift_quantors,[status(thm)],[23]) ).
fof(25,plain,
! [X5,X9] :
( ( program(esk3_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| program(esk3_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( program(esk3_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( program(esk3_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,good)
| ~ halts2(esk5_1(X5),X9) )
& ( program(esk3_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| program(esk3_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| halts2(esk5_1(X5),X9)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| program(esk3_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| outputs(esk5_1(X5),bad)
| ~ program(X9)
| ~ halts3(X5,X9,X9)
| ~ outputs(X5,bad) )
& ( program(esk3_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| program(esk3_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| program(esk3_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( program(esk3_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| halts2(esk3_1(X5),esk4_1(X5))
| ~ program(X5)
| program(esk5_1(X5)) )
& ( program(esk3_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts2(esk3_1(X5),esk4_1(X5))
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| program(esk5_1(X5)) )
& ( ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,bad)
| ~ halts3(X5,esk3_1(X5),esk4_1(X5))
| ~ outputs(X5,good)
| ~ program(X5)
| program(esk5_1(X5)) ) ),
inference(distribute,[status(thm)],[24]) ).
cnf(26,plain,
( program(esk5_1(X1))
| ~ program(X1)
| ~ outputs(X1,good)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(27,plain,
( program(esk5_1(X1))
| ~ program(X1)
| ~ outputs(X1,good)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ halts2(esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(29,plain,
( program(esk5_1(X1))
| halts2(esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(34,plain,
( program(esk5_1(X1))
| program(esk3_1(X1))
| program(esk3_1(X1))
| ~ program(X1) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(44,plain,
( halts2(esk5_1(X1),X2)
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ outputs(X1,good)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(47,plain,
( halts2(esk5_1(X1),X2)
| halts2(esk3_1(X1),esk4_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(52,plain,
( halts2(esk5_1(X1),X2)
| program(esk3_1(X1))
| program(esk3_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(53,plain,
( ~ halts2(esk5_1(X1),X2)
| ~ outputs(X1,good)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ outputs(X1,good)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(54,plain,
( ~ halts2(esk5_1(X1),X2)
| ~ outputs(X1,good)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ outputs(X1,good)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ halts2(esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(59,plain,
( program(esk3_1(X1))
| ~ halts2(esk5_1(X1),X2)
| ~ outputs(X1,good)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1)) ),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(61,plain,
( program(esk3_1(X1))
| program(esk3_1(X1))
| ~ halts2(esk5_1(X1),X2)
| ~ outputs(X1,good)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1) ),
inference(split_conjunct,[status(thm)],[25]) ).
fof(62,negated_conjecture,
? [X5] :
( algorithm(X5)
& ! [X6] :
( ~ program(X6)
| ! [X7] : decides(X5,X6,X7) ) ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(63,negated_conjecture,
? [X8] :
( algorithm(X8)
& ! [X9] :
( ~ program(X9)
| ! [X10] : decides(X8,X9,X10) ) ),
inference(variable_rename,[status(thm)],[62]) ).
fof(64,negated_conjecture,
( algorithm(esk6_0)
& ! [X9] :
( ~ program(X9)
| ! [X10] : decides(esk6_0,X9,X10) ) ),
inference(skolemize,[status(esa)],[63]) ).
fof(65,negated_conjecture,
! [X9,X10] :
( ( decides(esk6_0,X9,X10)
| ~ program(X9) )
& algorithm(esk6_0) ),
inference(shift_quantors,[status(thm)],[64]) ).
cnf(66,negated_conjecture,
algorithm(esk6_0),
inference(split_conjunct,[status(thm)],[65]) ).
cnf(67,negated_conjecture,
( decides(esk6_0,X1,X2)
| ~ program(X1) ),
inference(split_conjunct,[status(thm)],[65]) ).
fof(68,plain,
( ! [X8] :
( ~ algorithm(X8)
| ? [X2] :
( program(X2)
& ? [X3] : ~ decides(X8,X2,X3) ) )
| ? [X1] :
( program(X1)
& ! [X2] :
( ~ program(X2)
| ! [X3] : decides(X1,X2,X3) ) ) ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(69,plain,
( ! [X9] :
( ~ algorithm(X9)
| ? [X10] :
( program(X10)
& ? [X11] : ~ decides(X9,X10,X11) ) )
| ? [X12] :
( program(X12)
& ! [X13] :
( ~ program(X13)
| ! [X14] : decides(X12,X13,X14) ) ) ),
inference(variable_rename,[status(thm)],[68]) ).
fof(70,plain,
( ! [X9] :
( ~ algorithm(X9)
| ( program(esk7_1(X9))
& ~ decides(X9,esk7_1(X9),esk8_1(X9)) ) )
| ( program(esk9_0)
& ! [X13] :
( ~ program(X13)
| ! [X14] : decides(esk9_0,X13,X14) ) ) ),
inference(skolemize,[status(esa)],[69]) ).
fof(71,plain,
! [X9,X13,X14] :
( ( ( decides(esk9_0,X13,X14)
| ~ program(X13) )
& program(esk9_0) )
| ~ algorithm(X9)
| ( program(esk7_1(X9))
& ~ decides(X9,esk7_1(X9),esk8_1(X9)) ) ),
inference(shift_quantors,[status(thm)],[70]) ).
fof(72,plain,
! [X9,X13,X14] :
( ( program(esk7_1(X9))
| ~ algorithm(X9)
| decides(esk9_0,X13,X14)
| ~ program(X13) )
& ( ~ decides(X9,esk7_1(X9),esk8_1(X9))
| ~ algorithm(X9)
| decides(esk9_0,X13,X14)
| ~ program(X13) )
& ( program(esk7_1(X9))
| ~ algorithm(X9)
| program(esk9_0) )
& ( ~ decides(X9,esk7_1(X9),esk8_1(X9))
| ~ algorithm(X9)
| program(esk9_0) ) ),
inference(distribute,[status(thm)],[71]) ).
cnf(73,plain,
( program(esk9_0)
| ~ algorithm(X1)
| ~ decides(X1,esk7_1(X1),esk8_1(X1)) ),
inference(split_conjunct,[status(thm)],[72]) ).
cnf(74,plain,
( program(esk9_0)
| program(esk7_1(X1))
| ~ algorithm(X1) ),
inference(split_conjunct,[status(thm)],[72]) ).
cnf(75,plain,
( decides(esk9_0,X1,X2)
| ~ program(X1)
| ~ algorithm(X3)
| ~ decides(X3,esk7_1(X3),esk8_1(X3)) ),
inference(split_conjunct,[status(thm)],[72]) ).
cnf(76,plain,
( decides(esk9_0,X1,X2)
| program(esk7_1(X3))
| ~ program(X1)
| ~ algorithm(X3) ),
inference(split_conjunct,[status(thm)],[72]) ).
cnf(77,negated_conjecture,
( program(esk9_0)
| ~ algorithm(esk6_0)
| ~ program(esk7_1(esk6_0)) ),
inference(spm,[status(thm)],[73,67,theory(equality)]) ).
cnf(78,negated_conjecture,
( program(esk9_0)
| $false
| ~ program(esk7_1(esk6_0)) ),
inference(rw,[status(thm)],[77,66,theory(equality)]) ).
cnf(79,negated_conjecture,
( program(esk9_0)
| ~ program(esk7_1(esk6_0)) ),
inference(cn,[status(thm)],[78,theory(equality)]) ).
cnf(83,plain,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(X4,bad)
| program(esk1_1(X4))
| ~ program(X1)
| ~ program(X2)
| ~ program(X4) ),
inference(spm,[status(thm)],[18,14,theory(equality)]) ).
cnf(85,negated_conjecture,
( decides(esk9_0,X1,X2)
| ~ algorithm(esk6_0)
| ~ program(X1)
| ~ program(esk7_1(esk6_0)) ),
inference(spm,[status(thm)],[75,67,theory(equality)]) ).
cnf(87,negated_conjecture,
( decides(esk9_0,X1,X2)
| $false
| ~ program(X1)
| ~ program(esk7_1(esk6_0)) ),
inference(rw,[status(thm)],[85,66,theory(equality)]) ).
cnf(88,negated_conjecture,
( decides(esk9_0,X1,X2)
| ~ program(X1)
| ~ program(esk7_1(esk6_0)) ),
inference(cn,[status(thm)],[87,theory(equality)]) ).
cnf(89,plain,
( halts3(X3,X1,X2)
| program(esk1_1(X3))
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[20,16]) ).
cnf(100,plain,
( halts3(X3,X1,X2)
| ~ decides(X3,esk1_1(X3),esk2_1(X3))
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[19,15]) ).
cnf(112,plain,
( ~ outputs(X1,good)
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1) ),
inference(csr,[status(thm)],[53,44]) ).
cnf(118,plain,
( program(esk3_1(X1))
| ~ outputs(X1,good)
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ halts2(esk5_1(X1),X2)
| ~ program(X2)
| ~ program(X1) ),
inference(csr,[status(thm)],[59,61]) ).
cnf(119,plain,
( program(esk3_1(X1))
| ~ outputs(X1,good)
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1) ),
inference(csr,[status(thm)],[118,52]) ).
cnf(126,negated_conjecture,
( program(esk9_0)
| ~ algorithm(esk6_0) ),
inference(spm,[status(thm)],[79,74,theory(equality)]) ).
cnf(128,negated_conjecture,
( program(esk9_0)
| $false ),
inference(rw,[status(thm)],[126,66,theory(equality)]) ).
cnf(129,negated_conjecture,
program(esk9_0),
inference(cn,[status(thm)],[128,theory(equality)]) ).
cnf(135,negated_conjecture,
( decides(esk9_0,X1,X2)
| decides(esk9_0,X3,X4)
| ~ program(X1)
| ~ algorithm(esk6_0)
| ~ program(X3) ),
inference(spm,[status(thm)],[88,76,theory(equality)]) ).
cnf(136,negated_conjecture,
( decides(esk9_0,X1,X2)
| decides(esk9_0,X3,X4)
| ~ program(X1)
| $false
| ~ program(X3) ),
inference(rw,[status(thm)],[135,66,theory(equality)]) ).
cnf(137,negated_conjecture,
( decides(esk9_0,X1,X2)
| decides(esk9_0,X3,X4)
| ~ program(X1)
| ~ program(X3) ),
inference(cn,[status(thm)],[136,theory(equality)]) ).
cnf(141,negated_conjecture,
( decides(esk9_0,X5,X6)
| ~ program(X5) ),
inference(ef,[status(thm)],[137,theory(equality)]) ).
cnf(163,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(spm,[status(thm)],[13,141,theory(equality)]) ).
cnf(164,negated_conjecture,
( outputs(esk9_0,good)
| ~ halts2(X1,X2)
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(spm,[status(thm)],[17,141,theory(equality)]) ).
cnf(165,negated_conjecture,
( halts3(esk9_0,X1,X2)
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(spm,[status(thm)],[100,141,theory(equality)]) ).
cnf(166,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| $false
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(rw,[status(thm)],[163,129,theory(equality)]) ).
cnf(167,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(cn,[status(thm)],[166,theory(equality)]) ).
cnf(168,negated_conjecture,
( outputs(esk9_0,good)
| ~ halts2(X1,X2)
| $false
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(rw,[status(thm)],[164,129,theory(equality)]) ).
cnf(169,negated_conjecture,
( outputs(esk9_0,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(cn,[status(thm)],[168,theory(equality)]) ).
cnf(170,negated_conjecture,
( halts3(esk9_0,X1,X2)
| $false
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(rw,[status(thm)],[165,129,theory(equality)]) ).
cnf(171,negated_conjecture,
( halts3(esk9_0,X1,X2)
| ~ program(X1)
| ~ program(esk1_1(esk9_0)) ),
inference(cn,[status(thm)],[170,theory(equality)]) ).
cnf(172,plain,
( outputs(X4,bad)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X4)
| ~ program(X5) ),
inference(ef,[status(thm)],[83,theory(equality)]) ).
cnf(182,negated_conjecture,
( halts3(esk9_0,X1,X2)
| halts3(esk9_0,X3,X4)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3) ),
inference(spm,[status(thm)],[171,89,theory(equality)]) ).
cnf(187,negated_conjecture,
( halts3(esk9_0,X1,X2)
| halts3(esk9_0,X3,X4)
| ~ program(X1)
| $false
| ~ program(X3) ),
inference(rw,[status(thm)],[182,129,theory(equality)]) ).
cnf(188,negated_conjecture,
( halts3(esk9_0,X1,X2)
| halts3(esk9_0,X3,X4)
| ~ program(X1)
| ~ program(X3) ),
inference(cn,[status(thm)],[187,theory(equality)]) ).
cnf(204,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| halts2(X3,X4)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3) ),
inference(spm,[status(thm)],[167,14,theory(equality)]) ).
cnf(208,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| outputs(esk9_0,good)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3) ),
inference(spm,[status(thm)],[167,172,theory(equality)]) ).
cnf(209,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| halts2(X3,X4)
| ~ program(X1)
| $false
| ~ program(X3) ),
inference(rw,[status(thm)],[204,129,theory(equality)]) ).
cnf(210,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| halts2(X3,X4)
| ~ program(X1)
| ~ program(X3) ),
inference(cn,[status(thm)],[209,theory(equality)]) ).
cnf(217,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| outputs(esk9_0,good)
| ~ program(X1)
| $false
| ~ program(X3) ),
inference(rw,[status(thm)],[208,129,theory(equality)]) ).
cnf(218,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X1,X2)
| outputs(esk9_0,good)
| ~ program(X1)
| ~ program(X3) ),
inference(cn,[status(thm)],[217,theory(equality)]) ).
cnf(223,negated_conjecture,
( outputs(esk9_0,good)
| outputs(esk9_0,bad)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3) ),
inference(spm,[status(thm)],[169,172,theory(equality)]) ).
cnf(232,negated_conjecture,
( outputs(esk9_0,good)
| outputs(esk9_0,bad)
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X3) ),
inference(rw,[status(thm)],[223,129,theory(equality)]) ).
cnf(233,negated_conjecture,
( outputs(esk9_0,good)
| outputs(esk9_0,bad)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3) ),
inference(cn,[status(thm)],[232,theory(equality)]) ).
cnf(241,negated_conjecture,
( outputs(esk9_0,good)
| outputs(esk9_0,bad)
| ~ program(X1)
| ~ program(X3) ),
inference(csr,[status(thm)],[233,218]) ).
cnf(249,negated_conjecture,
( program(esk3_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3) ),
inference(spm,[status(thm)],[61,241,theory(equality)]) ).
cnf(250,negated_conjecture,
( program(esk5_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X2) ),
inference(spm,[status(thm)],[27,241,theory(equality)]) ).
cnf(253,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3) ),
inference(spm,[status(thm)],[54,241,theory(equality)]) ).
cnf(262,negated_conjecture,
( program(esk3_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3) ),
inference(rw,[status(thm)],[249,129,theory(equality)]) ).
cnf(263,negated_conjecture,
( program(esk3_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(cn,[status(thm)],[262,theory(equality)]) ).
cnf(264,negated_conjecture,
( program(esk5_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| $false
| ~ program(X1)
| ~ program(X2) ),
inference(rw,[status(thm)],[250,129,theory(equality)]) ).
cnf(265,negated_conjecture,
( program(esk5_1(esk9_0))
| outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2) ),
inference(cn,[status(thm)],[264,theory(equality)]) ).
cnf(270,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3) ),
inference(rw,[status(thm)],[253,129,theory(equality)]) ).
cnf(271,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(cn,[status(thm)],[270,theory(equality)]) ).
cnf(274,negated_conjecture,
( halts3(esk9_0,X5,X6)
| ~ program(X5) ),
inference(ef,[status(thm)],[188,theory(equality)]) ).
cnf(278,negated_conjecture,
( outputs(esk9_0,bad)
| halts2(X5,X6)
| ~ program(X5) ),
inference(ef,[status(thm)],[210,theory(equality)]) ).
cnf(284,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(esk9_0,bad)
| ~ program(X1)
| ~ program(X2) ),
inference(spm,[status(thm)],[18,278,theory(equality)]) ).
cnf(285,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[271,278,theory(equality)]) ).
cnf(310,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(csr,[status(thm)],[285,274]) ).
cnf(311,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(csr,[status(thm)],[310,274]) ).
cnf(413,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(csr,[status(thm)],[263,274]) ).
cnf(414,negated_conjecture,
( outputs(esk9_0,bad)
| ~ halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(csr,[status(thm)],[413,311]) ).
cnf(416,negated_conjecture,
( outputs(esk9_0,bad)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(esk5_1(esk9_0)) ),
inference(spm,[status(thm)],[414,278,theory(equality)]) ).
cnf(422,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[416,34,theory(equality)]) ).
cnf(423,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| $false ),
inference(rw,[status(thm)],[422,129,theory(equality)]) ).
cnf(424,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(cn,[status(thm)],[423,theory(equality)]) ).
cnf(435,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(spm,[status(thm)],[52,424,theory(equality)]) ).
cnf(456,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(rw,[status(thm)],[435,129,theory(equality)]) ).
cnf(457,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(cn,[status(thm)],[456,theory(equality)]) ).
cnf(543,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[457,274]) ).
cnf(550,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(spm,[status(thm)],[18,543,theory(equality)]) ).
cnf(576,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[550,34,theory(equality)]) ).
cnf(577,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| $false ),
inference(rw,[status(thm)],[576,129,theory(equality)]) ).
cnf(578,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(cn,[status(thm)],[577,theory(equality)]) ).
cnf(619,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| outputs(X1,good)
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(spm,[status(thm)],[424,578,theory(equality)]) ).
cnf(671,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[265,278,theory(equality)]) ).
cnf(683,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2) ),
inference(csr,[status(thm)],[671,274]) ).
cnf(684,negated_conjecture,
( outputs(esk9_0,bad)
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2) ),
inference(csr,[status(thm)],[683,416]) ).
cnf(815,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[619,424]) ).
cnf(816,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[815,424]) ).
cnf(817,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4) ),
inference(csr,[status(thm)],[816,424]) ).
cnf(818,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[817,424]) ).
cnf(819,negated_conjecture,
( outputs(esk9_0,bad)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[818,424]) ).
cnf(820,negated_conjecture,
( outputs(esk9_0,bad)
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[819,684]) ).
cnf(832,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(spm,[status(thm)],[29,820,theory(equality)]) ).
cnf(834,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(spm,[status(thm)],[47,820,theory(equality)]) ).
cnf(835,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,bad)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1) ),
inference(spm,[status(thm)],[820,83,theory(equality)]) ).
cnf(857,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| $false
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(rw,[status(thm)],[832,129,theory(equality)]) ).
cnf(858,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(cn,[status(thm)],[857,theory(equality)]) ).
cnf(861,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(rw,[status(thm)],[834,129,theory(equality)]) ).
cnf(862,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(cn,[status(thm)],[861,theory(equality)]) ).
cnf(921,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[858,274,theory(equality)]) ).
cnf(929,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,bad)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[835,820]) ).
cnf(930,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,bad)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[929,820]) ).
cnf(931,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,bad)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X4)
| ~ program(X2) ),
inference(csr,[status(thm)],[930,284]) ).
cnf(932,negated_conjecture,
( outputs(esk9_0,bad)
| outputs(X1,bad)
| outputs(X4,good)
| ~ program(X2)
| ~ program(X4) ),
inference(csr,[status(thm)],[931,820]) ).
cnf(933,negated_conjecture,
( outputs(X4,good)
| outputs(esk9_0,bad)
| ~ program(X5)
| ~ program(X4) ),
inference(ef,[status(thm)],[932,theory(equality)]) ).
cnf(975,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| outputs(X2,good)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3)
| ~ program(X2) ),
inference(spm,[status(thm)],[52,933,theory(equality)]) ).
cnf(981,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| outputs(X2,good)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3)
| ~ program(X2) ),
inference(spm,[status(thm)],[47,933,theory(equality)]) ).
cnf(991,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| outputs(X2,good)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X3)
| ~ program(X2) ),
inference(rw,[status(thm)],[975,129,theory(equality)]) ).
cnf(992,negated_conjecture,
( halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| outputs(X2,good)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X3)
| ~ program(X2) ),
inference(cn,[status(thm)],[991,theory(equality)]) ).
cnf(997,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| outputs(X2,good)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X3)
| ~ program(X2) ),
inference(rw,[status(thm)],[981,129,theory(equality)]) ).
cnf(998,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| outputs(X2,good)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X3)
| ~ program(X2) ),
inference(cn,[status(thm)],[997,theory(equality)]) ).
cnf(1118,negated_conjecture,
( outputs(X2,good)
| halts2(esk5_1(esk9_0),X1)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X2) ),
inference(csr,[status(thm)],[992,274]) ).
cnf(2169,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[862,274]) ).
cnf(2171,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[2169,274,theory(equality)]) ).
cnf(2179,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[2171,543]) ).
cnf(2186,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| halts2(esk5_1(esk9_0),X2)
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(spm,[status(thm)],[18,2179,theory(equality)]) ).
cnf(2215,negated_conjecture,
( outputs(X1,good)
| halts2(esk5_1(esk9_0),X2)
| program(esk1_1(X1))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1) ),
inference(csr,[status(thm)],[2186,543]) ).
cnf(2222,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(X3,good)
| program(esk1_1(X3))
| ~ program(X1)
| ~ program(esk5_1(esk9_0))
| ~ program(X3)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(spm,[status(thm)],[18,2215,theory(equality)]) ).
cnf(3518,negated_conjecture,
( outputs(X2,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X2) ),
inference(csr,[status(thm)],[998,274]) ).
cnf(3520,negated_conjecture,
( outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X2)
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[3518,274,theory(equality)]) ).
cnf(3530,negated_conjecture,
( outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| halts2(esk5_1(esk9_0),X2)
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[3520,1118]) ).
cnf(3533,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(X2,good)
| halts2(esk5_1(esk9_0),X3)
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X3)
| ~ program(X4)
| ~ program(X2) ),
inference(spm,[status(thm)],[18,3530,theory(equality)]) ).
cnf(3562,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk1_1(X1))
| ~ program(X3)
| ~ program(X4)
| ~ program(X2)
| ~ program(X1) ),
inference(csr,[status(thm)],[3533,543]) ).
cnf(3594,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk1_1(X2))
| outputs(X4,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[3562,578,theory(equality)]) ).
cnf(6588,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk3_1(esk9_0))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[3594,543]) ).
cnf(6589,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk3_1(esk9_0))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[6588,543]) ).
cnf(6590,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk3_1(esk9_0))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[6589,543]) ).
cnf(6591,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk3_1(esk9_0))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4) ),
inference(csr,[status(thm)],[6590,543]) ).
cnf(6592,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk3_1(esk9_0))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[6591,1118]) ).
cnf(6593,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X4,good)
| halts2(esk5_1(esk9_0),X3)
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[6592,3562]) ).
cnf(6594,negated_conjecture,
( outputs(X6,good)
| outputs(X5,good)
| halts2(esk5_1(esk9_0),X7)
| program(esk1_1(X6))
| ~ program(X6)
| ~ program(X7)
| ~ program(X5) ),
inference(ef,[status(thm)],[6593,theory(equality)]) ).
cnf(6732,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(X3,good)
| outputs(X4,good)
| program(esk1_1(X4))
| ~ program(X1)
| ~ program(esk5_1(esk9_0))
| ~ program(X4)
| ~ program(X2)
| ~ program(X3) ),
inference(spm,[status(thm)],[18,6594,theory(equality)]) ).
cnf(6861,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| program(esk1_1(X3))
| program(esk3_1(esk9_0))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[6732,34,theory(equality)]) ).
cnf(6862,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| program(esk1_1(X3))
| program(esk3_1(esk9_0))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| $false ),
inference(rw,[status(thm)],[6861,129,theory(equality)]) ).
cnf(6863,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| program(esk1_1(X3))
| program(esk3_1(esk9_0))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2) ),
inference(cn,[status(thm)],[6862,theory(equality)]) ).
cnf(6864,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2) ),
inference(csr,[status(thm)],[6863,578]) ).
cnf(6865,negated_conjecture,
( outputs(X5,good)
| outputs(X6,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X6))
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(ef,[status(thm)],[6864,theory(equality)]) ).
cnf(7022,negated_conjecture,
( program(esk3_1(X1))
| outputs(X3,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X3))
| ~ halts3(X1,X2,X2)
| ~ halts2(esk5_1(X1),X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4) ),
inference(spm,[status(thm)],[61,6865,theory(equality)]) ).
cnf(7032,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk3_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(esk9_0)
| ~ program(X4) ),
inference(spm,[status(thm)],[169,6865,theory(equality)]) ).
cnf(7158,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk3_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| $false
| ~ program(X4) ),
inference(rw,[status(thm)],[7032,129,theory(equality)]) ).
cnf(7159,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk3_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4) ),
inference(cn,[status(thm)],[7158,theory(equality)]) ).
cnf(7162,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(spm,[status(thm)],[7159,543,theory(equality)]) ).
cnf(7210,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[7162,34,theory(equality)]) ).
cnf(7211,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| $false ),
inference(rw,[status(thm)],[7210,129,theory(equality)]) ).
cnf(7212,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(cn,[status(thm)],[7211,theory(equality)]) ).
cnf(7213,negated_conjecture,
( outputs(esk9_0,good)
| program(esk3_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(ef,[status(thm)],[7212,theory(equality)]) ).
cnf(7302,negated_conjecture,
( outputs(esk9_0,good)
| program(esk3_1(esk9_0))
| $false
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(rw,[status(thm)],[7213,129,theory(equality)]) ).
cnf(7303,negated_conjecture,
( outputs(esk9_0,good)
| program(esk3_1(esk9_0))
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(cn,[status(thm)],[7302,theory(equality)]) ).
cnf(7337,negated_conjecture,
( program(esk3_1(esk9_0))
| ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(spm,[status(thm)],[119,7303,theory(equality)]) ).
cnf(7407,negated_conjecture,
( program(esk3_1(esk9_0))
| ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(rw,[status(thm)],[7337,129,theory(equality)]) ).
cnf(7408,negated_conjecture,
( program(esk3_1(esk9_0))
| ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(cn,[status(thm)],[7407,theory(equality)]) ).
cnf(7432,negated_conjecture,
( program(esk3_1(esk9_0))
| ~ outputs(esk9_0,bad)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[7408,274]) ).
cnf(7433,negated_conjecture,
( program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[7432,820]) ).
cnf(7482,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(spm,[status(thm)],[921,7433,theory(equality)]) ).
cnf(8000,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| outputs(X1,good)
| outputs(X10,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X1)
| ~ program(X11) ),
inference(spm,[status(thm)],[7482,6865,theory(equality)]) ).
cnf(8263,negated_conjecture,
( outputs(X3,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X3))
| ~ halts3(X1,X2,X2)
| ~ halts2(esk5_1(X1),X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[7022,578]) ).
cnf(8266,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ halts3(esk9_0,X2,X2)
| ~ program(X2)
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(spm,[status(thm)],[8263,543,theory(equality)]) ).
cnf(8273,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ halts3(esk9_0,X2,X2)
| ~ program(X2)
| $false
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(rw,[status(thm)],[8266,129,theory(equality)]) ).
cnf(8274,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ halts3(esk9_0,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(cn,[status(thm)],[8273,theory(equality)]) ).
cnf(8285,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ halts3(esk9_0,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[8274,578]) ).
cnf(8286,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[8285,274]) ).
cnf(8287,negated_conjecture,
( outputs(X1,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[8286,7433]) ).
cnf(15753,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X1) ),
inference(csr,[status(thm)],[8000,7433]) ).
cnf(15754,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[15753,7433]) ).
cnf(15755,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[15754,7433]) ).
cnf(15756,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[15755,7433]) ).
cnf(15757,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[15756,7433]) ).
cnf(15758,negated_conjecture,
( outputs(X1,good)
| outputs(X10,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[15757,921]) ).
cnf(15759,negated_conjecture,
( outputs(X9,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15) ),
inference(ef,[status(thm)],[15758,theory(equality)]) ).
cnf(15912,negated_conjecture,
( program(esk3_1(X1))
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ halts3(X1,X2,X2)
| ~ halts2(esk5_1(X1),X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[61,15759,theory(equality)]) ).
cnf(17151,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ halts3(X1,X2,X2)
| ~ halts2(esk5_1(X1),X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[15912,7482]) ).
cnf(17154,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(spm,[status(thm)],[17151,543,theory(equality)]) ).
cnf(17163,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(rw,[status(thm)],[17154,129,theory(equality)]) ).
cnf(17164,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(cn,[status(thm)],[17163,theory(equality)]) ).
cnf(17194,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[17164,7433]) ).
cnf(17195,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[17194,7433]) ).
cnf(17196,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[17195,7433]) ).
cnf(17197,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[17196,7433]) ).
cnf(17198,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[17197,7433]) ).
cnf(17199,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[17198,921]) ).
cnf(17212,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(spm,[status(thm)],[18,17199,theory(equality)]) ).
cnf(17267,negated_conjecture,
( halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| outputs(X1,good)
| outputs(X7,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1)
| ~ program(X8) ),
inference(spm,[status(thm)],[17199,6865,theory(equality)]) ).
cnf(17316,negated_conjecture,
( outputs(X1,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1) ),
inference(csr,[status(thm)],[17212,7433]) ).
cnf(17355,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[169,17316,theory(equality)]) ).
cnf(17537,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(rw,[status(thm)],[17355,129,theory(equality)]) ).
cnf(17538,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(cn,[status(thm)],[17537,theory(equality)]) ).
cnf(19237,negated_conjecture,
( outputs(X1,good)
| outputs(X7,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1) ),
inference(csr,[status(thm)],[17267,7433]) ).
cnf(19238,negated_conjecture,
( outputs(X1,good)
| outputs(X7,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[19237,7433]) ).
cnf(19239,negated_conjecture,
( outputs(X1,good)
| outputs(X7,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X7)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[19238,8287]) ).
cnf(19240,negated_conjecture,
( outputs(X1,good)
| outputs(X7,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X7) ),
inference(csr,[status(thm)],[19239,17199]) ).
cnf(19241,negated_conjecture,
( outputs(X7,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| program(esk5_1(esk9_0))
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X7) ),
inference(ef,[status(thm)],[19240,theory(equality)]) ).
cnf(19350,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(X2,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X2) ),
inference(spm,[status(thm)],[18,19241,theory(equality)]) ).
cnf(19412,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| outputs(X7,good)
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X7) ),
inference(spm,[status(thm)],[17538,19241,theory(equality)]) ).
cnf(19431,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X2)
| ~ program(X1) ),
inference(csr,[status(thm)],[19350,7433]) ).
cnf(19464,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X3) ),
inference(spm,[status(thm)],[169,19431,theory(equality)]) ).
cnf(19628,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X3) ),
inference(rw,[status(thm)],[19464,129,theory(equality)]) ).
cnf(19629,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X3) ),
inference(cn,[status(thm)],[19628,theory(equality)]) ).
cnf(19644,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(spm,[status(thm)],[19629,17199,theory(equality)]) ).
cnf(19647,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| outputs(X6,good)
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X6) ),
inference(spm,[status(thm)],[19629,19241,theory(equality)]) ).
cnf(19789,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X7,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X7) ),
inference(csr,[status(thm)],[19412,7433]) ).
cnf(20013,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[19644,19789]) ).
cnf(20014,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[20013,7433]) ).
cnf(21059,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X6,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[19647,20014]) ).
cnf(21060,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X6,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X1)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[21059,7433]) ).
cnf(21061,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15)
| ~ program(X11)
| ~ program(X16)
| ~ program(X17)
| ~ program(X18)
| ~ program(X19) ),
inference(ef,[status(thm)],[21060,theory(equality)]) ).
cnf(21299,negated_conjecture,
( program(esk5_1(X1))
| outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(spm,[status(thm)],[26,21061,theory(equality)]) ).
cnf(21359,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| program(esk1_1(X2))
| outputs(esk9_0,good)
| outputs(X7,good)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X7)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15) ),
inference(spm,[status(thm)],[2222,21061,theory(equality)]) ).
cnf(21375,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| program(esk1_1(X3))
| outputs(esk9_0,good)
| outputs(X5,good)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X5)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13) ),
inference(spm,[status(thm)],[6732,21061,theory(equality)]) ).
cnf(21725,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(spm,[status(thm)],[21299,820,theory(equality)]) ).
cnf(21733,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| $false
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(rw,[status(thm)],[21725,129,theory(equality)]) ).
cnf(21734,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(cn,[status(thm)],[21733,theory(equality)]) ).
cnf(21738,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[21734,274,theory(equality)]) ).
cnf(21741,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(csr,[status(thm)],[21738,7433]) ).
cnf(27980,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X16,good)
| outputs(X17,good)
| program(esk1_1(X17))
| ~ program(X17)
| ~ program(X18)
| ~ program(X19)
| ~ program(X20)
| ~ program(X21)
| ~ program(X22)
| ~ program(X23)
| ~ program(X24)
| ~ program(X25)
| ~ program(X16)
| ~ program(X26)
| ~ program(X28)
| ~ program(X27)
| ~ program(X29) ),
inference(ef,[status(thm)],[21359,theory(equality)]) ).
cnf(30449,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| outputs(X5,good)
| program(esk1_1(X1))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X5)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13) ),
inference(csr,[status(thm)],[21375,27980]) ).
cnf(30450,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X14,good)
| outputs(X15,good)
| outputs(X16,good)
| program(esk1_1(X16))
| ~ program(X14)
| ~ program(X16)
| ~ program(X17)
| ~ program(X15)
| ~ program(X18)
| ~ program(X19)
| ~ program(X20)
| ~ program(X21)
| ~ program(X22)
| ~ program(X23)
| ~ program(X24)
| ~ program(X25) ),
inference(ef,[status(thm)],[30449,theory(equality)]) ).
cnf(30795,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X13,good)
| outputs(X14,good)
| program(esk1_1(X13))
| ~ program(X14)
| ~ program(X13)
| ~ program(X15)
| ~ program(X16)
| ~ program(X17)
| ~ program(X18)
| ~ program(X19)
| ~ program(X20)
| ~ program(X21)
| ~ program(X22)
| ~ program(X23) ),
inference(ef,[status(thm)],[30450,theory(equality)]) ).
cnf(31192,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(esk9_0)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(spm,[status(thm)],[169,30795,theory(equality)]) ).
cnf(31415,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| $false
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(rw,[status(thm)],[31192,129,theory(equality)]) ).
cnf(31416,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(cn,[status(thm)],[31415,theory(equality)]) ).
cnf(31431,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15)
| ~ program(X16) ),
inference(spm,[status(thm)],[31416,17199,theory(equality)]) ).
cnf(32166,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15) ),
inference(csr,[status(thm)],[31431,21741]) ).
cnf(32167,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14) ),
inference(csr,[status(thm)],[32166,21741]) ).
cnf(32168,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13) ),
inference(csr,[status(thm)],[32167,21741]) ).
cnf(32169,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(csr,[status(thm)],[32168,21741]) ).
cnf(32170,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(csr,[status(thm)],[32169,21741]) ).
cnf(32171,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[32170,21741]) ).
cnf(32172,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[32171,21061]) ).
cnf(32173,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[32172,21061]) ).
cnf(32174,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[32173,7433]) ).
cnf(32196,negated_conjecture,
( program(esk5_1(X1))
| outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[26,32174,theory(equality)]) ).
cnf(32200,negated_conjecture,
( program(esk3_1(X1))
| outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(spm,[status(thm)],[119,32174,theory(equality)]) ).
cnf(33075,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(spm,[status(thm)],[32196,820,theory(equality)]) ).
cnf(33084,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| $false
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(rw,[status(thm)],[33075,129,theory(equality)]) ).
cnf(33085,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(cn,[status(thm)],[33084,theory(equality)]) ).
cnf(33107,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[33085,274,theory(equality)]) ).
cnf(33110,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[33107,7433]) ).
cnf(33141,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| outputs(X1,bad)
| outputs(X11,good)
| program(esk1_1(X11))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X1) ),
inference(spm,[status(thm)],[33110,83,theory(equality)]) ).
cnf(33897,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X11))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(csr,[status(thm)],[33141,17316]) ).
cnf(33898,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X11))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(csr,[status(thm)],[33897,17316]) ).
cnf(33899,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X11))
| ~ program(X11)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[33898,17316]) ).
cnf(33900,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X11))
| ~ program(X11)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[33899,17316]) ).
cnf(33901,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X11))
| ~ program(X11)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[33900,17316]) ).
cnf(33902,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| outputs(X11,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X11) ),
inference(csr,[status(thm)],[33901,32174]) ).
cnf(33932,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,bad)
| program(esk5_1(esk9_0))
| outputs(X3,bad)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X1)
| ~ program(X9)
| ~ program(X10)
| ~ program(X3) ),
inference(spm,[status(thm)],[33902,83,theory(equality)]) ).
cnf(36612,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,bad)
| outputs(X3,bad)
| outputs(X9,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X9))
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X1)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[33932,17316]) ).
cnf(36613,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,bad)
| outputs(X3,bad)
| outputs(X9,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X9))
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X1)
| ~ program(X9) ),
inference(csr,[status(thm)],[36612,17316]) ).
cnf(36614,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,bad)
| outputs(X3,bad)
| outputs(X9,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X9))
| ~ program(X1)
| ~ program(X9)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[36613,19431]) ).
cnf(36615,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,bad)
| outputs(X3,bad)
| outputs(X9,good)
| program(esk5_1(esk9_0))
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1)
| ~ program(X9) ),
inference(csr,[status(thm)],[36614,33902]) ).
cnf(36616,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X10,bad)
| outputs(X11,bad)
| outputs(X9,good)
| program(esk5_1(esk9_0))
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15)
| ~ program(X9) ),
inference(ef,[status(thm)],[36615,theory(equality)]) ).
cnf(36845,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X8,good)
| outputs(X9,bad)
| program(esk5_1(esk9_0))
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X8) ),
inference(ef,[status(thm)],[36616,theory(equality)]) ).
cnf(37078,negated_conjecture,
( program(esk5_1(X1))
| outputs(esk9_0,good)
| outputs(X2,bad)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(spm,[status(thm)],[26,36845,theory(equality)]) ).
cnf(37082,negated_conjecture,
( halts2(esk3_1(X1),esk4_1(X1))
| program(esk5_1(X1))
| outputs(esk9_0,good)
| outputs(X2,good)
| program(esk5_1(esk9_0))
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X2) ),
inference(spm,[status(thm)],[29,36845,theory(equality)]) ).
cnf(37448,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[37078,820,theory(equality)]) ).
cnf(37457,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(rw,[status(thm)],[37448,129,theory(equality)]) ).
cnf(37458,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| program(esk5_1(esk9_0))
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(cn,[status(thm)],[37457,theory(equality)]) ).
cnf(37476,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[37458,274,theory(equality)]) ).
cnf(37479,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,bad)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[37476,7433]) ).
cnf(39460,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(X2),esk4_1(X2))
| program(esk5_1(esk9_0))
| program(esk5_1(X2))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X1)
| ~ program(esk3_1(X2)) ),
inference(spm,[status(thm)],[37082,89,theory(equality)]) ).
cnf(39471,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(X2),esk4_1(X2))
| program(esk5_1(esk9_0))
| program(esk5_1(X2))
| program(esk1_1(X2))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X1) ),
inference(csr,[status(thm)],[39460,34]) ).
cnf(39480,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X2))
| program(esk5_1(X2))
| ~ program(X1)
| ~ program(esk3_1(X2))
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X3) ),
inference(spm,[status(thm)],[18,39471,theory(equality)]) ).
cnf(39568,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| program(esk1_1(X2))
| program(esk5_1(X2))
| ~ program(esk3_1(X2))
| ~ program(X1)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[39480,17316]) ).
cnf(39569,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| program(esk1_1(X2))
| program(esk5_1(X2))
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1) ),
inference(csr,[status(thm)],[39568,34]) ).
cnf(39570,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| program(esk1_1(X2))
| ~ program(X1)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[39569,17316]) ).
cnf(39571,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[39570,17316]) ).
cnf(39591,negated_conjecture,
( program(esk3_1(X1))
| outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk1_1(X3))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[119,39571,theory(equality)]) ).
cnf(39610,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[169,39571,theory(equality)]) ).
cnf(39847,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(rw,[status(thm)],[39610,129,theory(equality)]) ).
cnf(39848,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(cn,[status(thm)],[39847,theory(equality)]) ).
cnf(39863,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(spm,[status(thm)],[39848,17199,theory(equality)]) ).
cnf(39908,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(csr,[status(thm)],[39863,33110]) ).
cnf(39909,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[39908,33110]) ).
cnf(39910,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[39909,7433]) ).
cnf(39942,negated_conjecture,
( program(esk3_1(X1))
| outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(spm,[status(thm)],[119,39910,theory(equality)]) ).
cnf(40829,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[39942,33110]) ).
cnf(40830,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[40829,32200]) ).
cnf(40831,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[40830,37479]) ).
cnf(40832,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[40831,33110]) ).
cnf(40834,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[40832,274,theory(equality)]) ).
cnf(40835,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(rw,[status(thm)],[40834,129,theory(equality)]) ).
cnf(40836,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(cn,[status(thm)],[40835,theory(equality)]) ).
cnf(41718,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| program(esk1_1(X3))
| ~ outputs(X1,bad)
| ~ halts3(X1,X2,X2)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[39591,17316]) ).
cnf(41719,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| program(esk1_1(X3))
| ~ outputs(X1,bad)
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[41718,17316]) ).
cnf(41720,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| program(esk1_1(X3))
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[41719,17316]) ).
cnf(41721,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| program(esk3_1(X1))
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[41720,40836]) ).
cnf(41722,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[41721,40836]) ).
cnf(41741,negated_conjecture,
( program(esk5_1(X1))
| outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ outputs(X1,bad)
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(spm,[status(thm)],[26,41722,theory(equality)]) ).
cnf(42053,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| program(esk5_1(X1))
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[41741,37479]) ).
cnf(42054,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ halts3(X1,esk3_1(X1),esk4_1(X1))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[42053,40836]) ).
cnf(42056,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(esk9_0)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[42054,274,theory(equality)]) ).
cnf(42057,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| $false
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(esk3_1(esk9_0)) ),
inference(rw,[status(thm)],[42056,129,theory(equality)]) ).
cnf(42058,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(esk3_1(esk9_0)) ),
inference(cn,[status(thm)],[42057,theory(equality)]) ).
cnf(42059,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[42058,7433]) ).
cnf(42134,negated_conjecture,
( outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| program(esk1_1(X3))
| outputs(esk9_0,good)
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(spm,[status(thm)],[6732,42059,theory(equality)]) ).
cnf(42135,negated_conjecture,
( outputs(esk9_0,good)
| program(esk5_1(esk9_0))
| outputs(X1,good)
| outputs(X7,good)
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1)
| ~ program(X8) ),
inference(spm,[status(thm)],[42059,6865,theory(equality)]) ).
cnf(42587,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X1) ),
inference(csr,[status(thm)],[42135,7433]) ).
cnf(42588,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[42587,7433]) ).
cnf(42589,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk5_1(esk9_0))
| program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[42588,7303]) ).
cnf(42590,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk5_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[42589,42059]) ).
cnf(42591,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X8,good)
| program(esk5_1(esk9_0))
| ~ program(X9)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13) ),
inference(ef,[status(thm)],[42590,theory(equality)]) ).
cnf(43778,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| outputs(X3,good)
| program(esk1_1(X1))
| ~ program(X3)
| ~ program(X1)
| ~ program(X4)
| ~ program(X2)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[42134,30795]) ).
cnf(43779,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X11,good)
| outputs(X12,good)
| program(esk1_1(X12))
| ~ program(X11)
| ~ program(X12)
| ~ program(X13)
| ~ program(X14)
| ~ program(X15)
| ~ program(X16)
| ~ program(X17)
| ~ program(X18)
| ~ program(X19) ),
inference(ef,[status(thm)],[43778,theory(equality)]) ).
cnf(44119,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(esk9_0)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(spm,[status(thm)],[169,43779,theory(equality)]) ).
cnf(44333,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| $false
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(rw,[status(thm)],[44119,129,theory(equality)]) ).
cnf(44334,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(cn,[status(thm)],[44333,theory(equality)]) ).
cnf(44342,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X2)
| ~ program(X11)
| ~ program(X12)
| ~ program(X13) ),
inference(spm,[status(thm)],[44334,2215,theory(equality)]) ).
cnf(45477,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X2)
| ~ program(X11)
| ~ program(X12) ),
inference(csr,[status(thm)],[44342,43779]) ).
cnf(45478,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X2)
| ~ program(X11) ),
inference(csr,[status(thm)],[45477,43779]) ).
cnf(45479,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X2) ),
inference(csr,[status(thm)],[45478,43779]) ).
cnf(45480,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[45479,43779]) ).
cnf(45481,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(esk5_1(esk9_0))
| ~ program(X10)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[45480,43779]) ).
cnf(45482,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X10,good)
| program(esk1_1(X10))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X10) ),
inference(csr,[status(thm)],[45481,17316]) ).
cnf(45527,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[169,45482,theory(equality)]) ).
cnf(45721,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| $false ),
inference(rw,[status(thm)],[45527,129,theory(equality)]) ).
cnf(45722,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(cn,[status(thm)],[45721,theory(equality)]) ).
cnf(45730,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X2)
| ~ program(X10)
| ~ program(X11)
| ~ program(X12) ),
inference(spm,[status(thm)],[45722,2215,theory(equality)]) ).
cnf(46355,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X2)
| ~ program(X10)
| ~ program(X11) ),
inference(csr,[status(thm)],[45730,45482]) ).
cnf(46356,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X2)
| ~ program(X10) ),
inference(csr,[status(thm)],[46355,45482]) ).
cnf(46357,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X2) ),
inference(csr,[status(thm)],[46356,45482]) ).
cnf(46358,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[46357,45482]) ).
cnf(46359,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(esk5_1(esk9_0))
| ~ program(X9)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[46358,45482]) ).
cnf(46360,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X9,good)
| program(esk1_1(X9))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X9) ),
inference(csr,[status(thm)],[46359,17316]) ).
cnf(46399,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[169,46360,theory(equality)]) ).
cnf(46580,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| $false ),
inference(rw,[status(thm)],[46399,129,theory(equality)]) ).
cnf(46581,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(cn,[status(thm)],[46580,theory(equality)]) ).
cnf(46589,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X2)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(spm,[status(thm)],[46581,2215,theory(equality)]) ).
cnf(47168,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X2)
| ~ program(X9)
| ~ program(X10) ),
inference(csr,[status(thm)],[46589,46360]) ).
cnf(47169,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X2)
| ~ program(X9) ),
inference(csr,[status(thm)],[47168,46360]) ).
cnf(47170,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X2) ),
inference(csr,[status(thm)],[47169,46360]) ).
cnf(47171,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[47170,46360]) ).
cnf(47172,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(esk5_1(esk9_0))
| ~ program(X8)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[47171,46360]) ).
cnf(47173,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X8,good)
| program(esk1_1(X8))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X8) ),
inference(csr,[status(thm)],[47172,42059]) ).
cnf(47206,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[169,47173,theory(equality)]) ).
cnf(47374,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| $false ),
inference(rw,[status(thm)],[47206,129,theory(equality)]) ).
cnf(47375,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(cn,[status(thm)],[47374,theory(equality)]) ).
cnf(47383,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X2)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10) ),
inference(spm,[status(thm)],[47375,2215,theory(equality)]) ).
cnf(47910,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X2)
| ~ program(X8)
| ~ program(X9) ),
inference(csr,[status(thm)],[47383,47173]) ).
cnf(47911,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X2)
| ~ program(X8) ),
inference(csr,[status(thm)],[47910,47173]) ).
cnf(47912,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X2) ),
inference(csr,[status(thm)],[47911,47173]) ).
cnf(47913,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[47912,47173]) ).
cnf(47914,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(esk5_1(esk9_0))
| ~ program(X7)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[47913,47173]) ).
cnf(47915,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X7,good)
| program(esk1_1(X7))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X7) ),
inference(csr,[status(thm)],[47914,42591]) ).
cnf(47942,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(esk9_0) ),
inference(spm,[status(thm)],[169,47915,theory(equality)]) ).
cnf(48097,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| $false ),
inference(rw,[status(thm)],[47942,129,theory(equality)]) ).
cnf(48098,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(cn,[status(thm)],[48097,theory(equality)]) ).
cnf(48105,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X2)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[48098,2179,theory(equality)]) ).
cnf(48671,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X2)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[48105,17199]) ).
cnf(48686,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(esk9_0,good)
| outputs(X2,good)
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(spm,[status(thm)],[18,48671,theory(equality)]) ).
cnf(48826,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(csr,[status(thm)],[48686,47915]) ).
cnf(48827,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[48826,47915]) ).
cnf(48828,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[48827,47915]) ).
cnf(48829,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[48828,47915]) ).
cnf(48830,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[48829,47915]) ).
cnf(48831,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X1) ),
inference(csr,[status(thm)],[48830,6865]) ).
cnf(48852,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(spm,[status(thm)],[169,48831,theory(equality)]) ).
cnf(48989,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(rw,[status(thm)],[48852,129,theory(equality)]) ).
cnf(48990,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(cn,[status(thm)],[48989,theory(equality)]) ).
cnf(48997,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X2)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(spm,[status(thm)],[48990,2179,theory(equality)]) ).
cnf(49478,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| halts2(esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X2)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[48997,17199]) ).
cnf(49491,negated_conjecture,
( outputs(X1,good)
| program(esk1_1(X1))
| outputs(esk9_0,good)
| outputs(X2,good)
| ~ program(X1)
| ~ program(esk3_1(esk9_0))
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8) ),
inference(spm,[status(thm)],[18,49478,theory(equality)]) ).
cnf(49618,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(csr,[status(thm)],[49491,48831]) ).
cnf(49619,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6) ),
inference(csr,[status(thm)],[49618,48831]) ).
cnf(49620,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(csr,[status(thm)],[49619,48831]) ).
cnf(49621,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(csr,[status(thm)],[49620,48831]) ).
cnf(49622,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3) ),
inference(csr,[status(thm)],[49621,48831]) ).
cnf(49623,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X2,good)
| program(esk1_1(X1))
| ~ program(X2)
| ~ program(X3)
| ~ program(X1) ),
inference(csr,[status(thm)],[49622,6865]) ).
cnf(49638,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X3)
| ~ program(X4) ),
inference(spm,[status(thm)],[169,49623,theory(equality)]) ).
cnf(49762,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| $false
| ~ program(X3)
| ~ program(X4) ),
inference(rw,[status(thm)],[49638,129,theory(equality)]) ).
cnf(49763,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X3,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4) ),
inference(cn,[status(thm)],[49762,theory(equality)]) ).
cnf(49773,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| halts2(esk5_1(esk9_0),X4)
| ~ program(esk3_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X3) ),
inference(spm,[status(thm)],[49763,3530,theory(equality)]) ).
cnf(50329,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X3,good)
| halts2(esk5_1(esk9_0),X4)
| ~ program(X1)
| ~ program(X2)
| ~ program(X4)
| ~ program(X5)
| ~ program(X3) ),
inference(csr,[status(thm)],[49773,543]) ).
cnf(50330,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X6,good)
| halts2(esk5_1(esk9_0),X7)
| ~ program(X6)
| ~ program(X8)
| ~ program(X7)
| ~ program(X9) ),
inference(ef,[status(thm)],[50329,theory(equality)]) ).
cnf(50432,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X4,good)
| ~ program(esk5_1(esk9_0))
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X2)
| ~ program(X6) ),
inference(spm,[status(thm)],[49763,50330,theory(equality)]) ).
cnf(50465,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X1,good)
| outputs(X4,good)
| ~ program(X1)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X2)
| ~ program(X6) ),
inference(csr,[status(thm)],[50432,42059]) ).
cnf(50466,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X7,good)
| ~ program(X7)
| ~ program(X8)
| ~ program(esk9_0)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(ef,[status(thm)],[50465,theory(equality)]) ).
cnf(50558,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X7,good)
| ~ program(X7)
| ~ program(X8)
| $false
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(rw,[status(thm)],[50466,129,theory(equality)]) ).
cnf(50559,negated_conjecture,
( outputs(esk9_0,good)
| outputs(X7,good)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9)
| ~ program(X10)
| ~ program(X11) ),
inference(cn,[status(thm)],[50558,theory(equality)]) ).
cnf(50578,negated_conjecture,
( outputs(esk9_0,good)
| ~ program(esk9_0)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(ef,[status(thm)],[50559,theory(equality)]) ).
cnf(50660,negated_conjecture,
( outputs(esk9_0,good)
| $false
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(rw,[status(thm)],[50578,129,theory(equality)]) ).
cnf(50661,negated_conjecture,
( outputs(esk9_0,good)
| ~ program(X6)
| ~ program(X7)
| ~ program(X8)
| ~ program(X9) ),
inference(cn,[status(thm)],[50660,theory(equality)]) ).
cnf(50691,negated_conjecture,
( ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(esk9_0)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(spm,[status(thm)],[112,50661,theory(equality)]) ).
cnf(50748,negated_conjecture,
( ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| $false
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(rw,[status(thm)],[50691,129,theory(equality)]) ).
cnf(50749,negated_conjecture,
( ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ halts3(esk9_0,X1,X1)
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5) ),
inference(cn,[status(thm)],[50748,theory(equality)]) ).
fof(50750,plain,
( ~ epred1_0
<=> ! [X1] :
( ~ program(X1)
| ~ halts3(esk9_0,X1,X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ outputs(esk9_0,bad) ) ),
introduced(definition),
[split] ).
cnf(50751,plain,
( epred1_0
| ~ program(X1)
| ~ halts3(esk9_0,X1,X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ outputs(esk9_0,bad) ),
inference(split_equiv,[status(thm)],[50750]) ).
fof(50752,plain,
( ~ epred2_0
<=> ! [X2] : ~ program(X2) ),
introduced(definition),
[split] ).
cnf(50753,plain,
( epred2_0
| ~ program(X2) ),
inference(split_equiv,[status(thm)],[50752]) ).
fof(50754,plain,
( ~ epred3_0
<=> ! [X3] : ~ program(X3) ),
introduced(definition),
[split] ).
cnf(50755,plain,
( epred3_0
| ~ program(X3) ),
inference(split_equiv,[status(thm)],[50754]) ).
fof(50756,plain,
( ~ epred4_0
<=> ! [X4] : ~ program(X4) ),
introduced(definition),
[split] ).
cnf(50757,plain,
( epred4_0
| ~ program(X4) ),
inference(split_equiv,[status(thm)],[50756]) ).
fof(50758,plain,
( ~ epred5_0
<=> ! [X5] : ~ program(X5) ),
introduced(definition),
[split] ).
cnf(50759,plain,
( epred5_0
| ~ program(X5) ),
inference(split_equiv,[status(thm)],[50758]) ).
cnf(50760,negated_conjecture,
( ~ epred5_0
| ~ epred4_0
| ~ epred3_0
| ~ epred2_0
| ~ epred1_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[50749,50750,theory(equality)]),50752,theory(equality)]),50754,theory(equality)]),50756,theory(equality)]),50758,theory(equality)]),
[split] ).
cnf(50776,negated_conjecture,
epred2_0,
inference(spm,[status(thm)],[50753,129,theory(equality)]) ).
cnf(50794,negated_conjecture,
epred3_0,
inference(spm,[status(thm)],[50755,129,theory(equality)]) ).
cnf(50835,negated_conjecture,
epred4_0,
inference(spm,[status(thm)],[50757,129,theory(equality)]) ).
cnf(50853,negated_conjecture,
epred5_0,
inference(spm,[status(thm)],[50759,129,theory(equality)]) ).
cnf(50948,negated_conjecture,
( $false
| ~ epred4_0
| ~ epred3_0
| ~ epred2_0
| ~ epred1_0 ),
inference(rw,[status(thm)],[50760,50853,theory(equality)]) ).
cnf(50949,negated_conjecture,
( $false
| $false
| ~ epred3_0
| ~ epred2_0
| ~ epred1_0 ),
inference(rw,[status(thm)],[50948,50835,theory(equality)]) ).
cnf(50950,negated_conjecture,
( $false
| $false
| $false
| ~ epred2_0
| ~ epred1_0 ),
inference(rw,[status(thm)],[50949,50794,theory(equality)]) ).
cnf(50951,negated_conjecture,
( $false
| $false
| $false
| $false
| ~ epred1_0 ),
inference(rw,[status(thm)],[50950,50776,theory(equality)]) ).
cnf(50952,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[50951,theory(equality)]) ).
cnf(50964,negated_conjecture,
( ~ program(X1)
| ~ halts3(esk9_0,X1,X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ outputs(esk9_0,bad) ),
inference(sr,[status(thm)],[50751,50952,theory(equality)]) ).
cnf(50965,negated_conjecture,
( ~ outputs(esk9_0,bad)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1) ),
inference(csr,[status(thm)],[50964,274]) ).
cnf(50966,negated_conjecture,
( ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0))
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4) ),
inference(spm,[status(thm)],[50965,820,theory(equality)]) ).
fof(50968,plain,
( ~ epred11_0
<=> ! [X1] :
( ~ program(X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0)) ) ),
introduced(definition),
[split] ).
cnf(50969,plain,
( epred11_0
| ~ program(X1)
| ~ halts3(esk9_0,esk3_1(esk9_0),esk4_1(esk9_0)) ),
inference(split_equiv,[status(thm)],[50968]) ).
fof(50970,plain,
( ~ epred12_0
<=> ! [X2] : ~ program(X2) ),
introduced(definition),
[split] ).
cnf(50971,plain,
( epred12_0
| ~ program(X2) ),
inference(split_equiv,[status(thm)],[50970]) ).
fof(50972,plain,
( ~ epred13_0
<=> ! [X3] : ~ program(X3) ),
introduced(definition),
[split] ).
cnf(50973,plain,
( epred13_0
| ~ program(X3) ),
inference(split_equiv,[status(thm)],[50972]) ).
fof(50974,plain,
( ~ epred14_0
<=> ! [X4] : ~ program(X4) ),
introduced(definition),
[split] ).
cnf(50975,plain,
( epred14_0
| ~ program(X4) ),
inference(split_equiv,[status(thm)],[50974]) ).
cnf(50976,negated_conjecture,
( ~ epred14_0
| ~ epred13_0
| ~ epred12_0
| ~ epred11_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[50966,50968,theory(equality)]),50970,theory(equality)]),50972,theory(equality)]),50974,theory(equality)]),
[split] ).
cnf(50981,negated_conjecture,
epred12_0,
inference(spm,[status(thm)],[50971,129,theory(equality)]) ).
cnf(50999,negated_conjecture,
epred13_0,
inference(spm,[status(thm)],[50973,129,theory(equality)]) ).
cnf(51017,negated_conjecture,
epred14_0,
inference(spm,[status(thm)],[50975,129,theory(equality)]) ).
cnf(51036,negated_conjecture,
( epred11_0
| ~ program(X1)
| ~ program(esk3_1(esk9_0)) ),
inference(spm,[status(thm)],[50969,274,theory(equality)]) ).
cnf(51039,negated_conjecture,
( epred11_0
| ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(spm,[status(thm)],[51036,7433,theory(equality)]) ).
cnf(51041,negated_conjecture,
( $false
| ~ epred13_0
| ~ epred12_0
| ~ epred11_0 ),
inference(rw,[status(thm)],[50976,51017,theory(equality)]) ).
cnf(51042,negated_conjecture,
( $false
| $false
| ~ epred12_0
| ~ epred11_0 ),
inference(rw,[status(thm)],[51041,50999,theory(equality)]) ).
cnf(51043,negated_conjecture,
( $false
| $false
| $false
| ~ epred11_0 ),
inference(rw,[status(thm)],[51042,50981,theory(equality)]) ).
cnf(51044,negated_conjecture,
~ epred11_0,
inference(cn,[status(thm)],[51043,theory(equality)]) ).
cnf(51050,negated_conjecture,
( ~ program(X1)
| ~ program(X2)
| ~ program(X3)
| ~ program(X4)
| ~ program(X5)
| ~ program(X6)
| ~ program(X7) ),
inference(sr,[status(thm)],[51039,51044,theory(equality)]) ).
fof(51051,plain,
( ~ epred15_0
<=> ! [X1] : ~ program(X1) ),
introduced(definition),
[split] ).
cnf(51052,plain,
( epred15_0
| ~ program(X1) ),
inference(split_equiv,[status(thm)],[51051]) ).
fof(51053,plain,
( ~ epred16_0
<=> ! [X2] : ~ program(X2) ),
introduced(definition),
[split] ).
cnf(51054,plain,
( epred16_0
| ~ program(X2) ),
inference(split_equiv,[status(thm)],[51053]) ).
fof(51055,plain,
( ~ epred17_0
<=> ! [X3] : ~ program(X3) ),
introduced(definition),
[split] ).
cnf(51056,plain,
( epred17_0
| ~ program(X3) ),
inference(split_equiv,[status(thm)],[51055]) ).
fof(51057,plain,
( ~ epred18_0
<=> ! [X4] : ~ program(X4) ),
introduced(definition),
[split] ).
cnf(51058,plain,
( epred18_0
| ~ program(X4) ),
inference(split_equiv,[status(thm)],[51057]) ).
fof(51059,plain,
( ~ epred19_0
<=> ! [X5] : ~ program(X5) ),
introduced(definition),
[split] ).
cnf(51060,plain,
( epred19_0
| ~ program(X5) ),
inference(split_equiv,[status(thm)],[51059]) ).
fof(51061,plain,
( ~ epred20_0
<=> ! [X6] : ~ program(X6) ),
introduced(definition),
[split] ).
cnf(51062,plain,
( epred20_0
| ~ program(X6) ),
inference(split_equiv,[status(thm)],[51061]) ).
fof(51063,plain,
( ~ epred21_0
<=> ! [X7] : ~ program(X7) ),
introduced(definition),
[split] ).
cnf(51064,plain,
( epred21_0
| ~ program(X7) ),
inference(split_equiv,[status(thm)],[51063]) ).
cnf(51065,negated_conjecture,
( ~ epred21_0
| ~ epred20_0
| ~ epred19_0
| ~ epred18_0
| ~ epred17_0
| ~ epred16_0
| ~ epred15_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[51050,51051,theory(equality)]),51053,theory(equality)]),51055,theory(equality)]),51057,theory(equality)]),51059,theory(equality)]),51061,theory(equality)]),51063,theory(equality)]),
[split] ).
cnf(51066,negated_conjecture,
epred15_0,
inference(spm,[status(thm)],[51052,129,theory(equality)]) ).
cnf(51084,negated_conjecture,
epred16_0,
inference(spm,[status(thm)],[51054,129,theory(equality)]) ).
cnf(51102,negated_conjecture,
epred17_0,
inference(spm,[status(thm)],[51056,129,theory(equality)]) ).
cnf(51120,negated_conjecture,
epred18_0,
inference(spm,[status(thm)],[51058,129,theory(equality)]) ).
cnf(51138,negated_conjecture,
epred19_0,
inference(spm,[status(thm)],[51060,129,theory(equality)]) ).
cnf(51220,negated_conjecture,
epred20_0,
inference(spm,[status(thm)],[51062,129,theory(equality)]) ).
cnf(51237,negated_conjecture,
epred21_0,
inference(spm,[status(thm)],[51064,129,theory(equality)]) ).
cnf(51495,negated_conjecture,
( $false
| ~ epred20_0
| ~ epred19_0
| ~ epred18_0
| ~ epred17_0
| ~ epred16_0
| ~ epred15_0 ),
inference(rw,[status(thm)],[51065,51237,theory(equality)]) ).
cnf(51496,negated_conjecture,
( $false
| $false
| ~ epred19_0
| ~ epred18_0
| ~ epred17_0
| ~ epred16_0
| ~ epred15_0 ),
inference(rw,[status(thm)],[51495,51220,theory(equality)]) ).
cnf(51497,negated_conjecture,
( $false
| $false
| $false
| ~ epred18_0
| ~ epred17_0
| ~ epred16_0
| ~ epred15_0 ),
inference(rw,[status(thm)],[51496,51138,theory(equality)]) ).
cnf(51498,negated_conjecture,
( $false
| $false
| $false
| $false
| ~ epred17_0
| ~ epred16_0
| ~ epred15_0 ),
inference(rw,[status(thm)],[51497,51120,theory(equality)]) ).
cnf(51499,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| ~ epred16_0
| ~ epred15_0 ),
inference(rw,[status(thm)],[51498,51102,theory(equality)]) ).
cnf(51500,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| ~ epred15_0 ),
inference(rw,[status(thm)],[51499,51084,theory(equality)]) ).
cnf(51501,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[51500,51066,theory(equality)]) ).
cnf(51502,negated_conjecture,
$false,
inference(cn,[status(thm)],[51501,theory(equality)]) ).
cnf(51503,negated_conjecture,
$false,
51502,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/COM/COM003+3.p
% --creating new selector for []
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpYKn8_K/sel_COM003+3.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpYKn8_K/sel_COM003+3.p_2 with time limit 81
% -prover status Theorem
% Problem COM003+3.p solved in phase 1.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/COM/COM003+3.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/COM/COM003+3.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
%
%------------------------------------------------------------------------------