%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : KRS081+1 : TPTP v5.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 12:57:51 EST 2010
% Result : Unsatisfiable 0.32s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 6
% Syntax : Number of formulae : 82 ( 5 unt; 0 def)
% Number of atoms : 1089 ( 260 equ)
% Maximal formula atoms : 420 ( 13 avg)
% Number of connectives : 1677 ( 670 ~; 771 |; 229 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-1 aty)
% Number of variables : 205 ( 1 sgn 97 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
cUnsatisfiable(i2003_11_14_17_19_24236),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_7) ).
fof(3,axiom,
! [X3] :
( cp4(X3)
=> ~ cp5(X3) ),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_6) ).
fof(8,axiom,
! [X3] :
( cUnsatisfiable(X3)
<=> ( ? [X4] :
( rr(X3,X4)
& cp3(X4) )
& ? [X4] :
( rr(X3,X4)
& cp4(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp4(X4) )
& ? [X4] :
( rr(X3,X4)
& cp2(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp5(X4) )
& ? [X4] :
( rr(X3,X4)
& cp(X4)
& cp3(X4) )
& ? [X4] :
( rr(X3,X4)
& cp1(X4) )
& ! [X5,X6,X7,X8,X9] :
( ( rr(X3,X5)
& rr(X3,X6)
& rr(X3,X7)
& rr(X3,X8)
& rr(X3,X9) )
=> ( X5 = X6
| X5 = X7
| X5 = X8
| X5 = X9
| X6 = X7
| X6 = X8
| X6 = X9
| X7 = X8
| X7 = X9
| X8 = X9 ) )
& ? [X4] :
( rr(X3,X4)
& cp1(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp2(X4) ) ) ),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_2) ).
fof(9,axiom,
! [X3] :
( cp1(X3)
=> ~ ( cp2(X3)
| cp4(X3)
| cp5(X3)
| cp3(X3) ) ),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_3) ).
fof(14,axiom,
! [X3] :
( cp2(X3)
=> ~ ( cp4(X3)
| cp5(X3)
| cp3(X3) ) ),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_4) ).
fof(15,axiom,
! [X3] :
( cp3(X3)
=> ~ ( cp4(X3)
| cp5(X3) ) ),
file('/tmp/tmpzSsO5W/sel_KRS081+1.p_1',axiom_5) ).
fof(22,plain,
! [X3] :
( cp4(X3)
=> ~ cp5(X3) ),
inference(fof_simplification,[status(thm)],[3,theory(equality)]) ).
cnf(28,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(split_conjunct,[status(thm)],[2]) ).
fof(29,plain,
! [X3] :
( ~ cp4(X3)
| ~ cp5(X3) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(30,plain,
! [X4] :
( ~ cp4(X4)
| ~ cp5(X4) ),
inference(variable_rename,[status(thm)],[29]) ).
cnf(31,plain,
( ~ cp5(X1)
| ~ cp4(X1) ),
inference(split_conjunct,[status(thm)],[30]) ).
fof(44,plain,
! [X3] :
( ( ~ cUnsatisfiable(X3)
| ( ? [X4] :
( rr(X3,X4)
& cp3(X4) )
& ? [X4] :
( rr(X3,X4)
& cp4(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp4(X4) )
& ? [X4] :
( rr(X3,X4)
& cp2(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp5(X4) )
& ? [X4] :
( rr(X3,X4)
& cp(X4)
& cp3(X4) )
& ? [X4] :
( rr(X3,X4)
& cp1(X4) )
& ! [X5,X6,X7,X8,X9] :
( ~ rr(X3,X5)
| ~ rr(X3,X6)
| ~ rr(X3,X7)
| ~ rr(X3,X8)
| ~ rr(X3,X9)
| X5 = X6
| X5 = X7
| X5 = X8
| X5 = X9
| X6 = X7
| X6 = X8
| X6 = X9
| X7 = X8
| X7 = X9
| X8 = X9 )
& ? [X4] :
( rr(X3,X4)
& cp1(X4)
& cp(X4) )
& ? [X4] :
( rr(X3,X4)
& cp2(X4) ) ) )
& ( ! [X4] :
( ~ rr(X3,X4)
| ~ cp3(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp4(X4)
| ~ cp(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp4(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp2(X4)
| ~ cp(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp5(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp(X4)
| ~ cp3(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp1(X4) )
| ? [X5,X6,X7,X8,X9] :
( rr(X3,X5)
& rr(X3,X6)
& rr(X3,X7)
& rr(X3,X8)
& rr(X3,X9)
& X5 != X6
& X5 != X7
& X5 != X8
& X5 != X9
& X6 != X7
& X6 != X8
& X6 != X9
& X7 != X8
& X7 != X9
& X8 != X9 )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp1(X4)
| ~ cp(X4) )
| ! [X4] :
( ~ rr(X3,X4)
| ~ cp2(X4) )
| cUnsatisfiable(X3) ) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(45,plain,
! [X10] :
( ( ~ cUnsatisfiable(X10)
| ( ? [X11] :
( rr(X10,X11)
& cp3(X11) )
& ? [X12] :
( rr(X10,X12)
& cp4(X12)
& cp(X12) )
& ? [X13] :
( rr(X10,X13)
& cp4(X13) )
& ? [X14] :
( rr(X10,X14)
& cp2(X14)
& cp(X14) )
& ? [X15] :
( rr(X10,X15)
& cp5(X15) )
& ? [X16] :
( rr(X10,X16)
& cp(X16)
& cp3(X16) )
& ? [X17] :
( rr(X10,X17)
& cp1(X17) )
& ! [X18,X19,X20,X21,X22] :
( ~ rr(X10,X18)
| ~ rr(X10,X19)
| ~ rr(X10,X20)
| ~ rr(X10,X21)
| ~ rr(X10,X22)
| X18 = X19
| X18 = X20
| X18 = X21
| X18 = X22
| X19 = X20
| X19 = X21
| X19 = X22
| X20 = X21
| X20 = X22
| X21 = X22 )
& ? [X23] :
( rr(X10,X23)
& cp1(X23)
& cp(X23) )
& ? [X24] :
( rr(X10,X24)
& cp2(X24) ) ) )
& ( ! [X25] :
( ~ rr(X10,X25)
| ~ cp3(X25) )
| ! [X26] :
( ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26) )
| ! [X27] :
( ~ rr(X10,X27)
| ~ cp4(X27) )
| ! [X28] :
( ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28) )
| ! [X29] :
( ~ rr(X10,X29)
| ~ cp5(X29) )
| ! [X30] :
( ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30) )
| ! [X31] :
( ~ rr(X10,X31)
| ~ cp1(X31) )
| ? [X32,X33,X34,X35,X36] :
( rr(X10,X32)
& rr(X10,X33)
& rr(X10,X34)
& rr(X10,X35)
& rr(X10,X36)
& X32 != X33
& X32 != X34
& X32 != X35
& X32 != X36
& X33 != X34
& X33 != X35
& X33 != X36
& X34 != X35
& X34 != X36
& X35 != X36 )
| ! [X37] :
( ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37) )
| ! [X38] :
( ~ rr(X10,X38)
| ~ cp2(X38) )
| cUnsatisfiable(X10) ) ),
inference(variable_rename,[status(thm)],[44]) ).
fof(46,plain,
! [X10] :
( ( ~ cUnsatisfiable(X10)
| ( rr(X10,esk1_1(X10))
& cp3(esk1_1(X10))
& rr(X10,esk2_1(X10))
& cp4(esk2_1(X10))
& cp(esk2_1(X10))
& rr(X10,esk3_1(X10))
& cp4(esk3_1(X10))
& rr(X10,esk4_1(X10))
& cp2(esk4_1(X10))
& cp(esk4_1(X10))
& rr(X10,esk5_1(X10))
& cp5(esk5_1(X10))
& rr(X10,esk6_1(X10))
& cp(esk6_1(X10))
& cp3(esk6_1(X10))
& rr(X10,esk7_1(X10))
& cp1(esk7_1(X10))
& ! [X18,X19,X20,X21,X22] :
( ~ rr(X10,X18)
| ~ rr(X10,X19)
| ~ rr(X10,X20)
| ~ rr(X10,X21)
| ~ rr(X10,X22)
| X18 = X19
| X18 = X20
| X18 = X21
| X18 = X22
| X19 = X20
| X19 = X21
| X19 = X22
| X20 = X21
| X20 = X22
| X21 = X22 )
& rr(X10,esk8_1(X10))
& cp1(esk8_1(X10))
& cp(esk8_1(X10))
& rr(X10,esk9_1(X10))
& cp2(esk9_1(X10)) ) )
& ( ! [X25] :
( ~ rr(X10,X25)
| ~ cp3(X25) )
| ! [X26] :
( ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26) )
| ! [X27] :
( ~ rr(X10,X27)
| ~ cp4(X27) )
| ! [X28] :
( ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28) )
| ! [X29] :
( ~ rr(X10,X29)
| ~ cp5(X29) )
| ! [X30] :
( ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30) )
| ! [X31] :
( ~ rr(X10,X31)
| ~ cp1(X31) )
| ( rr(X10,esk10_1(X10))
& rr(X10,esk11_1(X10))
& rr(X10,esk12_1(X10))
& rr(X10,esk13_1(X10))
& rr(X10,esk14_1(X10))
& esk10_1(X10) != esk11_1(X10)
& esk10_1(X10) != esk12_1(X10)
& esk10_1(X10) != esk13_1(X10)
& esk10_1(X10) != esk14_1(X10)
& esk11_1(X10) != esk12_1(X10)
& esk11_1(X10) != esk13_1(X10)
& esk11_1(X10) != esk14_1(X10)
& esk12_1(X10) != esk13_1(X10)
& esk12_1(X10) != esk14_1(X10)
& esk13_1(X10) != esk14_1(X10) )
| ! [X37] :
( ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37) )
| ! [X38] :
( ~ rr(X10,X38)
| ~ cp2(X38) )
| cUnsatisfiable(X10) ) ),
inference(skolemize,[status(esa)],[45]) ).
fof(47,plain,
! [X10,X18,X19,X20,X21,X22,X25,X26,X27,X28,X29,X30,X31,X37,X38] :
( ( ~ rr(X10,X38)
| ~ cp2(X38)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ( rr(X10,esk10_1(X10))
& rr(X10,esk11_1(X10))
& rr(X10,esk12_1(X10))
& rr(X10,esk13_1(X10))
& rr(X10,esk14_1(X10))
& esk10_1(X10) != esk11_1(X10)
& esk10_1(X10) != esk12_1(X10)
& esk10_1(X10) != esk13_1(X10)
& esk10_1(X10) != esk14_1(X10)
& esk11_1(X10) != esk12_1(X10)
& esk11_1(X10) != esk13_1(X10)
& esk11_1(X10) != esk14_1(X10)
& esk12_1(X10) != esk13_1(X10)
& esk12_1(X10) != esk14_1(X10)
& esk13_1(X10) != esk14_1(X10) )
| cUnsatisfiable(X10) )
& ( ( ( ~ rr(X10,X18)
| ~ rr(X10,X19)
| ~ rr(X10,X20)
| ~ rr(X10,X21)
| ~ rr(X10,X22)
| X18 = X19
| X18 = X20
| X18 = X21
| X18 = X22
| X19 = X20
| X19 = X21
| X19 = X22
| X20 = X21
| X20 = X22
| X21 = X22 )
& rr(X10,esk1_1(X10))
& cp3(esk1_1(X10))
& rr(X10,esk2_1(X10))
& cp4(esk2_1(X10))
& cp(esk2_1(X10))
& rr(X10,esk3_1(X10))
& cp4(esk3_1(X10))
& rr(X10,esk4_1(X10))
& cp2(esk4_1(X10))
& cp(esk4_1(X10))
& rr(X10,esk5_1(X10))
& cp5(esk5_1(X10))
& rr(X10,esk6_1(X10))
& cp(esk6_1(X10))
& cp3(esk6_1(X10))
& rr(X10,esk7_1(X10))
& cp1(esk7_1(X10))
& rr(X10,esk8_1(X10))
& cp1(esk8_1(X10))
& cp(esk8_1(X10))
& rr(X10,esk9_1(X10))
& cp2(esk9_1(X10)) )
| ~ cUnsatisfiable(X10) ) ),
inference(shift_quantors,[status(thm)],[46]) ).
fof(48,plain,
! [X10,X18,X19,X20,X21,X22,X25,X26,X27,X28,X29,X30,X31,X37,X38] :
( ( rr(X10,esk10_1(X10))
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( rr(X10,esk11_1(X10))
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( rr(X10,esk12_1(X10))
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( rr(X10,esk13_1(X10))
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( rr(X10,esk14_1(X10))
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk10_1(X10) != esk11_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk10_1(X10) != esk12_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk10_1(X10) != esk13_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk10_1(X10) != esk14_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk11_1(X10) != esk12_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk11_1(X10) != esk13_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk11_1(X10) != esk14_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk12_1(X10) != esk13_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk12_1(X10) != esk14_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( esk13_1(X10) != esk14_1(X10)
| ~ rr(X10,X31)
| ~ cp1(X31)
| ~ rr(X10,X30)
| ~ cp(X30)
| ~ cp3(X30)
| ~ rr(X10,X29)
| ~ cp5(X29)
| ~ rr(X10,X28)
| ~ cp2(X28)
| ~ cp(X28)
| ~ rr(X10,X27)
| ~ cp4(X27)
| ~ rr(X10,X26)
| ~ cp4(X26)
| ~ cp(X26)
| ~ rr(X10,X25)
| ~ cp3(X25)
| ~ rr(X10,X37)
| ~ cp1(X37)
| ~ cp(X37)
| ~ rr(X10,X38)
| ~ cp2(X38)
| cUnsatisfiable(X10) )
& ( ~ rr(X10,X18)
| ~ rr(X10,X19)
| ~ rr(X10,X20)
| ~ rr(X10,X21)
| ~ rr(X10,X22)
| X18 = X19
| X18 = X20
| X18 = X21
| X18 = X22
| X19 = X20
| X19 = X21
| X19 = X22
| X20 = X21
| X20 = X22
| X21 = X22
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk1_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp3(esk1_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk2_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp4(esk2_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp(esk2_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk3_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp4(esk3_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk4_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp2(esk4_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp(esk4_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk5_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp5(esk5_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk6_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp(esk6_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp3(esk6_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk7_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp1(esk7_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk8_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp1(esk8_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp(esk8_1(X10))
| ~ cUnsatisfiable(X10) )
& ( rr(X10,esk9_1(X10))
| ~ cUnsatisfiable(X10) )
& ( cp2(esk9_1(X10))
| ~ cUnsatisfiable(X10) ) ),
inference(distribute,[status(thm)],[47]) ).
cnf(54,plain,
( cp1(esk7_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(55,plain,
( rr(X1,esk7_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(59,plain,
( cp5(esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(60,plain,
( rr(X1,esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(62,plain,
( cp2(esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(63,plain,
( rr(X1,esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(67,plain,
( cp4(esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(68,plain,
( rr(X1,esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(69,plain,
( cp3(esk1_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(70,plain,
( rr(X1,esk1_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(71,plain,
( X2 = X3
| X4 = X3
| X4 = X2
| X5 = X3
| X5 = X2
| X5 = X4
| X6 = X3
| X6 = X2
| X6 = X4
| X6 = X5
| ~ cUnsatisfiable(X1)
| ~ rr(X1,X3)
| ~ rr(X1,X2)
| ~ rr(X1,X4)
| ~ rr(X1,X5)
| ~ rr(X1,X6) ),
inference(split_conjunct,[status(thm)],[48]) ).
fof(87,plain,
! [X3] :
( ~ cp1(X3)
| ( ~ cp2(X3)
& ~ cp4(X3)
& ~ cp5(X3)
& ~ cp3(X3) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(88,plain,
! [X4] :
( ~ cp1(X4)
| ( ~ cp2(X4)
& ~ cp4(X4)
& ~ cp5(X4)
& ~ cp3(X4) ) ),
inference(variable_rename,[status(thm)],[87]) ).
fof(89,plain,
! [X4] :
( ( ~ cp2(X4)
| ~ cp1(X4) )
& ( ~ cp4(X4)
| ~ cp1(X4) )
& ( ~ cp5(X4)
| ~ cp1(X4) )
& ( ~ cp3(X4)
| ~ cp1(X4) ) ),
inference(distribute,[status(thm)],[88]) ).
cnf(90,plain,
( ~ cp1(X1)
| ~ cp3(X1) ),
inference(split_conjunct,[status(thm)],[89]) ).
cnf(91,plain,
( ~ cp1(X1)
| ~ cp5(X1) ),
inference(split_conjunct,[status(thm)],[89]) ).
cnf(92,plain,
( ~ cp1(X1)
| ~ cp4(X1) ),
inference(split_conjunct,[status(thm)],[89]) ).
cnf(93,plain,
( ~ cp1(X1)
| ~ cp2(X1) ),
inference(split_conjunct,[status(thm)],[89]) ).
fof(107,plain,
! [X3] :
( ~ cp2(X3)
| ( ~ cp4(X3)
& ~ cp5(X3)
& ~ cp3(X3) ) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(108,plain,
! [X4] :
( ~ cp2(X4)
| ( ~ cp4(X4)
& ~ cp5(X4)
& ~ cp3(X4) ) ),
inference(variable_rename,[status(thm)],[107]) ).
fof(109,plain,
! [X4] :
( ( ~ cp4(X4)
| ~ cp2(X4) )
& ( ~ cp5(X4)
| ~ cp2(X4) )
& ( ~ cp3(X4)
| ~ cp2(X4) ) ),
inference(distribute,[status(thm)],[108]) ).
cnf(110,plain,
( ~ cp2(X1)
| ~ cp3(X1) ),
inference(split_conjunct,[status(thm)],[109]) ).
cnf(111,plain,
( ~ cp2(X1)
| ~ cp5(X1) ),
inference(split_conjunct,[status(thm)],[109]) ).
cnf(112,plain,
( ~ cp2(X1)
| ~ cp4(X1) ),
inference(split_conjunct,[status(thm)],[109]) ).
fof(113,plain,
! [X3] :
( ~ cp3(X3)
| ( ~ cp4(X3)
& ~ cp5(X3) ) ),
inference(fof_nnf,[status(thm)],[15]) ).
fof(114,plain,
! [X4] :
( ~ cp3(X4)
| ( ~ cp4(X4)
& ~ cp5(X4) ) ),
inference(variable_rename,[status(thm)],[113]) ).
fof(115,plain,
! [X4] :
( ( ~ cp4(X4)
| ~ cp3(X4) )
& ( ~ cp5(X4)
| ~ cp3(X4) ) ),
inference(distribute,[status(thm)],[114]) ).
cnf(116,plain,
( ~ cp3(X1)
| ~ cp5(X1) ),
inference(split_conjunct,[status(thm)],[115]) ).
cnf(117,plain,
( ~ cp3(X1)
| ~ cp4(X1) ),
inference(split_conjunct,[status(thm)],[115]) ).
cnf(136,plain,
( ~ cp4(esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[31,59,theory(equality)]) ).
cnf(137,plain,
( ~ cp2(esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[111,59,theory(equality)]) ).
cnf(138,plain,
( ~ cp3(esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[116,59,theory(equality)]) ).
cnf(139,plain,
( ~ cp1(esk5_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[91,59,theory(equality)]) ).
cnf(140,plain,
( ~ cp4(esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[112,62,theory(equality)]) ).
cnf(143,plain,
( ~ cp4(esk1_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[117,69,theory(equality)]) ).
cnf(144,plain,
( ~ cp2(esk1_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[110,69,theory(equality)]) ).
cnf(147,plain,
( ~ cp4(esk7_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[92,54,theory(equality)]) ).
cnf(148,plain,
( ~ cp2(esk7_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[93,54,theory(equality)]) ).
cnf(149,plain,
( ~ cp3(esk7_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[90,54,theory(equality)]) ).
cnf(153,plain,
( X1 = X2
| X1 = X3
| X1 = X4
| X1 = esk1_1(X5)
| X2 = X3
| X2 = X4
| X2 = esk1_1(X5)
| X3 = X4
| X3 = esk1_1(X5)
| X4 = esk1_1(X5)
| ~ rr(X5,X4)
| ~ rr(X5,X3)
| ~ rr(X5,X2)
| ~ rr(X5,X1)
| ~ cUnsatisfiable(X5) ),
inference(spm,[status(thm)],[71,70,theory(equality)]) ).
cnf(297,plain,
( esk2_1(X1) = esk1_1(X1)
| X2 = esk1_1(X1)
| X3 = esk1_1(X1)
| X4 = esk1_1(X1)
| X2 = esk2_1(X1)
| X3 = esk2_1(X1)
| X3 = X2
| X4 = esk2_1(X1)
| X4 = X2
| X4 = X3
| ~ rr(X1,X2)
| ~ rr(X1,X3)
| ~ rr(X1,X4)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[153,68,theory(equality)]) ).
cnf(306,plain,
( esk1_1(X1) = esk2_1(X1)
| X2 = esk2_1(X1)
| X3 = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| X2 = esk1_1(X1)
| X3 = esk1_1(X1)
| esk4_1(X1) = esk1_1(X1)
| X2 = X3
| X2 = esk4_1(X1)
| X3 = esk4_1(X1)
| ~ rr(X1,X3)
| ~ rr(X1,X2)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[297,63,theory(equality)]) ).
cnf(908,plain,
( esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| X2 = esk4_1(X1)
| esk5_1(X1) = esk1_1(X1)
| X2 = esk1_1(X1)
| esk5_1(X1) = esk2_1(X1)
| X2 = esk2_1(X1)
| X2 = esk5_1(X1)
| ~ rr(X1,X2)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[306,60,theory(equality)]) ).
cnf(1228,plain,
( esk5_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk7_1(X1) = esk5_1(X1)
| esk7_1(X1) = esk2_1(X1)
| esk7_1(X1) = esk1_1(X1)
| esk7_1(X1) = esk4_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[908,55,theory(equality)]) ).
cnf(1254,plain,
( esk7_1(X1) = esk4_1(X1)
| esk7_1(X1) = esk2_1(X1)
| esk7_1(X1) = esk5_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cp3(esk1_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[149,1228,theory(equality)]) ).
cnf(1369,plain,
( esk7_1(X1) = esk4_1(X1)
| esk7_1(X1) = esk2_1(X1)
| esk7_1(X1) = esk5_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1254,69]) ).
cnf(1372,plain,
( cp1(esk5_1(X1))
| esk5_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk7_1(X1) = esk2_1(X1)
| esk7_1(X1) = esk4_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[54,1369,theory(equality)]) ).
cnf(1377,plain,
( esk7_1(X1) = esk4_1(X1)
| esk7_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1372,139]) ).
cnf(1382,plain,
( esk7_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cp2(esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[148,1377,theory(equality)]) ).
cnf(1394,plain,
( esk7_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1382,62]) ).
cnf(1397,plain,
( esk5_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| ~ cp4(esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[147,1394,theory(equality)]) ).
cnf(1410,plain,
( esk5_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk5_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1397,67]) ).
cnf(1413,plain,
( cp3(esk5_1(X1))
| esk1_1(X1) = esk4_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[69,1410,theory(equality)]) ).
cnf(1418,plain,
( esk5_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| esk1_1(X1) = esk4_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1413,138]) ).
cnf(1423,plain,
( esk5_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| ~ cp2(esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[144,1418,theory(equality)]) ).
cnf(1430,plain,
( esk5_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk1_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1423,62]) ).
cnf(1433,plain,
( esk4_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cp4(esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[143,1430,theory(equality)]) ).
cnf(1437,plain,
( esk4_1(X1) = esk2_1(X1)
| esk5_1(X1) = esk4_1(X1)
| esk5_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1433,67]) ).
cnf(1442,plain,
( esk5_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| ~ cp2(esk4_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[137,1437,theory(equality)]) ).
cnf(1458,plain,
( esk5_1(X1) = esk2_1(X1)
| esk4_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1442,62]) ).
cnf(1461,plain,
( esk4_1(X1) = esk2_1(X1)
| ~ cp4(esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[136,1458,theory(equality)]) ).
cnf(1469,plain,
( esk4_1(X1) = esk2_1(X1)
| ~ cUnsatisfiable(X1) ),
inference(csr,[status(thm)],[1461,67]) ).
cnf(1473,plain,
( ~ cp4(esk2_1(X1))
| ~ cUnsatisfiable(X1) ),
inference(spm,[status(thm)],[140,1469,theory(equality)]) ).
cnf(1475,plain,
~ cUnsatisfiable(X1),
inference(csr,[status(thm)],[1473,67]) ).
cnf(1476,plain,
$false,
inference(sr,[status(thm)],[28,1475,theory(equality)]) ).
cnf(1477,plain,
$false,
1476,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/KRS/KRS081+1.p
% --creating new selector for []
% -running prover on /tmp/tmpzSsO5W/sel_KRS081+1.p_1 with time limit 29
% -prover status Unsatisfiable
% Problem KRS081+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/KRS/KRS081+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/KRS/KRS081+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Unsatisfiable
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------