%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : CSR125^2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 10:16:05 AM UTC 2026
% Result : Theorem 0.42s 0.37s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 22 ( 18 unt; 0 typ; 0 def)
% Number of atoms : 81 ( 22 equ; 0 cnn)
% Maximal formula atoms : 2 ( 3 avg)
% Number of connectives : 80 ( 9 ~; 2 |; 0 &; 69 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 139 ( 136 usr; 71 con; 0-3 aty)
% Number of variables : 11 ( 0 ^; 11 !; 0 ?; 11 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_num,type,
num: $tType ).
thf(tp_agent_THFTYPE_IiioI,type,
agent_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_attribute_THFTYPE_i,type,
attribute_THFTYPE_i: $i ).
thf(tp_believes_THFTYPE_IiooI,type,
believes_THFTYPE_IiooI: $i > $o > $o ).
thf(tp_containsInformation_THFTYPE_IiooI,type,
containsInformation_THFTYPE_IiooI: $i > $o > $o ).
thf(tp_contraryAttribute_THFTYPE_IioI,type,
contraryAttribute_THFTYPE_IioI: $i > $o ).
thf(tp_contraryAttribute_THFTYPE_IoooI,type,
contraryAttribute_THFTYPE_IoooI: $o > $o > $o ).
thf(tp_disjointRelation_THFTYPE_IiioI,type,
disjointRelation_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_disjoint_THFTYPE_IiioI,type,
disjoint_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_documentation_THFTYPE_i,type,
documentation_THFTYPE_i: $i ).
thf(tp_domainSubclass_THFTYPE_IIiiiIiioI,type,
domainSubclass_THFTYPE_IIiiiIiioI: ( $i > $i > $i ) > $i > $i > $o ).
thf(tp_domainSubclass_THFTYPE_IIiioIiioI,type,
domainSubclass_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
thf(tp_domainSubclass_THFTYPE_IIioIiioI,type,
domainSubclass_THFTYPE_IIioIiioI: ( $i > $o ) > $i > $i > $o ).
thf(tp_domainSubclass_THFTYPE_IiiioI,type,
domainSubclass_THFTYPE_IiiioI: $i > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIIioIiioIiioI,type,
domain_THFTYPE_IIIioIiioIiioI: ( ( $i > $o ) > $i > $i > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIiiIiioI,type,
domain_THFTYPE_IIiiIiioI: ( $i > $i ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIiiiIiioI,type,
domain_THFTYPE_IIiiiIiioI: ( $i > $i > $i ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIiiioIiioI,type,
domain_THFTYPE_IIiiioIiioI: ( $i > $i > $i > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIiioIiioI,type,
domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIioIiioI,type,
domain_THFTYPE_IIioIiioI: ( $i > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIiooIiioI,type,
domain_THFTYPE_IIiooIiioI: ( $i > $o > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IIoooIiioI,type,
domain_THFTYPE_IIoooIiioI: ( $o > $o > $o ) > $i > $i > $o ).
thf(tp_domain_THFTYPE_IiiioI,type,
domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
thf(tp_duration_THFTYPE_IiioI,type,
duration_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_equal_THFTYPE_i,type,
equal_THFTYPE_i: $i ).
thf(tp_greaterThan_THFTYPE_i,type,
greaterThan_THFTYPE_i: $i ).
thf(tp_holdsDuring_THFTYPE_IiooI,type,
holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
thf(tp_inList_THFTYPE_IiioI,type,
inList_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_instance_THFTYPE_IIIiioIiioIioI,type,
instance_THFTYPE_IIIiioIiioIioI: ( ( $i > $i > $o ) > $i > $i > $o ) > $i > $o ).
thf(tp_instance_THFTYPE_IIIioIiioIioI,type,
instance_THFTYPE_IIIioIiioIioI: ( ( $i > $o ) > $i > $i > $o ) > $i > $o ).
thf(tp_instance_THFTYPE_IIiiIioI,type,
instance_THFTYPE_IIiiIioI: ( $i > $i ) > $i > $o ).
thf(tp_instance_THFTYPE_IIiiiIioI,type,
instance_THFTYPE_IIiiiIioI: ( $i > $i > $i ) > $i > $o ).
thf(tp_instance_THFTYPE_IIiiioIioI,type,
instance_THFTYPE_IIiiioIioI: ( $i > $i > $i > $o ) > $i > $o ).
thf(tp_instance_THFTYPE_IIiioIioI,type,
instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
thf(tp_instance_THFTYPE_IIiooIioI,type,
instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
thf(tp_instance_THFTYPE_IiioI,type,
instance_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_instance_THFTYPE_IoioI,type,
instance_THFTYPE_IoioI: $o > $i > $o ).
thf(tp_instrument_THFTYPE_i,type,
instrument_THFTYPE_i: $i ).
thf(tp_knows_THFTYPE_IiooI,type,
knows_THFTYPE_IiooI: $i > $o > $o ).
thf(tp_lAdditionFn_THFTYPE_i,type,
lAdditionFn_THFTYPE_i: $i ).
thf(tp_lAgent_THFTYPE_i,type,
lAgent_THFTYPE_i: $i ).
thf(tp_lAsymmetricRelation_THFTYPE_i,type,
lAsymmetricRelation_THFTYPE_i: $i ).
thf(tp_lAttribute_THFTYPE_i,type,
lAttribute_THFTYPE_i: $i ).
thf(tp_lBeginFn_THFTYPE_IiiI,type,
lBeginFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lBill_THFTYPE_i,type,
lBill_THFTYPE_i: $i ).
thf(tp_lBinaryFunction_THFTYPE_i,type,
lBinaryFunction_THFTYPE_i: $i ).
thf(tp_lBinaryPredicate_THFTYPE_i,type,
lBinaryPredicate_THFTYPE_i: $i ).
thf(tp_lCardinalityFn_THFTYPE_IiiI,type,
lCardinalityFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lCognitiveAgent_THFTYPE_i,type,
lCognitiveAgent_THFTYPE_i: $i ).
thf(tp_lContentBearingObject_THFTYPE_i,type,
lContentBearingObject_THFTYPE_i: $i ).
thf(tp_lDayDuration_THFTYPE_i,type,
lDayDuration_THFTYPE_i: $i ).
thf(tp_lDay_THFTYPE_i,type,
lDay_THFTYPE_i: $i ).
thf(tp_lDirectionalAttribute_THFTYPE_i,type,
lDirectionalAttribute_THFTYPE_i: $i ).
thf(tp_lEndFn_THFTYPE_IiiI,type,
lEndFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lEntity_THFTYPE_i,type,
lEntity_THFTYPE_i: $i ).
thf(tp_lFormula_THFTYPE_i,type,
lFormula_THFTYPE_i: $i ).
thf(tp_lHuman_THFTYPE_i,type,
lHuman_THFTYPE_i: $i ).
thf(tp_lInheritableRelation_THFTYPE_i,type,
lInheritableRelation_THFTYPE_i: $i ).
thf(tp_lInteger_THFTYPE_i,type,
lInteger_THFTYPE_i: $i ).
thf(tp_lIntentionalProcess_THFTYPE_i,type,
lIntentionalProcess_THFTYPE_i: $i ).
thf(tp_lInternalAttribute_THFTYPE_i,type,
lInternalAttribute_THFTYPE_i: $i ).
thf(tp_lIrreflexiveRelation_THFTYPE_i,type,
lIrreflexiveRelation_THFTYPE_i: $i ).
thf(tp_lLinguisticExpression_THFTYPE_i,type,
lLinguisticExpression_THFTYPE_i: $i ).
thf(tp_lListFn_THFTYPE_IiiI,type,
lListFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lListFn_THFTYPE_i,type,
lListFn_THFTYPE_i: $i ).
thf(tp_lListOrderFn_THFTYPE_IiiiI,type,
lListOrderFn_THFTYPE_IiiiI: $i > $i > $i ).
thf(tp_lListOrderFn_THFTYPE_i,type,
lListOrderFn_THFTYPE_i: $i ).
thf(tp_lList_THFTYPE_i,type,
lList_THFTYPE_i: $i ).
thf(tp_lMary_THFTYPE_i,type,
lMary_THFTYPE_i: $i ).
thf(tp_lMeasureFn_THFTYPE_IiiiI,type,
lMeasureFn_THFTYPE_IiiiI: $i > $i > $i ).
thf(tp_lMonthFn_THFTYPE_i,type,
lMonthFn_THFTYPE_i: $i ).
thf(tp_lMonth_THFTYPE_i,type,
lMonth_THFTYPE_i: $i ).
thf(tp_lMultiplicationFn_THFTYPE_i,type,
lMultiplicationFn_THFTYPE_i: $i ).
thf(tp_lObject_THFTYPE_i,type,
lObject_THFTYPE_i: $i ).
thf(tp_lOrganism_THFTYPE_i,type,
lOrganism_THFTYPE_i: $i ).
thf(tp_lOrganization_THFTYPE_i,type,
lOrganization_THFTYPE_i: $i ).
thf(tp_lPositionalAttribute_THFTYPE_i,type,
lPositionalAttribute_THFTYPE_i: $i ).
thf(tp_lProcess_THFTYPE_i,type,
lProcess_THFTYPE_i: $i ).
thf(tp_lProposition_THFTYPE_i,type,
lProposition_THFTYPE_i: $i ).
thf(tp_lQuantity_THFTYPE_i,type,
lQuantity_THFTYPE_i: $i ).
thf(tp_lRelationExtendedToQuantities_THFTYPE_i,type,
lRelationExtendedToQuantities_THFTYPE_i: $i ).
thf(tp_lRelation_THFTYPE_i,type,
lRelation_THFTYPE_i: $i ).
thf(tp_lRelationalAttribute_THFTYPE_i,type,
lRelationalAttribute_THFTYPE_i: $i ).
thf(tp_lSelfConnectedObject_THFTYPE_i,type,
lSelfConnectedObject_THFTYPE_i: $i ).
thf(tp_lSentence_THFTYPE_i,type,
lSentence_THFTYPE_i: $i ).
thf(tp_lSetOrClass_THFTYPE_i,type,
lSetOrClass_THFTYPE_i: $i ).
thf(tp_lSubtractionFn_THFTYPE_i,type,
lSubtractionFn_THFTYPE_i: $i ).
thf(tp_lSue_THFTYPE_i,type,
lSue_THFTYPE_i: $i ).
thf(tp_lTemporalCompositionFn_THFTYPE_IiiiI,type,
lTemporalCompositionFn_THFTYPE_IiiiI: $i > $i > $i ).
thf(tp_lTemporalCompositionFn_THFTYPE_i,type,
lTemporalCompositionFn_THFTYPE_i: $i ).
thf(tp_lTemporalRelation_THFTYPE_i,type,
lTemporalRelation_THFTYPE_i: $i ).
thf(tp_lTernaryPredicate_THFTYPE_i,type,
lTernaryPredicate_THFTYPE_i: $i ).
thf(tp_lText_THFTYPE_i,type,
lText_THFTYPE_i: $i ).
thf(tp_lTimeInterval_THFTYPE_i,type,
lTimeInterval_THFTYPE_i: $i ).
thf(tp_lTotalValuedRelation_THFTYPE_i,type,
lTotalValuedRelation_THFTYPE_i: $i ).
thf(tp_lTransitiveRelation_THFTYPE_i,type,
lTransitiveRelation_THFTYPE_i: $i ).
thf(tp_lTruthValue_THFTYPE_i,type,
lTruthValue_THFTYPE_i: $i ).
thf(tp_lUnaryFunction_THFTYPE_i,type,
lUnaryFunction_THFTYPE_i: $i ).
thf(tp_lWhenFn_THFTYPE_IiiI,type,
lWhenFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lWhenFn_THFTYPE_i,type,
lWhenFn_THFTYPE_i: $i ).
thf(tp_lYearFn_THFTYPE_IiiI,type,
lYearFn_THFTYPE_IiiI: $i > $i ).
thf(tp_lYearFn_THFTYPE_i,type,
lYearFn_THFTYPE_i: $i ).
thf(tp_lYear_THFTYPE_i,type,
lYear_THFTYPE_i: $i ).
thf(tp_lessThan_THFTYPE_i,type,
lessThan_THFTYPE_i: $i ).
thf(tp_likes_THFTYPE_IiioI,type,
likes_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_located_THFTYPE_IiioI,type,
located_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_meetsTemporally_THFTYPE_IiioI,type,
meetsTemporally_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_member_THFTYPE_IiioI,type,
member_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_minus_THFTYPE_IiiiI,type,
minus_THFTYPE_IiiiI: $i > $i > $i ).
thf(tp_modalAttribute_THFTYPE_i,type,
modalAttribute_THFTYPE_i: $i ).
thf(tp_n12_THFTYPE_i,type,
n12_THFTYPE_i: $i ).
thf(tp_n1_THFTYPE_i,type,
n1_THFTYPE_i: $i ).
thf(tp_n2009_THFTYPE_i,type,
n2009_THFTYPE_i: $i ).
thf(tp_n2_THFTYPE_i,type,
n2_THFTYPE_i: $i ).
thf(tp_n3_THFTYPE_i,type,
n3_THFTYPE_i: $i ).
thf(tp_orientation_THFTYPE_IiiioI,type,
orientation_THFTYPE_IiiioI: $i > $i > $i > $o ).
thf(tp_part_THFTYPE_IiioI,type,
part_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_partition_THFTYPE_IiiioI,type,
partition_THFTYPE_IiiioI: $i > $i > $i > $o ).
thf(tp_patient_THFTYPE_i,type,
patient_THFTYPE_i: $i ).
thf(tp_property_THFTYPE_IiioI,type,
property_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_rangeSubclass_THFTYPE_IiioI,type,
rangeSubclass_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_range_THFTYPE_IiioI,type,
range_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_relatedInternalConcept_THFTYPE_IIiioIIiioIoI,type,
relatedInternalConcept_THFTYPE_IIiioIIiioIoI: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(tp_relatedInternalConcept_THFTYPE_IiIiiIoI,type,
relatedInternalConcept_THFTYPE_IiIiiIoI: $i > ( $i > $i ) > $o ).
thf(tp_relatedInternalConcept_THFTYPE_IiIiooIoI,type,
relatedInternalConcept_THFTYPE_IiIiooIoI: $i > ( $i > $o > $o ) > $o ).
thf(tp_relatedInternalConcept_THFTYPE_IiioI,type,
relatedInternalConcept_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_result_THFTYPE_i,type,
result_THFTYPE_i: $i ).
thf(tp_subAttribute_THFTYPE_IiioI,type,
subAttribute_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_subProcess_THFTYPE_IiioI,type,
subProcess_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_subclass_THFTYPE_IiioI,type,
subclass_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_subrelation_THFTYPE_IIiioIIiioIoI,type,
subrelation_THFTYPE_IIiioIIiioIoI: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(tp_subrelation_THFTYPE_IIioIIioIoI,type,
subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
thf(tp_subrelation_THFTYPE_IIoooIIiioIoI,type,
subrelation_THFTYPE_IIoooIIiioIoI: ( $o > $o > $o ) > ( $i > $i > $o ) > $o ).
thf(tp_subrelation_THFTYPE_IiIiioIoI,type,
subrelation_THFTYPE_IiIiioIoI: $i > ( $i > $i > $o ) > $o ).
thf(tp_subrelation_THFTYPE_IiioI,type,
subrelation_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_temporalPart_THFTYPE_IiioI,type,
temporalPart_THFTYPE_IiioI: $i > $i > $o ).
thf(tp_truth_THFTYPE_IoooI,type,
truth_THFTYPE_IoooI: $o > $o > $o ).
thf(190,axiom,
likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_082) ).
thf(204,axiom,
! [X: $i] :
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_068) ).
thf(273,conjecture,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con) ).
thf(274,negated_conjecture,
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false )
= $false ),
inference(negate_conjecture,[status(cth)],[273]) ).
thf(275,plain,
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false )
= $false ),
inference(unfold_def,[status(thm)],[274]) ).
thf(290,plain,
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i )
= $true ),
inference(unfold_def,[status(thm)],[190]) ).
thf(296,plain,
( ( ! [X: $i] :
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X ) ) )
= $true ),
inference(unfold_def,[status(thm)],[204]) ).
thf(299,plain,
( ( ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) )
= $true ),
inference(polarity_switch,[status(thm)],[275]) ).
thf(304,plain,
( ( ! [X: $i] :
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X ) ) )
= $true ),
inference(copy,[status(thm)],[296]) ).
thf(310,plain,
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i )
= $true ),
inference(copy,[status(thm)],[290]) ).
thf(325,plain,
( ( ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) )
= $true ),
inference(copy,[status(thm)],[299]) ).
thf(330,plain,
! [SV3: $i] :
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV3 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[304]) ).
thf(331,plain,
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false )
= $false ),
inference(extcnf_not_pos,[status(thm)],[325]) ).
thf(406,plain,
! [SV11: $i] :
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV11 ) )
= $true ),
inference(rename,[status(thm)],[330]) ).
thf(407,plain,
! [SV11: $i] :
( ( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false )
= ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV11 ) ) )
= $false ),
inference(res,[status(thm)],[331,406]) ).
thf(428,plain,
! [SV11: $i] :
( ( $false = $true )
| ( ( ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV11 ) )
= $true ) ),
inference(extuni,[status(esa)],[407]) ).
thf(431,plain,
! [SV11: $i] :
( ( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV11 )
= $false )
| ( $false = $true ) ),
inference(extcnf_not_pos,[status(thm)],[428]) ).
thf(432,plain,
! [SV11: $i] :
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV11 )
= $false ),
inference(sim,[status(thm)],[431]) ).
thf(433,plain,
! [SV12: $i] :
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV12 )
= $false ),
inference(rename,[status(thm)],[432]) ).
thf(449,plain,
! [SV12: $i] :
( ( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ SV12 )
= ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ) )
= $false ),
inference(res,[status(thm)],[433,310]) ).
thf(455,plain,
$false = $true,
inference(extuni,[status(esa)],[449:[bind(SV12,$thf( lBill_THFTYPE_i ))]]) ).
thf(456,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR125^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.18 % Computer : n001.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Oct 6 19:01:24 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.37 .
% 0.42/0.37
% 0.42/0.37 No.of.Axioms: 272
% 0.42/0.37
% 0.42/0.37 Length.of.Defs: 0
% 0.42/0.37
% 0.42/0.37 Contains.Choice.Funs: false
% 0.42/0.37 .........
% 0.42/0.37
% 0.42/0.37 ********************************
% 0.42/0.37 * All subproblems solved! *
% 0.42/0.37 ********************************
% 0.42/0.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:2,axioms:23,ps:3,u:5,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:455,loop_count:23,foatp_calls:2,translation:fof_full)
% 0.42/0.37
% 0.42/0.37 %**** Beginning of derivation protocol ****
% 0.42/0.37 % SZS output start CNFRefutation
% See solution above
% 0.42/0.37
% 0.42/0.37 %**** End of derivation protocol ****
% 0.42/0.37 %**** no. of clauses in derivation: 22 ****
% 0.42/0.37 %**** clause counter: 455 ****
% 0.42/0.37
% 0.42/0.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:2,axioms:23,ps:3,u:5,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:455,loop_count:23,foatp_calls:2,translation:fof_full)
%------------------------------------------------------------------------------