%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV406+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 12:39:19 EST 2010
% Result : Theorem 185.69s
% Output : CNFRefutation 185.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 6
% Syntax : Number of formulae : 80 ( 10 unt; 0 def)
% Number of atoms : 295 ( 32 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 336 ( 121 ~; 149 |; 49 &)
% ( 9 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 4 usr; 2 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-3 aty)
% Number of variables : 218 ( 22 sgn 126 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(17,axiom,
! [X1,X2,X3,X4,X5] :
( pair_in_list(insert_slb(X1,pair(X2,X4)),X3,X5)
<=> ( pair_in_list(X1,X3,X5)
| ( X2 = X3
& X4 = X5 ) ) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',ax23) ).
fof(18,axiom,
! [X1,X2] :
( less_than(X1,X2)
| less_than(X2,X1) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',totality) ).
fof(19,axiom,
! [X1,X2] :
( strictly_less_than(X1,X2)
<=> ( less_than(X1,X2)
& ~ less_than(X2,X1) ) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',stricly_smaller_definition) ).
fof(24,axiom,
! [X1,X2,X3,X4,X5] :
( less_than(X5,X4)
=> ( check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
<=> check_cpq(triple(X1,X2,X3)) ) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',ax37) ).
fof(28,axiom,
! [X1,X2,X3,X4,X5] :
( strictly_less_than(X4,X5)
=> ( check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
<=> ~ $true ) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',ax38) ).
fof(30,conjecture,
! [X1] :
( ! [X2,X3] :
( check_cpq(triple(X2,X1,X3))
<=> ! [X4,X5] :
( pair_in_list(X1,X4,X5)
=> less_than(X5,X4) ) )
=> ! [X6,X7,X8,X9] :
( check_cpq(triple(X6,insert_slb(X1,pair(X8,X9)),X7))
<=> ! [X10,X11] :
( pair_in_list(insert_slb(X1,pair(X8,X9)),X10,X11)
=> less_than(X11,X10) ) ) ),
file('/tmp/tmptK4FIG/sel_SWV406+1.p_4',l42_co) ).
fof(31,negated_conjecture,
~ ! [X1] :
( ! [X2,X3] :
( check_cpq(triple(X2,X1,X3))
<=> ! [X4,X5] :
( pair_in_list(X1,X4,X5)
=> less_than(X5,X4) ) )
=> ! [X6,X7,X8,X9] :
( check_cpq(triple(X6,insert_slb(X1,pair(X8,X9)),X7))
<=> ! [X10,X11] :
( pair_in_list(insert_slb(X1,pair(X8,X9)),X10,X11)
=> less_than(X11,X10) ) ) ),
inference(assume_negation,[status(cth)],[30]) ).
fof(37,plain,
! [X1,X2] :
( strictly_less_than(X1,X2)
<=> ( less_than(X1,X2)
& ~ less_than(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[19,theory(equality)]) ).
fof(83,plain,
! [X1,X2,X3,X4,X5] :
( ( ~ pair_in_list(insert_slb(X1,pair(X2,X4)),X3,X5)
| pair_in_list(X1,X3,X5)
| ( X2 = X3
& X4 = X5 ) )
& ( ( ~ pair_in_list(X1,X3,X5)
& ( X2 != X3
| X4 != X5 ) )
| pair_in_list(insert_slb(X1,pair(X2,X4)),X3,X5) ) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(84,plain,
! [X6,X7,X8,X9,X10] :
( ( ~ pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10)
| pair_in_list(X6,X8,X10)
| ( X7 = X8
& X9 = X10 ) )
& ( ( ~ pair_in_list(X6,X8,X10)
& ( X7 != X8
| X9 != X10 ) )
| pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10) ) ),
inference(variable_rename,[status(thm)],[83]) ).
fof(85,plain,
! [X6,X7,X8,X9,X10] :
( ( X7 = X8
| pair_in_list(X6,X8,X10)
| ~ pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10) )
& ( X9 = X10
| pair_in_list(X6,X8,X10)
| ~ pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10) )
& ( ~ pair_in_list(X6,X8,X10)
| pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10) )
& ( X7 != X8
| X9 != X10
| pair_in_list(insert_slb(X6,pair(X7,X9)),X8,X10) ) ),
inference(distribute,[status(thm)],[84]) ).
cnf(86,plain,
( pair_in_list(insert_slb(X1,pair(X2,X3)),X4,X5)
| X3 != X5
| X2 != X4 ),
inference(split_conjunct,[status(thm)],[85]) ).
cnf(87,plain,
( pair_in_list(insert_slb(X1,pair(X2,X3)),X4,X5)
| ~ pair_in_list(X1,X4,X5) ),
inference(split_conjunct,[status(thm)],[85]) ).
cnf(88,plain,
( pair_in_list(X1,X4,X5)
| X3 = X5
| ~ pair_in_list(insert_slb(X1,pair(X2,X3)),X4,X5) ),
inference(split_conjunct,[status(thm)],[85]) ).
cnf(89,plain,
( pair_in_list(X1,X4,X5)
| X2 = X4
| ~ pair_in_list(insert_slb(X1,pair(X2,X3)),X4,X5) ),
inference(split_conjunct,[status(thm)],[85]) ).
fof(90,plain,
! [X3,X4] :
( less_than(X3,X4)
| less_than(X4,X3) ),
inference(variable_rename,[status(thm)],[18]) ).
cnf(91,plain,
( less_than(X1,X2)
| less_than(X2,X1) ),
inference(split_conjunct,[status(thm)],[90]) ).
fof(92,plain,
! [X1,X2] :
( ( ~ strictly_less_than(X1,X2)
| ( less_than(X1,X2)
& ~ less_than(X2,X1) ) )
& ( ~ less_than(X1,X2)
| less_than(X2,X1)
| strictly_less_than(X1,X2) ) ),
inference(fof_nnf,[status(thm)],[37]) ).
fof(93,plain,
! [X3,X4] :
( ( ~ strictly_less_than(X3,X4)
| ( less_than(X3,X4)
& ~ less_than(X4,X3) ) )
& ( ~ less_than(X3,X4)
| less_than(X4,X3)
| strictly_less_than(X3,X4) ) ),
inference(variable_rename,[status(thm)],[92]) ).
fof(94,plain,
! [X3,X4] :
( ( less_than(X3,X4)
| ~ strictly_less_than(X3,X4) )
& ( ~ less_than(X4,X3)
| ~ strictly_less_than(X3,X4) )
& ( ~ less_than(X3,X4)
| less_than(X4,X3)
| strictly_less_than(X3,X4) ) ),
inference(distribute,[status(thm)],[93]) ).
cnf(95,plain,
( strictly_less_than(X1,X2)
| less_than(X2,X1)
| ~ less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[94]) ).
fof(108,plain,
! [X1,X2,X3,X4,X5] :
( ~ less_than(X5,X4)
| ( ( ~ check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
| check_cpq(triple(X1,X2,X3)) )
& ( ~ check_cpq(triple(X1,X2,X3))
| check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3)) ) ) ),
inference(fof_nnf,[status(thm)],[24]) ).
fof(109,plain,
! [X6,X7,X8,X9,X10] :
( ~ less_than(X10,X9)
| ( ( ~ check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| check_cpq(triple(X6,X7,X8)) )
& ( ~ check_cpq(triple(X6,X7,X8))
| check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8)) ) ) ),
inference(variable_rename,[status(thm)],[108]) ).
fof(110,plain,
! [X6,X7,X8,X9,X10] :
( ( ~ check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| check_cpq(triple(X6,X7,X8))
| ~ less_than(X10,X9) )
& ( ~ check_cpq(triple(X6,X7,X8))
| check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| ~ less_than(X10,X9) ) ),
inference(distribute,[status(thm)],[109]) ).
cnf(111,plain,
( check_cpq(triple(X3,insert_slb(X4,pair(X2,X1)),X5))
| ~ less_than(X1,X2)
| ~ check_cpq(triple(X3,X4,X5)) ),
inference(split_conjunct,[status(thm)],[110]) ).
cnf(112,plain,
( check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ check_cpq(triple(X3,insert_slb(X4,pair(X2,X1)),X5)) ),
inference(split_conjunct,[status(thm)],[110]) ).
fof(121,plain,
! [X1,X2,X3,X4,X5] :
( ~ strictly_less_than(X4,X5)
| ( ( ~ check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
| ~ $true )
& ( $true
| check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3)) ) ) ),
inference(fof_nnf,[status(thm)],[28]) ).
fof(122,plain,
! [X6,X7,X8,X9,X10] :
( ~ strictly_less_than(X9,X10)
| ( ( ~ check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| ~ $true )
& ( $true
| check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8)) ) ) ),
inference(variable_rename,[status(thm)],[121]) ).
fof(123,plain,
! [X6,X7,X8,X9,X10] :
( ( ~ check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| ~ $true
| ~ strictly_less_than(X9,X10) )
& ( $true
| check_cpq(triple(X6,insert_slb(X7,pair(X9,X10)),X8))
| ~ strictly_less_than(X9,X10) ) ),
inference(distribute,[status(thm)],[122]) ).
cnf(125,plain,
( ~ strictly_less_than(X1,X2)
| $false
| ~ check_cpq(triple(X3,insert_slb(X4,pair(X1,X2)),X5)) ),
inference(split_conjunct,[status(thm)],[123]) ).
fof(129,negated_conjecture,
? [X1] :
( ! [X2,X3] :
( ( ~ check_cpq(triple(X2,X1,X3))
| ! [X4,X5] :
( ~ pair_in_list(X1,X4,X5)
| less_than(X5,X4) ) )
& ( ? [X4,X5] :
( pair_in_list(X1,X4,X5)
& ~ less_than(X5,X4) )
| check_cpq(triple(X2,X1,X3)) ) )
& ? [X6,X7,X8,X9] :
( ( ~ check_cpq(triple(X6,insert_slb(X1,pair(X8,X9)),X7))
| ? [X10,X11] :
( pair_in_list(insert_slb(X1,pair(X8,X9)),X10,X11)
& ~ less_than(X11,X10) ) )
& ( check_cpq(triple(X6,insert_slb(X1,pair(X8,X9)),X7))
| ! [X10,X11] :
( ~ pair_in_list(insert_slb(X1,pair(X8,X9)),X10,X11)
| less_than(X11,X10) ) ) ) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(130,negated_conjecture,
? [X12] :
( ! [X13,X14] :
( ( ~ check_cpq(triple(X13,X12,X14))
| ! [X15,X16] :
( ~ pair_in_list(X12,X15,X16)
| less_than(X16,X15) ) )
& ( ? [X17,X18] :
( pair_in_list(X12,X17,X18)
& ~ less_than(X18,X17) )
| check_cpq(triple(X13,X12,X14)) ) )
& ? [X19,X20,X21,X22] :
( ( ~ check_cpq(triple(X19,insert_slb(X12,pair(X21,X22)),X20))
| ? [X23,X24] :
( pair_in_list(insert_slb(X12,pair(X21,X22)),X23,X24)
& ~ less_than(X24,X23) ) )
& ( check_cpq(triple(X19,insert_slb(X12,pair(X21,X22)),X20))
| ! [X25,X26] :
( ~ pair_in_list(insert_slb(X12,pair(X21,X22)),X25,X26)
| less_than(X26,X25) ) ) ) ),
inference(variable_rename,[status(thm)],[129]) ).
fof(131,negated_conjecture,
( ! [X13,X14] :
( ( ~ check_cpq(triple(X13,esk1_0,X14))
| ! [X15,X16] :
( ~ pair_in_list(esk1_0,X15,X16)
| less_than(X16,X15) ) )
& ( ( pair_in_list(esk1_0,esk2_2(X13,X14),esk3_2(X13,X14))
& ~ less_than(esk3_2(X13,X14),esk2_2(X13,X14)) )
| check_cpq(triple(X13,esk1_0,X14)) ) )
& ( ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| ( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
& ~ less_than(esk9_0,esk8_0) ) )
& ( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| ! [X25,X26] :
( ~ pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),X25,X26)
| less_than(X26,X25) ) ) ),
inference(skolemize,[status(esa)],[130]) ).
fof(132,negated_conjecture,
! [X13,X14,X15,X16,X25,X26] :
( ( ~ pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),X25,X26)
| less_than(X26,X25)
| check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0)) )
& ( ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| ( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
& ~ less_than(esk9_0,esk8_0) ) )
& ( ~ pair_in_list(esk1_0,X15,X16)
| less_than(X16,X15)
| ~ check_cpq(triple(X13,esk1_0,X14)) )
& ( ( pair_in_list(esk1_0,esk2_2(X13,X14),esk3_2(X13,X14))
& ~ less_than(esk3_2(X13,X14),esk2_2(X13,X14)) )
| check_cpq(triple(X13,esk1_0,X14)) ) ),
inference(shift_quantors,[status(thm)],[131]) ).
fof(133,negated_conjecture,
! [X13,X14,X15,X16,X25,X26] :
( ( ~ pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),X25,X26)
| less_than(X26,X25)
| check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0)) )
& ( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0)) )
& ( ~ less_than(esk9_0,esk8_0)
| ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0)) )
& ( ~ pair_in_list(esk1_0,X15,X16)
| less_than(X16,X15)
| ~ check_cpq(triple(X13,esk1_0,X14)) )
& ( pair_in_list(esk1_0,esk2_2(X13,X14),esk3_2(X13,X14))
| check_cpq(triple(X13,esk1_0,X14)) )
& ( ~ less_than(esk3_2(X13,X14),esk2_2(X13,X14))
| check_cpq(triple(X13,esk1_0,X14)) ) ),
inference(distribute,[status(thm)],[132]) ).
cnf(134,negated_conjecture,
( check_cpq(triple(X1,esk1_0,X2))
| ~ less_than(esk3_2(X1,X2),esk2_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(135,negated_conjecture,
( check_cpq(triple(X1,esk1_0,X2))
| pair_in_list(esk1_0,esk2_2(X1,X2),esk3_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(136,negated_conjecture,
( less_than(X3,X4)
| ~ check_cpq(triple(X1,esk1_0,X2))
| ~ pair_in_list(esk1_0,X4,X3) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(137,negated_conjecture,
( ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| ~ less_than(esk9_0,esk8_0) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(138,negated_conjecture,
( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0)) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(139,negated_conjecture,
( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| less_than(X1,X2)
| ~ pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),X2,X1) ),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(148,plain,
( strictly_less_than(X1,X2)
| less_than(X2,X1) ),
inference(csr,[status(thm)],[95,91]) ).
cnf(157,plain,
( pair_in_list(insert_slb(X1,pair(X2,X3)),X4,X3)
| X2 != X4 ),
inference(er,[status(thm)],[86,theory(equality)]) ).
cnf(158,plain,
pair_in_list(insert_slb(X1,pair(X2,X3)),X2,X3),
inference(er,[status(thm)],[157,theory(equality)]) ).
cnf(160,negated_conjecture,
( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| less_than(X1,X2)
| ~ pair_in_list(esk1_0,X2,X1) ),
inference(spm,[status(thm)],[139,87,theory(equality)]) ).
cnf(162,negated_conjecture,
( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| ~ less_than(esk7_0,esk6_0) ),
inference(spm,[status(thm)],[138,111,theory(equality)]) ).
cnf(163,negated_conjecture,
( ~ less_than(esk9_0,esk8_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| ~ less_than(esk7_0,esk6_0) ),
inference(spm,[status(thm)],[137,111,theory(equality)]) ).
cnf(263,negated_conjecture,
( esk7_0 = esk9_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| ~ less_than(esk7_0,esk6_0) ),
inference(spm,[status(thm)],[88,162,theory(equality)]) ).
cnf(266,negated_conjecture,
( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| less_than(esk7_0,esk6_0) ),
inference(spm,[status(thm)],[139,158,theory(equality)]) ).
cnf(282,negated_conjecture,
( less_than(esk7_0,esk6_0)
| ~ strictly_less_than(esk6_0,esk7_0) ),
inference(spm,[status(thm)],[125,266,theory(equality)]) ).
cnf(291,negated_conjecture,
less_than(esk7_0,esk6_0),
inference(csr,[status(thm)],[282,148]) ).
cnf(297,negated_conjecture,
( esk9_0 = esk7_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| $false ),
inference(rw,[status(thm)],[263,291,theory(equality)]) ).
cnf(298,negated_conjecture,
( esk9_0 = esk7_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0)) ),
inference(cn,[status(thm)],[297,theory(equality)]) ).
cnf(299,negated_conjecture,
( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| $false ),
inference(rw,[status(thm)],[162,291,theory(equality)]) ).
cnf(300,negated_conjecture,
( pair_in_list(insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0)) ),
inference(cn,[status(thm)],[299,theory(equality)]) ).
cnf(301,negated_conjecture,
( ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| ~ less_than(esk9_0,esk8_0)
| $false ),
inference(rw,[status(thm)],[163,291,theory(equality)]) ).
cnf(302,negated_conjecture,
( ~ check_cpq(triple(esk4_0,esk1_0,esk5_0))
| ~ less_than(esk9_0,esk8_0) ),
inference(cn,[status(thm)],[301,theory(equality)]) ).
cnf(346,negated_conjecture,
( esk6_0 = esk8_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| ~ check_cpq(triple(esk4_0,esk1_0,esk5_0)) ),
inference(spm,[status(thm)],[89,300,theory(equality)]) ).
cnf(440,negated_conjecture,
( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| less_than(esk3_2(X1,X2),esk2_2(X1,X2))
| check_cpq(triple(X1,esk1_0,X2)) ),
inference(spm,[status(thm)],[160,135,theory(equality)]) ).
cnf(902,negated_conjecture,
( check_cpq(triple(esk4_0,insert_slb(esk1_0,pair(esk6_0,esk7_0)),esk5_0))
| check_cpq(triple(X1,esk1_0,X2)) ),
inference(csr,[status(thm)],[440,134]) ).
cnf(905,negated_conjecture,
( check_cpq(triple(X1,esk1_0,X2))
| ~ less_than(esk9_0,esk8_0) ),
inference(spm,[status(thm)],[137,902,theory(equality)]) ).
cnf(907,negated_conjecture,
( check_cpq(triple(esk4_0,esk1_0,esk5_0))
| check_cpq(triple(X1,esk1_0,X2))
| ~ less_than(esk7_0,esk6_0) ),
inference(spm,[status(thm)],[112,902,theory(equality)]) ).
cnf(908,negated_conjecture,
( check_cpq(triple(esk4_0,esk1_0,esk5_0))
| check_cpq(triple(X1,esk1_0,X2))
| $false ),
inference(rw,[status(thm)],[907,291,theory(equality)]) ).
cnf(909,negated_conjecture,
( check_cpq(triple(esk4_0,esk1_0,esk5_0))
| check_cpq(triple(X1,esk1_0,X2)) ),
inference(cn,[status(thm)],[908,theory(equality)]) ).
cnf(912,negated_conjecture,
~ less_than(esk9_0,esk8_0),
inference(spm,[status(thm)],[302,905,theory(equality)]) ).
cnf(1791,negated_conjecture,
check_cpq(triple(esk4_0,esk1_0,esk5_0)),
inference(ef,[status(thm)],[909,theory(equality)]) ).
cnf(1798,negated_conjecture,
( less_than(X1,X2)
| ~ pair_in_list(esk1_0,X2,X1) ),
inference(spm,[status(thm)],[136,1791,theory(equality)]) ).
cnf(1804,negated_conjecture,
( esk8_0 = esk6_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| $false ),
inference(rw,[status(thm)],[346,1791,theory(equality)]) ).
cnf(1805,negated_conjecture,
( esk8_0 = esk6_0
| pair_in_list(esk1_0,esk8_0,esk9_0) ),
inference(cn,[status(thm)],[1804,theory(equality)]) ).
cnf(1810,negated_conjecture,
( esk9_0 = esk7_0
| pair_in_list(esk1_0,esk8_0,esk9_0)
| $false ),
inference(rw,[status(thm)],[298,1791,theory(equality)]) ).
cnf(1811,negated_conjecture,
( esk9_0 = esk7_0
| pair_in_list(esk1_0,esk8_0,esk9_0) ),
inference(cn,[status(thm)],[1810,theory(equality)]) ).
cnf(1819,negated_conjecture,
( less_than(esk9_0,esk8_0)
| esk8_0 = esk6_0 ),
inference(spm,[status(thm)],[1798,1805,theory(equality)]) ).
cnf(1821,negated_conjecture,
esk8_0 = esk6_0,
inference(sr,[status(thm)],[1819,912,theory(equality)]) ).
cnf(1824,negated_conjecture,
~ less_than(esk9_0,esk6_0),
inference(rw,[status(thm)],[912,1821,theory(equality)]) ).
cnf(1825,negated_conjecture,
( esk9_0 = esk7_0
| pair_in_list(esk1_0,esk6_0,esk9_0) ),
inference(rw,[status(thm)],[1811,1821,theory(equality)]) ).
cnf(1933,negated_conjecture,
( less_than(esk9_0,esk6_0)
| esk9_0 = esk7_0 ),
inference(spm,[status(thm)],[1798,1825,theory(equality)]) ).
cnf(1934,negated_conjecture,
esk9_0 = esk7_0,
inference(sr,[status(thm)],[1933,1824,theory(equality)]) ).
cnf(1937,negated_conjecture,
$false,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[1824,1934,theory(equality)]),291,theory(equality)]) ).
cnf(1938,negated_conjecture,
$false,
inference(cn,[status(thm)],[1937,theory(equality)]) ).
cnf(1939,negated_conjecture,
$false,
1938,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV406+1.p
% --creating new selector for [SWV007+0.ax, SWV007+2.ax, SWV007+3.ax]
% eprover: CPU time limit exceeded, terminating
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmptK4FIG/sel_SWV406+1.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmptK4FIG/sel_SWV406+1.p_2 with time limit 81
% -prover status ResourceOut
% --creating new selector for [SWV007+0.ax, SWV007+2.ax, SWV007+3.ax]
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmptK4FIG/sel_SWV406+1.p_3 with time limit 75
% -prover status ResourceOut
% --creating new selector for [SWV007+0.ax, SWV007+2.ax, SWV007+3.ax]
% -running prover on /tmp/tmptK4FIG/sel_SWV406+1.p_4 with time limit 56
% -prover status Theorem
% Problem SWV406+1.p solved in phase 3.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV406+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV406+1.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
%
%------------------------------------------------------------------------------