%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.2xcgFtpWky 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 : Tue May 5 07:08:52 PM UTC 2026
% Result : Unsatisfiable 0.56s 0.95s
% Output : Refutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.2xcgFtpWky true
% 0.16/0.34 % Computer : n005.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 12:35:30 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 % Running portfolio for 300 s
% 0.16/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Number of cores: 8
% 0.16/0.34 % Python version: Python 3.6.8
% 0.16/0.35 % Running in FO mode
% 0.54/0.64 % Total configuration time : 435
% 0.54/0.64 % Estimated wc time : 1092
% 0.54/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.55/0.78 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 0.56/0.95 % Solved by fo/fo3_bce.sh.
% 0.56/0.95 % BCE start: 56
% 0.56/0.95 % BCE eliminated: 0
% 0.56/0.95 % PE start: 56
% 0.56/0.95 logic: eq
% 0.56/0.95 % PE eliminated: 0
% 0.56/0.95 % done 309 iterations in 0.217s
% 0.56/0.95 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.56/0.95 % SZS output start Refutation
% 0.56/0.95 thf(a_type, type, a: $i).
% 0.56/0.95 thf(var_type, type, var: $i > $i).
% 0.56/0.95 thf(arr_type, type, arr: $i > $i > $i).
% 0.56/0.95 thf(lam_type, type, lam: $i > $i).
% 0.56/0.95 thf(tc_type, type, tc: $i > $i > $i > $i).
% 0.56/0.95 thf(nil_type, type, nil: $i).
% 0.56/0.95 thf(just_type, type, just: $i > $i).
% 0.56/0.95 thf(cons_type, type, cons: $i > $i > $i).
% 0.56/0.95 thf(bfalse_type, type, bfalse: $i).
% 0.56/0.95 thf(notb_type, type, notb: $i > $i).
% 0.56/0.95 thf(eq4_type, type, eq4: $i > $i > $i).
% 0.56/0.95 thf(eq_type, type, eq: $i > $i > $i).
% 0.56/0.95 thf(andb_type, type, andb: $i > $i > $i).
% 0.56/0.95 thf(zero_type, type, zero: $i).
% 0.56/0.95 thf(b_type, type, b: $i).
% 0.56/0.95 thf(aux_type, type, aux: $i > $i > $i > $i > $i).
% 0.56/0.95 thf(sat_synth_nf_k_type, type, sat_synth_nf_k: $i > $i).
% 0.56/0.95 thf(nf_type, type, nf: $i > $i).
% 0.56/0.95 thf(btrue_type, type, btrue: $i).
% 0.56/0.95 thf(index_type, type, index: $i > $i > $i).
% 0.56/0.95 thf(axiom_005, axiom, (( index @ ( cons @ Z @ Xs ) @ zero ) = ( just @ Z ))).
% 0.56/0.95 thf(zip_derived_cl5, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i]: ((index @ (cons @ X0 @ X1) @ zero) = (just @ X0))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_005])).
% 0.56/0.95 thf(axiom_019, axiom,
% 0.56/0.95 (( tc @ X @ ( var @ X3 ) @ Z ) = ( aux @ X @ Z @ X3 @ ( index @ X @ X3 ) ))).
% 0.56/0.95 thf(zip_derived_cl19, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.56/0.95 ((tc @ X0 @ (var @ X2) @ X1)
% 0.56/0.95 = (aux @ X0 @ X1 @ X2 @ (index @ X0 @ X2)))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_019])).
% 0.56/0.95 thf(zip_derived_cl64, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.56/0.95 ((tc @ (cons @ X0 @ X1) @ (var @ zero) @ X2)
% 0.56/0.95 = (aux @ (cons @ X0 @ X1) @ X2 @ zero @ (just @ X0)))),
% 0.56/0.95 inference('sup+', [status(thm)], [zip_derived_cl5, zip_derived_cl19])).
% 0.56/0.95 thf(axiom_001, axiom,
% 0.56/0.95 (( aux @ X @ Z @ X3 @ ( just @ Tx3 ) ) = ( eq @ Tx3 @ Z ))).
% 0.56/0.95 thf(zip_derived_cl1, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.56/0.95 ((aux @ X2 @ X1 @ X3 @ (just @ X0)) = (eq @ X0 @ X1))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_001])).
% 0.56/0.95 thf(zip_derived_cl67, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.56/0.95 ((tc @ (cons @ X0 @ X1) @ (var @ zero) @ X2) = (eq @ X0 @ X2))),
% 0.56/0.95 inference('demod', [status(thm)], [zip_derived_cl64, zip_derived_cl1])).
% 0.56/0.95 thf(axiom_015, axiom,
% 0.56/0.95 (( tc @ X @ ( lam @ E ) @ ( arr @ Tx2 @ T1 ) ) =
% 0.56/0.95 ( tc @ ( cons @ Tx2 @ X ) @ E @ T1 ))).
% 0.56/0.95 thf(zip_derived_cl15, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.56/0.95 ((tc @ X1 @ (lam @ X2) @ (arr @ X0 @ X3))
% 0.56/0.95 = (tc @ (cons @ X0 @ X1) @ X2 @ X3))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_015])).
% 0.56/0.95 thf(zip_derived_cl165, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.56/0.95 ((tc @ X2 @ (lam @ (var @ zero)) @ (arr @ X1 @ X0)) = (eq @ X1 @ X0))),
% 0.56/0.95 inference('sup+', [status(thm)], [zip_derived_cl67, zip_derived_cl15])).
% 0.56/0.95 thf(zip_derived_cl15, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.56/0.95 ((tc @ X1 @ (lam @ X2) @ (arr @ X0 @ X3))
% 0.56/0.95 = (tc @ (cons @ X0 @ X1) @ X2 @ X3))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_015])).
% 0.56/0.95 thf(zip_derived_cl428, plain,
% 0.56/0.95 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.56/0.95 ((tc @ X3 @ (lam @ (lam @ (var @ zero))) @
% 0.56/0.95 (arr @ X2 @ (arr @ X1 @ X0))) = (eq @ X1 @ X0))),
% 0.56/0.95 inference('sup+', [status(thm)], [zip_derived_cl165, zip_derived_cl15])).
% 0.56/0.95 thf(axiom_020, axiom,
% 0.56/0.95 (( sat_synth_nf_k @ X ) =
% 0.56/0.95 ( notb @
% 0.56/0.95 ( andb @ ( nf @ X ) @ ( tc @ nil @ X @ ( arr @ a @ ( arr @ b @ b ) ) ) ) ))).
% 0.56/0.95 thf(zip_derived_cl20, plain,
% 0.56/0.95 (![X0 : $i]:
% 0.56/0.95 ((sat_synth_nf_k @ X0)
% 0.56/0.95 = (notb @
% 0.56/0.95 (andb @ (nf @ X0) @ (tc @ nil @ X0 @ (arr @ a @ (arr @ b @ b))))))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_020])).
% 0.56/0.95 thf(zip_derived_cl1151, plain,
% 0.56/0.95 (((sat_synth_nf_k @ (lam @ (lam @ (var @ zero))))
% 0.56/0.95 = (notb @ (andb @ (nf @ (lam @ (lam @ (var @ zero)))) @ (eq @ b @ b))))),
% 0.56/0.95 inference('sup+', [status(thm)], [zip_derived_cl428, zip_derived_cl20])).
% 0.56/0.95 thf(axiom_012, axiom, (( nf @ ( lam @ E ) ) = ( nf @ E ))).
% 0.56/0.95 thf(zip_derived_cl12, plain, (![X0 : $i]: ((nf @ (lam @ X0)) = (nf @ X0))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_012])).
% 0.56/0.95 thf(zip_derived_cl12, plain, (![X0 : $i]: ((nf @ (lam @ X0)) = (nf @ X0))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_012])).
% 0.56/0.95 thf(axiom_013, axiom, (( nf @ ( var @ X4 ) ) = ( btrue ))).
% 0.56/0.95 thf(zip_derived_cl13, plain, (![X0 : $i]: ((nf @ (var @ X0)) = (btrue))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_013])).
% 0.56/0.95 thf(axiom_051, axiom, (( eq @ X @ X ) = ( btrue ))).
% 0.56/0.95 thf(zip_derived_cl51, plain, (![X0 : $i]: ((eq @ X0 @ X0) = (btrue))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_051])).
% 0.56/0.95 thf(axiom_007, axiom, (( andb @ btrue @ Q ) = ( Q ))).
% 0.56/0.95 thf(zip_derived_cl7, plain, (![X0 : $i]: ((andb @ btrue @ X0) = (X0))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_007])).
% 0.56/0.95 thf(axiom_002, axiom, (( notb @ btrue ) = ( bfalse ))).
% 0.56/0.95 thf(zip_derived_cl2, plain, (((notb @ btrue) = (bfalse))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_002])).
% 0.56/0.95 thf(zip_derived_cl1170, plain,
% 0.56/0.95 (((sat_synth_nf_k @ (lam @ (lam @ (var @ zero)))) = (bfalse))),
% 0.56/0.95 inference('demod', [status(thm)],
% 0.56/0.95 [zip_derived_cl1151, zip_derived_cl12, zip_derived_cl12,
% 0.56/0.95 zip_derived_cl13, zip_derived_cl51, zip_derived_cl7,
% 0.56/0.95 zip_derived_cl2])).
% 0.56/0.95 thf(goal, conjecture,
% 0.56/0.95 (( eq4 @ ( sat_synth_nf_k @ X ) @ bfalse ) = ( btrue ))).
% 0.56/0.95 thf(zf_stmt_0, negated_conjecture,
% 0.56/0.95 (( eq4 @ ( sat_synth_nf_k @ X ) @ bfalse ) != ( btrue )),
% 0.56/0.95 inference('cnf.neg', [status(esa)], [goal])).
% 0.56/0.95 thf(zip_derived_cl55, plain,
% 0.56/0.95 (![X0 : $i]: ((eq4 @ (sat_synth_nf_k @ X0) @ bfalse) != (btrue))),
% 0.56/0.95 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.95 thf(zip_derived_cl1188, plain, (((eq4 @ bfalse @ bfalse) != (btrue))),
% 0.56/0.95 inference('sup-', [status(thm)], [zip_derived_cl1170, zip_derived_cl55])).
% 0.56/0.95 thf(axiom_054, axiom, (( eq4 @ X @ X ) = ( btrue ))).
% 0.56/0.95 thf(zip_derived_cl54, plain, (![X0 : $i]: ((eq4 @ X0 @ X0) = (btrue))),
% 0.56/0.95 inference('cnf', [status(esa)], [axiom_054])).
% 0.56/0.95 thf(zip_derived_cl1189, plain, (((btrue) != (btrue))),
% 0.56/0.95 inference('demod', [status(thm)], [zip_derived_cl1188, zip_derived_cl54])).
% 0.56/0.95 thf(zip_derived_cl1190, plain, ($false),
% 0.56/0.95 inference('simplify', [status(thm)], [zip_derived_cl1189])).
% 0.56/0.95
% 0.56/0.95 % SZS output end Refutation
% 0.56/0.95
% 0.56/0.95
% 0.56/0.95 % Terminating...
% 3.09/1.05 % Runner terminated.
% 3.09/1.07 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------