%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : CSR134^2 : TPTP v9.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.CBa7c75t8m true
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:32:24 PM UTC 2025
% Result : Theorem 0.38s 0.89s
% Output : Refutation 0.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 4
% Syntax : Number of formulae : 47 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 127 ( 0 equ; 20 cnn)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 322 ( 49 ~; 14 |; 16 &; 243 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 13 ( 13 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 67 ( 22 ^; 39 !; 6 ?; 67 :)
% Comments :
%------------------------------------------------------------------------------
thf(lYearFn_THFTYPE_IiiI_type,type,
lYearFn_THFTYPE_IiiI: $i > $i ).
thf(lBob_THFTYPE_i_type,type,
lBob_THFTYPE_i: $i ).
thf(instance_THFTYPE_IIiioIioI_type,type,
instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
thf(holdsDuring_THFTYPE_IiooI_type,type,
holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
thf(n2009_THFTYPE_i_type,type,
n2009_THFTYPE_i: $i ).
thf(subclass_THFTYPE_IiioI_type,type,
subclass_THFTYPE_IiioI: $i > $i > $o ).
thf(lSue_THFTYPE_i_type,type,
lSue_THFTYPE_i: $i ).
thf(lBinaryPredicate_THFTYPE_i_type,type,
lBinaryPredicate_THFTYPE_i: $i ).
thf(lAnna_THFTYPE_i_type,type,
lAnna_THFTYPE_i: $i ).
thf(parent_THFTYPE_IiioI_type,type,
parent_THFTYPE_IiioI: $i > $i > $o ).
thf(ax_019,axiom,
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ) ).
thf(zip_derived_cl10,plain,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ),
inference(cnf,[status(esa)],[ax_019]) ).
thf(zip_derived_cl426,plain,
( ~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ $true ) ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl10]) ).
thf(zip_derived_cl427,plain,
( ~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl426]) ).
thf(ax_058,axiom,
instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
thf(zip_derived_cl25,plain,
instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i,
inference(cnf,[status(esa)],[ax_058]) ).
thf(con,conjecture,
? [R: $i > $i > $o,X: $i,Y: $i] :
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ~ ( R @ Y @ lAnna_THFTYPE_i )
& ( R @ X @ lAnna_THFTYPE_i ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [R: $i > $i > $o,X: $i,Y: $i] :
( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ~ ( R @ Y @ lAnna_THFTYPE_i )
& ( R @ X @ lAnna_THFTYPE_i ) ) ),
inference('cnf.neg',[status(esa)],[con]) ).
thf(zip_derived_cl27,plain,
! [X0: $i > $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( X0 @ X1 @ lAnna_THFTYPE_i ) )
& ( X0 @ X2 @ lAnna_THFTYPE_i ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl695,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~)
@ ( ^ [Y0: $i,Y1: $i] : ( X0 @ Y0 )
@ X1
@ lAnna_THFTYPE_i ) )
& ( ^ [Y0: $i,Y1: $i] : ( X0 @ Y0 )
@ X2
@ lAnna_THFTYPE_i ) ) ),
inference(prune_arg_fun,[status(thm)],[zip_derived_cl27]) ).
thf(zip_derived_cl696,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( X0 @ X1 ) )
& ( X0 @ X2 ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl695]) ).
thf(zip_derived_cl748,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ $true )
& ( ^ [Y0: $i] :
( instance_THFTYPE_IIiioIioI
@ ( ^ [Y1: $i,Y2: $i,Y3: $i] :
( subclass_THFTYPE_IiioI
@ ( ^ [Y4: $i,Y5: $i,Y6: $i] : Y5
@ Y1
@ Y2
@ Y3 )
@ ( ^ [Y4: $i,Y5: $i,Y6: $i] : Y6
@ Y1
@ Y2
@ Y3 ) )
@ Y0 )
@ ( ^ [Y1: $i] : lBinaryPredicate_THFTYPE_i
@ Y0 ) )
@ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl25,zip_derived_cl696]) ).
thf(zip_derived_cl847,plain,
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ $true )
& ( instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl748]) ).
thf(zip_derived_cl25_001,plain,
instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i,
inference(cnf,[status(esa)],[ax_058]) ).
thf(zip_derived_cl848,plain,
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ $true )
& $true ) ),
inference(demod,[status(thm)],[zip_derived_cl847,zip_derived_cl25]) ).
thf(zip_derived_cl849,plain,
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl848]) ).
thf(zip_derived_cl948,plain,
~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ),
inference(demod,[status(thm)],[zip_derived_cl427,zip_derived_cl849]) ).
thf(ax_009,axiom,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ) ).
thf(zip_derived_cl6,plain,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ),
inference(cnf,[status(esa)],[ax_009]) ).
thf(zip_derived_cl92,plain,
( ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl6]) ).
thf(zip_derived_cl849_002,plain,
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl848]) ).
thf(zip_derived_cl941,plain,
parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i,
inference(demod,[status(thm)],[zip_derived_cl92,zip_derived_cl849]) ).
thf(zip_derived_cl696_003,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( X0 @ X1 ) )
& ( X0 @ X2 ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl695]) ).
thf(zip_derived_cl1073,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~)
@ ( ^ [Y0: $i] :
( parent_THFTYPE_IiioI
@ ( ^ [Y1: $i] : Y1
@ Y0 )
@ ( ^ [Y1: $i] : lAnna_THFTYPE_i
@ Y0 ) )
@ X0 ) )
& $true ) ),
inference('sup-',[status(thm)],[zip_derived_cl941,zip_derived_cl696]) ).
thf(zip_derived_cl1085,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i ) )
& $true ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl1073]) ).
thf(zip_derived_cl1086,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i ) ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1085]) ).
thf(zip_derived_cl1267,plain,
! [X0: $i] :
( ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i )
| ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ $false ) ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl1086]) ).
thf(zip_derived_cl1271,plain,
! [X0: $i] :
( ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i )
| ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1267]) ).
thf(zip_derived_cl93,plain,
( ~ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl6]) ).
thf(zip_derived_cl92_004,plain,
( ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl6]) ).
thf(zip_derived_cl98,plain,
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $false ) ),
inference('sup+',[status(thm)],[zip_derived_cl93,zip_derived_cl92]) ).
thf(zip_derived_cl696_005,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( X0 @ X1 ) )
& ( X0 @ X2 ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl695]) ).
thf(zip_derived_cl699,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
( ( ( (~) @ ( X0 @ X2 ) )
& ( X0 @ X1 ) )
| ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true ) ),
inference(ext_sup,[status(thm)],[zip_derived_cl98,zip_derived_cl696]) ).
thf(zip_derived_cl990,plain,
! [X0: $i > $o,X1: $i] :
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true )
| ( X0 @ X1 ) ),
inference(cnf_otf,[status(thm)],[zip_derived_cl699]) ).
thf(zip_derived_cl992,plain,
! [X0: $o,X1: $i] :
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true )
| ( ^ [Y0: $i] : X0
@ X1 ) ),
inference(prune_arg_fun,[status(thm)],[zip_derived_cl990]) ).
thf(zip_derived_cl993,plain,
! [X0: $o] :
( ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true )
| X0 ),
inference(ho_norm,[status(thm)],[zip_derived_cl992]) ).
thf(zip_derived_cl994,plain,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true,
inference(condensation,[status(thm)],[zip_derived_cl993]) ).
thf(zip_derived_cl696_006,plain,
! [X0: $i > $o,X1: $i,X2: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( X0 @ X1 ) )
& ( X0 @ X2 ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl695]) ).
thf(zip_derived_cl998,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~)
@ ( ^ [Y0: $i] :
( holdsDuring_THFTYPE_IiooI
@ ( ^ [Y1: $i] : Y1
@ Y0 )
@ ( ^ [Y1: $i] : $true
@ Y0 ) )
@ X0 ) )
& $true ) ),
inference('sup-',[status(thm)],[zip_derived_cl994,zip_derived_cl696]) ).
thf(zip_derived_cl1017,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
@ ( ( (~) @ ( holdsDuring_THFTYPE_IiooI @ X0 @ $true ) )
& $true ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl998]) ).
thf(zip_derived_cl1018,plain,
! [X0: $i] :
~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ ( holdsDuring_THFTYPE_IiooI @ X0 @ $true ) ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1017]) ).
thf(zip_derived_cl1219,plain,
! [X0: $i] :
( ( holdsDuring_THFTYPE_IiooI @ X0 @ $true )
| ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( (~) @ $false ) ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl1018]) ).
thf(zip_derived_cl1223,plain,
! [X0: $i] :
( ( holdsDuring_THFTYPE_IiooI @ X0 @ $true )
| ~ ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1219]) ).
thf(zip_derived_cl994_007,plain,
holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ $true,
inference(condensation,[status(thm)],[zip_derived_cl993]) ).
thf(zip_derived_cl1224,plain,
! [X0: $i] : ( holdsDuring_THFTYPE_IiooI @ X0 @ $true ),
inference(demod,[status(thm)],[zip_derived_cl1223,zip_derived_cl994]) ).
thf(zip_derived_cl1272,plain,
! [X0: $i] : ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i ),
inference(demod,[status(thm)],[zip_derived_cl1271,zip_derived_cl1224]) ).
thf(zip_derived_cl1273,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl948,zip_derived_cl1272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CSR134^2 : TPTP v9.2.0. Released v4.1.0.
% 0.04/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.CBa7c75t8m true
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8042.1875MB
% 0.08/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Oct 1 14:56:53 EDT 2025
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Running portfolio for 300 s
% 0.08/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Number of cores: 8
% 0.08/0.36 % Python version: Python 3.6.8
% 0.08/0.36 % Running in HO mode
% 0.30/0.61 % Total configuration time : 828
% 0.30/0.61 % Estimated wc time : 1656
% 0.30/0.61 % Estimated cpu time (8 cpus) : 207.0
% 0.36/0.65 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.36/0.70 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.37/0.78 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.38/0.88 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.38/0.89 % Solved by lams/40_c.s.sh.
% 0.38/0.89 % done 150 iterations in 0.136s
% 0.38/0.89 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.38/0.89 % SZS output start Refutation
% See solution above
% 0.38/0.89
% 0.38/0.89
% 0.38/0.89 % Terminating...
% 0.40/1.18 % Runner terminated.
% 1.34/1.20 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------