%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SYO377^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 11:08:09 AM UTC 2026
% Result : Theorem 90.66s 15.38s
% Output : CNFRefutation 90.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 1
% Syntax : Number of formulae : 174 ( 43 unt; 0 typ; 0 def)
% Number of atoms : 1237 ( 480 equ; 0 cnn)
% Maximal formula atoms : 4 ( 7 avg)
% Number of connectives : 953 ( 223 ~; 408 |; 18 &; 284 @)
% ( 4 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 125 ( 125 >; 0 *; 0 +; 0 <<)
% Number of symbols : 6 ( 3 usr; 4 con; 0-2 aty)
% Number of variables : 307 ( 0 ^; 307 !; 0 ?; 307 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $o ).
thf(tp_b,type,
b: $o ).
thf(tp_sK1_Xp,type,
sK1_Xp: $o > $o ).
thf(1,conjecture,
( ! [Xx: $o,Xy: $o] :
( ( Xx
<=> Xy )
=> ! [Xq: $o > $o] :
( ( Xq @ Xx )
=> ( Xq @ Xy ) ) )
=> ! [Xp: $o > $o] :
( ( ( Xp @ a )
& ( Xp @ b ) )
=> ( Xp
@ ( a
& b ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cEXT_IMP_EMB2) ).
thf(2,negated_conjecture,
( ( ! [Xx: $o,Xy: $o] :
( ( Xx
<=> Xy )
=> ! [Xq: $o > $o] :
( ( Xq @ Xx )
=> ( Xq @ Xy ) ) )
=> ! [Xp: $o > $o] :
( ( ( Xp @ a )
& ( Xp @ b ) )
=> ( Xp
@ ( a
& b ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( ! [Xx: $o,Xy: $o] :
( ( Xx
<=> Xy )
=> ! [Xq: $o > $o] :
( ( Xq @ Xx )
=> ( Xq @ Xy ) ) )
=> ! [Xp: $o > $o] :
( ( ( Xp @ a )
& ( Xp @ b ) )
=> ( Xp
@ ( a
& b ) ) ) )
= $false ),
inference(unfold_def,[status(thm)],[2]) ).
thf(4,plain,
( ( ! [Xx: $o,Xy: $o] :
( ( Xx
<=> Xy )
=> ! [Xq: $o > $o] :
( ( Xq @ Xx )
=> ( Xq @ Xy ) ) ) )
= $true ),
inference(standard_cnf,[status(thm)],[3]) ).
thf(5,plain,
( ( ! [Xp: $o > $o] :
( ( ( Xp @ a )
& ( Xp @ b ) )
=> ( Xp
@ ( a
& b ) ) ) )
= $false ),
inference(standard_cnf,[status(thm)],[3]) ).
thf(6,plain,
( ( ~ ! [Xp: $o > $o] :
( ( ( Xp @ a )
& ( Xp @ b ) )
=> ( Xp
@ ( a
& b ) ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[5]) ).
thf(7,plain,
( ( ( sK1_Xp @ a )
& ( sK1_Xp @ b )
& ~ ( sK1_Xp
@ ( a
& b ) ) )
= $true ),
inference(extcnf_combined,[status(esa)],[6]) ).
thf(8,plain,
( ( ! [Xx: $o,Xy: $o] :
( ~ Xx
| ~ Xy
| ! [Xq: $o > $o] :
( ~ ( Xq @ Xx )
| ( Xq @ Xy ) ) )
& ! [Xx: $o,Xy: $o] :
( Xx
| Xy
| ! [Xq: $o > $o] :
( ~ ( Xq @ Xx )
| ( Xq @ Xy ) ) ) )
= $true ),
inference(extcnf_combined,[status(esa)],[4]) ).
thf(9,plain,
( ( ! [Xx: $o,Xy: $o] :
( ~ Xx
| ~ Xy
| ! [Xq: $o > $o] :
( ~ ( Xq @ Xx )
| ( Xq @ Xy ) ) )
& ! [Xx: $o,Xy: $o] :
( Xx
| Xy
| ! [Xq: $o > $o] :
( ~ ( Xq @ Xx )
| ( Xq @ Xy ) ) ) )
= $true ),
inference(copy,[status(thm)],[8]) ).
thf(10,plain,
( ( ( sK1_Xp @ a )
& ( sK1_Xp @ b )
& ~ ( sK1_Xp
@ ( a
& b ) ) )
= $true ),
inference(copy,[status(thm)],[7]) ).
thf(11,plain,
( ( ~ ( ~ ! [SX0: $o,SX1: $o] :
( ~ SX0
| ~ SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) )
| ~ ! [SX0: $o,SX1: $o] :
( SX0
| SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[9]) ).
thf(12,plain,
( ( ~ ( ~ ~ ( ~ ( sK1_Xp @ a )
| ~ ( sK1_Xp @ b ) )
| ~ ~ ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[10]) ).
thf(13,plain,
( ( ~ ! [SX0: $o,SX1: $o] :
( ~ SX0
| ~ SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) )
| ~ ! [SX0: $o,SX1: $o] :
( SX0
| SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[11]) ).
thf(14,plain,
( ( ~ ~ ( ~ ( sK1_Xp @ a )
| ~ ( sK1_Xp @ b ) )
| ~ ~ ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[12]) ).
thf(15,plain,
( ( ~ ! [SX0: $o,SX1: $o] :
( ~ SX0
| ~ SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[13]) ).
thf(16,plain,
( ( ~ ! [SX0: $o,SX1: $o] :
( SX0
| SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[13]) ).
thf(17,plain,
( ( ~ ~ ( ~ ( sK1_Xp @ a )
| ~ ( sK1_Xp @ b ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[14]) ).
thf(18,plain,
( ( ~ ~ ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[14]) ).
thf(19,plain,
( ( ! [SX0: $o,SX1: $o] :
( ~ SX0
| ~ SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[15]) ).
thf(20,plain,
( ( ! [SX0: $o,SX1: $o] :
( SX0
| SX1
| ! [SX2: $o > $o] :
( ~ ( SX2 @ SX0 )
| ( SX2 @ SX1 ) ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[16]) ).
thf(21,plain,
( ( ~ ( ~ ( sK1_Xp @ a )
| ~ ( sK1_Xp @ b ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[17]) ).
thf(22,plain,
( ( ~ ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[18]) ).
thf(23,plain,
! [SV1: $o] :
( ( ! [SY4: $o] :
( ~ SV1
| ~ SY4
| ! [SY5: $o > $o] :
( ~ ( SY5 @ SV1 )
| ( SY5 @ SY4 ) ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[19]) ).
thf(24,plain,
( ( ! [SX0: $o] :
( ~ $true
| ~ SX0
| ! [SX1: $o > $o] :
( ~ ( SX1 @ $true )
| ( SX1 @ SX0 ) ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[19]) ).
thf(26,plain,
! [SV2: $o] :
( ( ! [SY6: $o] :
( SV2
| SY6
| ! [SY7: $o > $o] :
( ~ ( SY7 @ SV2 )
| ( SY7 @ SY6 ) ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[20]) ).
thf(28,plain,
( ( ! [SX0: $o] :
( $false
| SX0
| ! [SX1: $o > $o] :
( ~ ( SX1 @ $false )
| ( SX1 @ SX0 ) ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[20]) ).
thf(29,plain,
( ( ~ ( sK1_Xp @ a )
| ~ ( sK1_Xp @ b ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[21]) ).
thf(30,plain,
( ( sK1_Xp
@ ~ ( ~ a
| ~ b ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[22]) ).
thf(31,plain,
! [SV3: $o,SV1: $o] :
( ( ~ SV1
| ~ SV3
| ! [SY8: $o > $o] :
( ~ ( SY8 @ SV1 )
| ( SY8 @ SV3 ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[23]) ).
thf(32,plain,
! [SV1: $o] :
( ( ~ SV1
| ~ $true
| ! [SX0: $o > $o] :
( ~ ( SX0 @ SV1 )
| ( SX0 @ $true ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[23]) ).
thf(34,plain,
! [SV4: $o] :
( ( ~ $true
| ~ SV4
| ! [SY9: $o > $o] :
( ~ ( SY9 @ $true )
| ( SY9 @ SV4 ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[24]) ).
thf(40,plain,
! [SV6: $o,SV2: $o] :
( ( SV2
| SV6
| ! [SY11: $o > $o] :
( ~ ( SY11 @ SV2 )
| ( SY11 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[26]) ).
thf(42,plain,
! [SV2: $o] :
( ( SV2
| $false
| ! [SX0: $o > $o] :
( ~ ( SX0 @ SV2 )
| ( SX0 @ $false ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[26]) ).
thf(46,plain,
! [SV8: $o] :
( ( $false
| SV8
| ! [SY13: $o > $o] :
( ~ ( SY13 @ $false )
| ( SY13 @ SV8 ) ) )
= $true ),
inference(extcnf_forall_special_pos,[status(thm)],[28]) ).
thf(49,plain,
( ( ~ ( sK1_Xp @ a ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[29]) ).
thf(50,plain,
( ( ~ ( sK1_Xp @ b ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[29]) ).
thf(51,plain,
! [SV3: $o,SV1: $o] :
( ( ( ~ SV1
| ~ SV3 )
= $true )
| ( ( ! [SY8: $o > $o] :
( ~ ( SY8 @ SV1 )
| ( SY8 @ SV3 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[31]) ).
thf(52,plain,
! [SV1: $o] :
( ( ( ~ SV1
| ~ $true )
= $true )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV1 )
| ( SX0 @ $true ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[32]) ).
thf(54,plain,
! [SV4: $o] :
( ( ( ~ $true
| ~ SV4 )
= $true )
| ( ( ! [SY9: $o > $o] :
( ~ ( SY9 @ $true )
| ( SY9 @ SV4 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[34]) ).
thf(60,plain,
! [SV6: $o,SV2: $o] :
( ( ( SV2
| SV6 )
= $true )
| ( ( ! [SY11: $o > $o] :
( ~ ( SY11 @ SV2 )
| ( SY11 @ SV6 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[40]) ).
thf(62,plain,
! [SV2: $o] :
( ( ( SV2
| $false )
= $true )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV2 )
| ( SX0 @ $false ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[42]) ).
thf(66,plain,
! [SV8: $o] :
( ( ( $false
| SV8 )
= $true )
| ( ( ! [SY13: $o > $o] :
( ~ ( SY13 @ $false )
| ( SY13 @ SV8 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[46]) ).
thf(69,plain,
( ( sK1_Xp @ a )
= $true ),
inference(extcnf_not_neg,[status(thm)],[49]) ).
thf(70,plain,
( ( sK1_Xp @ b )
= $true ),
inference(extcnf_not_neg,[status(thm)],[50]) ).
thf(71,plain,
! [SV3: $o,SV1: $o] :
( ( ( ~ SV1 ) = $true )
| ( ( ~ SV3 ) = $true )
| ( ( ! [SY8: $o > $o] :
( ~ ( SY8 @ SV1 )
| ( SY8 @ SV3 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[51]) ).
thf(72,plain,
! [SV1: $o] :
( ( ( ~ SV1 ) = $true )
| ( ( ~ $true ) = $true )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV1 )
| ( SX0 @ $true ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[52]) ).
thf(74,plain,
! [SV4: $o] :
( ( ( ~ $true ) = $true )
| ( ( ~ SV4 ) = $true )
| ( ( ! [SY9: $o > $o] :
( ~ ( SY9 @ $true )
| ( SY9 @ SV4 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[54]) ).
thf(80,plain,
! [SV6: $o,SV2: $o] :
( ( SV2 = $true )
| ( SV6 = $true )
| ( ( ! [SY11: $o > $o] :
( ~ ( SY11 @ SV2 )
| ( SY11 @ SV6 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[60]) ).
thf(82,plain,
! [SV2: $o] :
( ( SV2 = $true )
| ( $false = $true )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV2 )
| ( SX0 @ $false ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[62]) ).
thf(86,plain,
! [SV8: $o] :
( ( $false = $true )
| ( SV8 = $true )
| ( ( ! [SY13: $o > $o] :
( ~ ( SY13 @ $false )
| ( SY13 @ SV8 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[66]) ).
thf(89,plain,
! [SV3: $o,SV1: $o] :
( ( SV1 = $false )
| ( ( ~ SV3 ) = $true )
| ( ( ! [SY8: $o > $o] :
( ~ ( SY8 @ SV1 )
| ( SY8 @ SV3 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[71]) ).
thf(90,plain,
! [SV1: $o] :
( ( SV1 = $false )
| ( ( ~ $true ) = $true )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV1 )
| ( SX0 @ $true ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[72]) ).
thf(92,plain,
! [SV4: $o] :
( ( $true = $false )
| ( ( ~ SV4 ) = $true )
| ( ( ! [SY9: $o > $o] :
( ~ ( SY9 @ $true )
| ( SY9 @ SV4 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[74]) ).
thf(98,plain,
! [SV6: $o,SV2: $o,SV9: $o > $o] :
( ( ( ~ ( SV9 @ SV2 )
| ( SV9 @ SV6 ) )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(extcnf_forall_special_pos,[status(thm)],[80]) ).
thf(108,plain,
! [SV2: $o,SV13: $o > $o] :
( ( ( ~ ( SV13 @ SV2 )
| ( SV13 @ $false ) )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(extcnf_forall_special_pos,[status(thm)],[82]) ).
thf(128,plain,
! [SV8: $o,SV21: $o > $o] :
( ( ( ~ ( SV21 @ $false )
| ( SV21 @ SV8 ) )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(extcnf_forall_special_pos,[status(thm)],[86]) ).
thf(143,plain,
! [SV1: $o,SV3: $o] :
( ( SV3 = $false )
| ( SV1 = $false )
| ( ( ! [SY8: $o > $o] :
( ~ ( SY8 @ SV1 )
| ( SY8 @ SV3 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[89]) ).
thf(144,plain,
! [SV1: $o] :
( ( $true = $false )
| ( SV1 = $false )
| ( ( ! [SX0: $o > $o] :
( ~ ( SX0 @ SV1 )
| ( SX0 @ $true ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[90]) ).
thf(146,plain,
! [SV4: $o] :
( ( SV4 = $false )
| ( $true = $false )
| ( ( ! [SY9: $o > $o] :
( ~ ( SY9 @ $true )
| ( SY9 @ SV4 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[92]) ).
thf(152,plain,
! [SV6: $o,SV2: $o,SV9: $o > $o] :
( ( ( ~ ( SV9 @ SV2 ) )
= $true )
| ( ( SV9 @ SV6 )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(extcnf_or_pos,[status(thm)],[98]) ).
thf(162,plain,
! [SV2: $o,SV13: $o > $o] :
( ( ( ~ ( SV13 @ SV2 ) )
= $true )
| ( ( SV13 @ $false )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(extcnf_or_pos,[status(thm)],[108]) ).
thf(182,plain,
! [SV8: $o,SV21: $o > $o] :
( ( ( ~ ( SV21 @ $false ) )
= $true )
| ( ( SV21 @ SV8 )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(extcnf_or_pos,[status(thm)],[128]) ).
thf(197,plain,
! [SV3: $o,SV1: $o,SV27: $o > $o] :
( ( ( ~ ( SV27 @ SV1 )
| ( SV27 @ SV3 ) )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(extcnf_forall_special_pos,[status(thm)],[143]) ).
thf(202,plain,
! [SV1: $o,SV29: $o > $o] :
( ( ( ~ ( SV29 @ SV1 )
| ( SV29 @ $true ) )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(extcnf_forall_special_pos,[status(thm)],[144]) ).
thf(212,plain,
! [SV4: $o,SV33: $o > $o] :
( ( ( ~ ( SV33 @ $true )
| ( SV33 @ SV4 ) )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(extcnf_forall_special_pos,[status(thm)],[146]) ).
thf(242,plain,
! [SV6: $o,SV2: $o,SV9: $o > $o] :
( ( ( SV9 @ SV2 )
= $false )
| ( ( SV9 @ SV6 )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_pos,[status(thm)],[152]) ).
thf(252,plain,
! [SV2: $o,SV13: $o > $o] :
( ( ( SV13 @ SV2 )
= $false )
| ( ( SV13 @ $false )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_pos,[status(thm)],[162]) ).
thf(272,plain,
! [SV8: $o,SV21: $o > $o] :
( ( ( SV21 @ $false )
= $false )
| ( ( SV21 @ SV8 )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(extcnf_not_pos,[status(thm)],[182]) ).
thf(287,plain,
! [SV3: $o,SV1: $o,SV27: $o > $o] :
( ( ( ~ ( SV27 @ SV1 ) )
= $true )
| ( ( SV27 @ SV3 )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(extcnf_or_pos,[status(thm)],[197]) ).
thf(292,plain,
! [SV1: $o,SV29: $o > $o] :
( ( ( ~ ( SV29 @ SV1 ) )
= $true )
| ( ( SV29 @ $true )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(extcnf_or_pos,[status(thm)],[202]) ).
thf(302,plain,
! [SV4: $o,SV33: $o > $o] :
( ( ( ~ ( SV33 @ $true ) )
= $true )
| ( ( SV33 @ SV4 )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(extcnf_or_pos,[status(thm)],[212]) ).
thf(341,plain,
! [SV3: $o,SV1: $o,SV27: $o > $o] :
( ( ( SV27 @ SV1 )
= $false )
| ( ( SV27 @ SV3 )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(extcnf_not_pos,[status(thm)],[287]) ).
thf(346,plain,
! [SV1: $o,SV29: $o > $o] :
( ( ( SV29 @ SV1 )
= $false )
| ( ( SV29 @ $true )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(extcnf_not_pos,[status(thm)],[292]) ).
thf(356,plain,
! [SV4: $o,SV33: $o > $o] :
( ( ( SV33 @ $true )
= $false )
| ( ( SV33 @ SV4 )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(extcnf_not_pos,[status(thm)],[302]) ).
thf(413,plain,
! [SV6: $o,SV2: $o] :
( ( ( SV2 = SV2 )
= $false )
| ( ( SV6 = SV2 )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(replace_leibnizEQ,[status(thm)],[242:[bind(SV9,$thf( ^ [SV45: $o] : ( SV45 = SV2 ) ))]]) ).
thf(414,plain,
! [SV6: $o,SV2: $o] :
( ( ( SV6 = SV2 )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[413]) ).
thf(416,plain,
! [SV2: $o] :
( ( ( SV2 = SV2 )
= $false )
| ( ( $false = SV2 )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(replace_leibnizEQ,[status(thm)],[252:[bind(SV13,$thf( ^ [SV47: $o] : ( SV47 = SV2 ) ))]]) ).
thf(417,plain,
! [SV2: $o] :
( ( ( $false = SV2 )
= $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[416]) ).
thf(421,plain,
! [SV8: $o] :
( ( ( $false = $false )
= $false )
| ( ( SV8 = $false )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(replace_leibnizEQ,[status(thm)],[272:[bind(SV21,$thf( ^ [SV51: $o] : ( SV51 = $false ) ))]]) ).
thf(422,plain,
! [SV8: $o] :
( ( ( SV8 = $false )
= $true )
| ( SV8 = $true ) ),
inference(sim,[status(thm)],[421]) ).
thf(425,plain,
! [SV3: $o,SV1: $o] :
( ( ( SV1 = SV1 )
= $false )
| ( ( SV3 = SV1 )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(replace_leibnizEQ,[status(thm)],[341:[bind(SV27,$thf( ^ [SV54: $o] : ( SV54 = SV1 ) ))]]) ).
thf(426,plain,
! [SV3: $o,SV1: $o] :
( ( ( SV3 = SV1 )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(sim,[status(thm)],[425]) ).
thf(427,plain,
! [SV1: $o] :
( ( ( SV1 = SV1 )
= $false )
| ( ( $true = SV1 )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(replace_leibnizEQ,[status(thm)],[346:[bind(SV29,$thf( ^ [SV55: $o] : ( SV55 = SV1 ) ))]]) ).
thf(428,plain,
! [SV1: $o] :
( ( ( $true = SV1 )
= $true )
| ( SV1 = $false ) ),
inference(sim,[status(thm)],[427]) ).
thf(430,plain,
! [SV4: $o] :
( ( ( $true = $true )
= $false )
| ( ( SV4 = $true )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(replace_leibnizEQ,[status(thm)],[356:[bind(SV33,$thf( ^ [SV57: $o] : ( SV57 = $true ) ))]]) ).
thf(431,plain,
! [SV4: $o] :
( ( ( SV4 = $true )
= $true )
| ( SV4 = $false ) ),
inference(sim,[status(thm)],[430]) ).
thf(438,plain,
! [SV6: $o,SV9: $o > $o] :
( ( ( SV9 @ $false )
= $false )
| ( ( SV9 @ SV6 )
= $true )
| ( SV6 = $true )
| ( $false = $true ) ),
inference(prim_subst,[status(thm)],[242:[bind(SV2,$thf( $false ))]]) ).
thf(439,plain,
! [SV6: $o,SV171: $o,SV9: $o > $o] :
( ( ( SV9 @ ~ SV171 )
= $false )
| ( ( SV9 @ SV6 )
= $true )
| ( SV6 = $true )
| ( ( ~ SV171 ) = $true ) ),
inference(prim_subst,[status(thm)],[242:[bind(SV2,$thf( ~ ( SV171 ) ))]]) ).
thf(441,plain,
! [SV2: $o,SV9: $o > $o] :
( ( ( SV9 @ SV2 )
= $false )
| ( ( SV9 @ $false )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(prim_subst,[status(thm)],[242:[bind(SV6,$thf( $false ))]]) ).
thf(442,plain,
! [SV172: $o,SV2: $o,SV9: $o > $o] :
( ( ( SV9 @ SV2 )
= $false )
| ( ( SV9 @ ~ SV172 )
= $true )
| ( ( ~ SV172 ) = $true )
| ( SV2 = $true ) ),
inference(prim_subst,[status(thm)],[242:[bind(SV6,$thf( ~ ( SV172 ) ))]]) ).
thf(445,plain,
! [SV6: $o,SV2: $o,SV176: $o > $o] :
( ( ( ~ ( SV176 @ SV2 ) )
= $false )
| ( ( ~ ( SV176 @ SV6 ) )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(prim_subst,[status(thm)],[242:[bind(SV9,$thf( ^ [SV175: $o] : ~ ( SV176 @ SV175 ) ))]]) ).
thf(491,plain,
! [SV2: $o,SV162: $o > $o] :
( ( ( ~ ( SV162 @ SV2 ) )
= $false )
| ( ( ~ ( SV162 @ $false ) )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(prim_subst,[status(thm)],[252:[bind(SV13,$thf( ^ [SV161: $o] : ~ ( SV162 @ SV161 ) ))]]) ).
thf(496,plain,
! [SV171: $o,SV13: $o > $o] :
( ( ( SV13 @ ~ SV171 )
= $false )
| ( ( SV13 @ $false )
= $true )
| ( $false = $true )
| ( ( ~ SV171 ) = $true ) ),
inference(prim_subst,[status(thm)],[252:[bind(SV2,$thf( ~ ( SV171 ) ))]]) ).
thf(538,plain,
! [SV133: $o,SV21: $o > $o] :
( ( ( SV21 @ $false )
= $false )
| ( ( SV21 @ ~ SV133 )
= $true )
| ( ( ~ SV133 ) = $true )
| ( $false = $true ) ),
inference(prim_subst,[status(thm)],[272:[bind(SV8,$thf( ~ ( SV133 ) ))]]) ).
thf(541,plain,
! [SV8: $o,SV137: $o > $o] :
( ( ( ~ ( SV137 @ $false ) )
= $false )
| ( ( ~ ( SV137 @ SV8 ) )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(prim_subst,[status(thm)],[272:[bind(SV21,$thf( ^ [SV136: $o] : ~ ( SV137 @ SV136 ) ))]]) ).
thf(566,plain,
! [SV1: $o,SV27: $o > $o] :
( ( ( SV27 @ SV1 )
= $false )
| ( ( SV27 @ $true )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(prim_subst,[status(thm)],[341:[bind(SV3,$thf( $true ))]]) ).
thf(568,plain,
! [SV113: $o,SV1: $o,SV27: $o > $o] :
( ( ( SV27 @ SV1 )
= $false )
| ( ( SV27 @ ~ SV113 )
= $true )
| ( SV1 = $false )
| ( ( ~ SV113 ) = $false ) ),
inference(prim_subst,[status(thm)],[341:[bind(SV3,$thf( ~ ( SV113 ) ))]]) ).
thf(569,plain,
! [SV3: $o,SV27: $o > $o] :
( ( ( SV27 @ $true )
= $false )
| ( ( SV27 @ SV3 )
= $true )
| ( $true = $false )
| ( SV3 = $false ) ),
inference(prim_subst,[status(thm)],[341:[bind(SV1,$thf( $true ))]]) ).
thf(571,plain,
! [SV3: $o,SV114: $o,SV27: $o > $o] :
( ( ( SV27 @ ~ SV114 )
= $false )
| ( ( SV27 @ SV3 )
= $true )
| ( ( ~ SV114 ) = $false )
| ( SV3 = $false ) ),
inference(prim_subst,[status(thm)],[341:[bind(SV1,$thf( ~ ( SV114 ) ))]]) ).
thf(574,plain,
! [SV3: $o,SV1: $o,SV118: $o > $o] :
( ( ( ~ ( SV118 @ SV1 ) )
= $false )
| ( ( ~ ( SV118 @ SV3 ) )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(prim_subst,[status(thm)],[341:[bind(SV27,$thf( ^ [SV117: $o] : ~ ( SV118 @ SV117 ) ))]]) ).
thf(603,plain,
! [SV1: $o,SV110: $o > $o] :
( ( ( ~ ( SV110 @ SV1 ) )
= $false )
| ( ( ~ ( SV110 @ $true ) )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(prim_subst,[status(thm)],[346:[bind(SV29,$thf( ^ [SV109: $o] : ~ ( SV110 @ SV109 ) ))]]) ).
thf(608,plain,
! [SV114: $o,SV29: $o > $o] :
( ( ( SV29 @ ~ SV114 )
= $false )
| ( ( SV29 @ $true )
= $true )
| ( ( ~ SV114 ) = $false )
| ( $true = $false ) ),
inference(prim_subst,[status(thm)],[346:[bind(SV1,$thf( ~ ( SV114 ) ))]]) ).
thf(640,plain,
! [SV94: $o,SV33: $o > $o] :
( ( ( SV33 @ $true )
= $false )
| ( ( SV33 @ ~ SV94 )
= $true )
| ( $true = $false )
| ( ( ~ SV94 ) = $false ) ),
inference(prim_subst,[status(thm)],[356:[bind(SV4,$thf( ~ ( SV94 ) ))]]) ).
thf(643,plain,
! [SV4: $o,SV98: $o > $o] :
( ( ( ~ ( SV98 @ $true ) )
= $false )
| ( ( ~ ( SV98 @ SV4 ) )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(prim_subst,[status(thm)],[356:[bind(SV33,$thf( ^ [SV97: $o] : ~ ( SV98 @ SV97 ) ))]]) ).
thf(1031,plain,
! [SV9: $o > $o,SV6: $o,SV171: $o] :
( ( SV171 = $false )
| ( SV6 = $true )
| ( ( SV9 @ SV6 )
= $true )
| ( ( SV9 @ ~ SV171 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[439]) ).
thf(1032,plain,
! [SV2: $o,SV9: $o > $o,SV172: $o] :
( ( SV172 = $false )
| ( ( SV9 @ ~ SV172 )
= $true )
| ( ( SV9 @ SV2 )
= $false )
| ( SV2 = $true ) ),
inference(extcnf_not_pos,[status(thm)],[442]) ).
thf(1033,plain,
! [SV6: $o,SV2: $o,SV176: $o > $o] :
( ( ( SV176 @ SV2 )
= $true )
| ( ( ~ ( SV176 @ SV6 ) )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_neg,[status(thm)],[445]) ).
thf(1065,plain,
! [SV2: $o,SV162: $o > $o] :
( ( ( SV162 @ SV2 )
= $true )
| ( ( ~ ( SV162 @ $false ) )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_neg,[status(thm)],[491]) ).
thf(1074,plain,
! [SV13: $o > $o,SV171: $o] :
( ( SV171 = $false )
| ( $false = $true )
| ( ( SV13 @ $false )
= $true )
| ( ( SV13 @ ~ SV171 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[496]) ).
thf(1111,plain,
! [SV21: $o > $o,SV133: $o] :
( ( SV133 = $false )
| ( ( SV21 @ ~ SV133 )
= $true )
| ( ( SV21 @ $false )
= $false )
| ( $false = $true ) ),
inference(extcnf_not_pos,[status(thm)],[538]) ).
thf(1112,plain,
! [SV8: $o,SV137: $o > $o] :
( ( ( SV137 @ $false )
= $true )
| ( ( ~ ( SV137 @ SV8 ) )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(extcnf_not_neg,[status(thm)],[541]) ).
thf(1144,plain,
! [SV27: $o > $o,SV1: $o,SV113: $o] :
( ( SV113 = $true )
| ( SV1 = $false )
| ( ( SV27 @ ~ SV113 )
= $true )
| ( ( SV27 @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[568]) ).
thf(1145,plain,
! [SV3: $o,SV27: $o > $o,SV114: $o] :
( ( SV114 = $true )
| ( ( SV27 @ SV3 )
= $true )
| ( ( SV27 @ ~ SV114 )
= $false )
| ( SV3 = $false ) ),
inference(extcnf_not_neg,[status(thm)],[571]) ).
thf(1146,plain,
! [SV3: $o,SV1: $o,SV118: $o > $o] :
( ( ( SV118 @ SV1 )
= $true )
| ( ( ~ ( SV118 @ SV3 ) )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(extcnf_not_neg,[status(thm)],[574]) ).
thf(1165,plain,
! [SV1: $o,SV110: $o > $o] :
( ( ( SV110 @ SV1 )
= $true )
| ( ( ~ ( SV110 @ $true ) )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(extcnf_not_neg,[status(thm)],[603]) ).
thf(1174,plain,
! [SV29: $o > $o,SV114: $o] :
( ( SV114 = $true )
| ( ( SV29 @ $true )
= $true )
| ( ( SV29 @ ~ SV114 )
= $false )
| ( $true = $false ) ),
inference(extcnf_not_neg,[status(thm)],[608]) ).
thf(1193,plain,
! [SV33: $o > $o,SV94: $o] :
( ( SV94 = $true )
| ( $true = $false )
| ( ( SV33 @ ~ SV94 )
= $true )
| ( ( SV33 @ $true )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[640]) ).
thf(1194,plain,
! [SV4: $o,SV98: $o > $o] :
( ( ( SV98 @ $true )
= $true )
| ( ( ~ ( SV98 @ SV4 ) )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(extcnf_not_neg,[status(thm)],[643]) ).
thf(1269,plain,
! [SV2: $o,SV6: $o,SV176: $o > $o] :
( ( ( SV176 @ SV6 )
= $false )
| ( ( SV176 @ SV2 )
= $true )
| ( SV6 = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_pos,[status(thm)],[1033]) ).
thf(1294,plain,
! [SV2: $o,SV162: $o > $o] :
( ( ( SV162 @ $false )
= $false )
| ( ( SV162 @ SV2 )
= $true )
| ( $false = $true )
| ( SV2 = $true ) ),
inference(extcnf_not_pos,[status(thm)],[1065]) ).
thf(1334,plain,
! [SV8: $o,SV137: $o > $o] :
( ( ( SV137 @ SV8 )
= $false )
| ( ( SV137 @ $false )
= $true )
| ( SV8 = $true )
| ( $false = $true ) ),
inference(extcnf_not_pos,[status(thm)],[1112]) ).
thf(1364,plain,
! [SV1: $o,SV3: $o,SV118: $o > $o] :
( ( ( SV118 @ SV3 )
= $false )
| ( ( SV118 @ SV1 )
= $true )
| ( SV1 = $false )
| ( SV3 = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1146]) ).
thf(1379,plain,
! [SV1: $o,SV110: $o > $o] :
( ( ( SV110 @ $true )
= $false )
| ( ( SV110 @ SV1 )
= $true )
| ( SV1 = $false )
| ( $true = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1165]) ).
thf(1401,plain,
! [SV4: $o,SV98: $o > $o] :
( ( ( SV98 @ SV4 )
= $false )
| ( ( SV98 @ $true )
= $true )
| ( $true = $false )
| ( SV4 = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1194]) ).
thf(1927,plain,
! [SV2: $o,SV13: $o > $o] :
( ( ( SV13 @ SV2 )
= $false )
| ( ( SV13 @ $false )
= $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[252]) ).
thf(1928,plain,
! [SV8: $o,SV21: $o > $o] :
( ( ( SV21 @ $false )
= $false )
| ( ( SV21 @ SV8 )
= $true )
| ( SV8 = $true ) ),
inference(sim,[status(thm)],[272]) ).
thf(1929,plain,
! [SV1: $o,SV29: $o > $o] :
( ( ( SV29 @ SV1 )
= $false )
| ( ( SV29 @ $true )
= $true )
| ( SV1 = $false ) ),
inference(sim,[status(thm)],[346]) ).
thf(1930,plain,
! [SV4: $o,SV33: $o > $o] :
( ( ( SV33 @ $true )
= $false )
| ( ( SV33 @ SV4 )
= $true )
| ( SV4 = $false ) ),
inference(sim,[status(thm)],[356]) ).
thf(1931,plain,
! [SV2: $o,SV13: $o > $o] :
( ( ( SV13 @ SV2 )
= $false )
| ( ( SV13 @ $false )
= $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[252]) ).
thf(1932,plain,
! [SV8: $o,SV21: $o > $o] :
( ( ( SV21 @ $false )
= $false )
| ( ( SV21 @ SV8 )
= $true )
| ( SV8 = $true ) ),
inference(sim,[status(thm)],[272]) ).
thf(1933,plain,
! [SV1: $o,SV29: $o > $o] :
( ( ( SV29 @ SV1 )
= $false )
| ( ( SV29 @ $true )
= $true )
| ( SV1 = $false ) ),
inference(sim,[status(thm)],[346]) ).
thf(1934,plain,
! [SV4: $o,SV33: $o > $o] :
( ( ( SV33 @ $true )
= $false )
| ( ( SV33 @ SV4 )
= $true )
| ( SV4 = $false ) ),
inference(sim,[status(thm)],[356]) ).
thf(1935,plain,
! [SV6: $o,SV9: $o > $o] :
( ( ( SV9 @ $false )
= $false )
| ( ( SV9 @ SV6 )
= $true )
| ( SV6 = $true ) ),
inference(sim,[status(thm)],[438]) ).
thf(1936,plain,
! [SV2: $o,SV9: $o > $o] :
( ( ( SV9 @ SV2 )
= $false )
| ( ( SV9 @ $false )
= $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[441]) ).
thf(1937,plain,
! [SV2: $o,SV162: $o > $o] :
( ( ( SV162 @ $false )
= $false )
| ( ( SV162 @ SV2 )
= $true )
| ( SV2 = $true ) ),
inference(sim,[status(thm)],[1294]) ).
thf(1938,plain,
! [SV13: $o > $o,SV171: $o] :
( ( SV171 = $false )
| ( ( SV13 @ $false )
= $true )
| ( ( SV13 @ ~ SV171 )
= $false ) ),
inference(sim,[status(thm)],[1074]) ).
thf(1939,plain,
! [SV21: $o > $o,SV133: $o] :
( ( SV133 = $false )
| ( ( SV21 @ ~ SV133 )
= $true )
| ( ( SV21 @ $false )
= $false ) ),
inference(sim,[status(thm)],[1111]) ).
thf(1940,plain,
! [SV8: $o,SV137: $o > $o] :
( ( ( SV137 @ SV8 )
= $false )
| ( ( SV137 @ $false )
= $true )
| ( SV8 = $true ) ),
inference(sim,[status(thm)],[1334]) ).
thf(1941,plain,
! [SV1: $o,SV27: $o > $o] :
( ( ( SV27 @ SV1 )
= $false )
| ( ( SV27 @ $true )
= $true )
| ( SV1 = $false ) ),
inference(sim,[status(thm)],[566]) ).
thf(1942,plain,
! [SV3: $o,SV27: $o > $o] :
( ( ( SV27 @ $true )
= $false )
| ( ( SV27 @ SV3 )
= $true )
| ( SV3 = $false ) ),
inference(sim,[status(thm)],[569]) ).
thf(1943,plain,
! [SV1: $o,SV110: $o > $o] :
( ( ( SV110 @ $true )
= $false )
| ( ( SV110 @ SV1 )
= $true )
| ( SV1 = $false ) ),
inference(sim,[status(thm)],[1379]) ).
thf(1944,plain,
! [SV29: $o > $o,SV114: $o] :
( ( SV114 = $true )
| ( ( SV29 @ $true )
= $true )
| ( ( SV29 @ ~ SV114 )
= $false ) ),
inference(sim,[status(thm)],[1174]) ).
thf(1945,plain,
! [SV33: $o > $o,SV94: $o] :
( ( SV94 = $true )
| ( ( SV33 @ ~ SV94 )
= $true )
| ( ( SV33 @ $true )
= $false ) ),
inference(sim,[status(thm)],[1193]) ).
thf(1946,plain,
! [SV4: $o,SV98: $o > $o] :
( ( ( SV98 @ SV4 )
= $false )
| ( ( SV98 @ $true )
= $true )
| ( SV4 = $false ) ),
inference(sim,[status(thm)],[1401]) ).
thf(1947,plain,
( ( ( sK1_Xp @ a )
= ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) )
= $false ),
inference(res,[status(thm)],[69,30]) ).
thf(1948,plain,
( ( a = $true )
| ( ( ~ ( ~ a
| ~ b ) )
= $true ) ),
inference(extuni,[status(esa)],[1947]) ).
thf(1949,plain,
( ( a = $false )
| ( ( ~ ( ~ a
| ~ b ) )
= $false ) ),
inference(extuni,[status(esa)],[1947]) ).
thf(1950,plain,
( ( ( ~ a
| ~ b )
= $true )
| ( a = $false ) ),
inference(extcnf_not_neg,[status(thm)],[1949]) ).
thf(1951,plain,
( ( ( ~ a
| ~ b )
= $false )
| ( a = $true ) ),
inference(extcnf_not_pos,[status(thm)],[1948]) ).
thf(1952,plain,
( ( ( ~ a ) = $true )
| ( ( ~ b ) = $true )
| ( a = $false ) ),
inference(extcnf_or_pos,[status(thm)],[1950]) ).
thf(1953,plain,
( ( ( ~ a ) = $false )
| ( a = $true ) ),
inference(extcnf_or_neg,[status(thm)],[1951]) ).
thf(1954,plain,
( ( ( ~ b ) = $false )
| ( a = $true ) ),
inference(extcnf_or_neg,[status(thm)],[1951]) ).
thf(1955,plain,
( ( a = $false )
| ( ( ~ b ) = $true )
| ( a = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1952]) ).
thf(1956,plain,
( ( a = $true )
| ( a = $true ) ),
inference(extcnf_not_neg,[status(thm)],[1953]) ).
thf(1957,plain,
( ( b = $true )
| ( a = $true ) ),
inference(extcnf_not_neg,[status(thm)],[1954]) ).
thf(1958,plain,
( ( b = $false )
| ( a = $false )
| ( a = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1955]) ).
thf(1959,plain,
( ( b = $false )
| ( a = $false ) ),
inference(sim,[status(thm)],[1958]) ).
thf(1960,plain,
a = $true,
inference(sim,[status(thm)],[1956]) ).
thf(1961,plain,
( ( ( sK1_Xp @ b )
= ( sK1_Xp
@ ~ ( ~ a
| ~ b ) ) )
= $false ),
inference(res,[status(thm)],[70,30]) ).
thf(1962,plain,
( ( b = $true )
| ( ( ~ ( ~ a
| ~ b ) )
= $true ) ),
inference(extuni,[status(esa)],[1961]) ).
thf(1963,plain,
( ( b = $false )
| ( ( ~ ( ~ a
| ~ b ) )
= $false ) ),
inference(extuni,[status(esa)],[1961]) ).
thf(1964,plain,
( ( ( ~ a
| ~ b )
= $true )
| ( b = $false ) ),
inference(extcnf_not_neg,[status(thm)],[1963]) ).
thf(1965,plain,
( ( ( ~ a
| ~ b )
= $false )
| ( b = $true ) ),
inference(extcnf_not_pos,[status(thm)],[1962]) ).
thf(1966,plain,
( ( ( ~ a ) = $true )
| ( ( ~ b ) = $true )
| ( b = $false ) ),
inference(extcnf_or_pos,[status(thm)],[1964]) ).
thf(1967,plain,
( ( ( ~ a ) = $false )
| ( b = $true ) ),
inference(extcnf_or_neg,[status(thm)],[1965]) ).
thf(1968,plain,
( ( ( ~ b ) = $false )
| ( b = $true ) ),
inference(extcnf_or_neg,[status(thm)],[1965]) ).
thf(1969,plain,
( ( a = $false )
| ( ( ~ b ) = $true )
| ( b = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1966]) ).
thf(1970,plain,
( ( a = $true )
| ( b = $true ) ),
inference(extcnf_not_neg,[status(thm)],[1967]) ).
thf(1971,plain,
( ( b = $true )
| ( b = $true ) ),
inference(extcnf_not_neg,[status(thm)],[1968]) ).
thf(1972,plain,
( ( b = $false )
| ( a = $false )
| ( b = $false ) ),
inference(extcnf_not_pos,[status(thm)],[1969]) ).
thf(1973,plain,
( ( b = $false )
| ( a = $false ) ),
inference(sim,[status(thm)],[1972]) ).
thf(1974,plain,
b = $true,
inference(sim,[status(thm)],[1971]) ).
thf(1976,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[30,1974,1973,1970,1960,1959,1957,1946,1945,1944,1943,1942,1941,1940,1939,1938,1937,1936,1935,1934,1933,1932,1931,1930,1929,1928,1927,1364,1269,1145,1144,1032,1031,431,428,426,422,417,414,341,242,70,69]) ).
thf(1977,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[1976]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO377^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.17 % Computer : n003.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Oct 6 17:41:06 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.66/15.38
% 90.66/15.38 No.of.Axioms: 0
% 90.66/15.38
% 90.66/15.38 Length.of.Defs: 0
% 90.66/15.38
% 90.66/15.38 Contains.Choice.Funs: false
% 90.66/15.38 ....eprover: CPU time limit exceeded, terminating
% 90.66/15.38 ................................
% 90.66/15.38
% 90.66/15.38 ********************************
% 90.66/15.38 * All subproblems solved! *
% 90.66/15.38 ********************************
% 90.66/15.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:15,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:1976,loop_count:5,foatp_calls:3,translation:fof_full)
% 90.66/15.38
% 90.66/15.38 %**** Beginning of derivation protocol ****
% 90.66/15.38 % SZS output start CNFRefutation
% See solution above
% 90.66/15.38
% 90.66/15.38 %**** End of derivation protocol ****
% 90.66/15.38 %**** no. of clauses in derivation: 174 ****
% 90.66/15.38 %**** clause counter: 1976 ****
% 90.66/15.38
% 90.66/15.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:15,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:1976,loop_count:5,foatp_calls:3,translation:fof_full)
%------------------------------------------------------------------------------