%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEG002^1 : 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.yLgkToQ0lv true
% Computer : n001.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:33:30 PM UTC 2025
% Result : Theorem 65.15s 8.87s
% Output : Refutation 65.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : GEG002^1 : TPTP v9.2.0. Released v4.1.0.
% 0.12/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yLgkToQ0lv true
% 0.14/0.37 % Computer : n001.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed Oct 1 11:14:08 EDT 2025
% 0.14/0.38 % CPUTime :
% 0.14/0.38 % Running portfolio for 300 s
% 0.14/0.38 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.38 % Number of cores: 8
% 0.14/0.38 % Python version: Python 3.6.8
% 0.14/0.38 % Running in HO mode
% 0.57/0.71 % Total configuration time : 828
% 0.57/0.71 % Estimated wc time : 1656
% 0.57/0.71 % Estimated cpu time (8 cpus) : 207.0
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.57/0.77 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.57/0.79 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.57/0.79 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.57/0.79 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.57/0.79 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.57/0.80 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 65.15/8.87 % Solved by lams/40_c_ic.sh.
% 65.15/8.87 % done 7403 iterations in 8.054s
% 65.15/8.87 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 65.15/8.87 % SZS output start Refutation
% 65.15/8.87 thf(reg_type, type, reg: $tType).
% 65.15/8.87 thf(zip_tseitin_5_type, type, zip_tseitin_5: reg > reg > $o).
% 65.15/8.87 thf(sk__10_type, type, sk__10: reg > reg).
% 65.15/8.87 thf(pp_type, type, pp: reg > reg > $o).
% 65.15/8.87 thf(sk__13_type, type, sk__13: reg > reg).
% 65.15/8.87 thf(zip_tseitin_3_type, type, zip_tseitin_3: reg > reg > $o).
% 65.15/8.87 thf(dc_type, type, dc: reg > reg > $o).
% 65.15/8.87 thf(tpp_type, type, tpp: reg > reg > $o).
% 65.15/8.87 thf(ec_type, type, ec: reg > reg > $o).
% 65.15/8.87 thf(catalunya_type, type, catalunya: reg).
% 65.15/8.87 thf(sk__14_type, type, sk__14: reg > reg).
% 65.15/8.87 thf(zip_tseitin_0_type, type, zip_tseitin_0: reg > reg > reg > $o).
% 65.15/8.87 thf(zip_tseitin_6_type, type, zip_tseitin_6: reg > reg > $o).
% 65.15/8.87 thf(zip_tseitin_2_type, type, zip_tseitin_2: reg > reg > reg > $o).
% 65.15/8.87 thf(zip_tseitin_4_type, type, zip_tseitin_4: reg > reg > $o).
% 65.15/8.87 thf(o_type, type, o: reg > reg > $o).
% 65.15/8.87 thf(p_type, type, p: reg > reg > $o).
% 65.15/8.87 thf(ntpp_type, type, ntpp: reg > reg > $o).
% 65.15/8.87 thf(zip_tseitin_7_type, type, zip_tseitin_7: reg > reg > $o).
% 65.15/8.87 thf(zip_tseitin_1_type, type, zip_tseitin_1: reg > reg > $o).
% 65.15/8.87 thf(c_type, type, c: reg > reg > $o).
% 65.15/8.87 thf(france_type, type, france: reg).
% 65.15/8.87 thf(spain_type, type, spain: reg).
% 65.15/8.87 thf(paris_type, type, paris: reg).
% 65.15/8.87 thf(sk__11_type, type, sk__11: reg > reg).
% 65.15/8.87 thf(ntpp, axiom,(( ntpp ) =
% 65.15/8.87 (^[X:reg,Y:reg]:
% 65.15/8.87 ( ( pp @ X @ Y ) & ( ~( ?[Z:reg]: ( ( ec @ Z @ Y ) & ( ec @ Z @ X ) ) ) ) )))).
% 65.15/8.87 thf(ec, axiom,(( ec ) =
% 65.15/8.87 (^[X:reg,Y:reg]: ( ( c @ X @ Y ) & ( ~( o @ X @ Y ) ) )))).
% 65.15/8.87 thf(o, axiom,(( o ) =
% 65.15/8.87 (^[X:reg,Y:reg]: ( ?[Z:reg]: ( ( p @ Z @ Y ) & ( p @ Z @ X ) ) )))).
% 65.15/8.87 thf(p, axiom,(( p ) =
% 65.15/8.87 (^[X:reg,Y:reg]: ( ![Z:reg]: ( ( c @ Z @ X ) => ( c @ Z @ Y ) ) )))).
% 65.15/8.87 thf('0', plain,
% 65.15/8.87 (( p ) =
% 65.15/8.87 ( ^[X:reg,Y:reg]: ( ![Z:reg]: ( ( c @ Z @ X ) => ( c @ Z @ Y ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [p])).
% 65.15/8.87 thf('1', plain,
% 65.15/8.87 (( p ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]:
% 65.15/8.87 ( ![X4:reg]: ( ( c @ X4 @ V_1 ) => ( c @ X4 @ V_2 ) ) ) )),
% 65.15/8.87 define([status(thm)])).
% 65.15/8.87 thf('2', plain,
% 65.15/8.87 (( o ) =
% 65.15/8.87 ( ^[X:reg,Y:reg]: ( ?[Z:reg]: ( ( p @ Z @ Y ) & ( p @ Z @ X ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [o, '1'])).
% 65.15/8.87 thf('3', plain,
% 65.15/8.87 (( o ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]:
% 65.15/8.87 ( ?[X4:reg]: ( ( p @ X4 @ V_2 ) & ( p @ X4 @ V_1 ) ) ) )),
% 65.15/8.87 define([status(thm)])).
% 65.15/8.87 thf('4', plain,
% 65.15/8.87 (( ec ) = ( ^[X:reg,Y:reg]: ( ( c @ X @ Y ) & ( ~( o @ X @ Y ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [ec, '3', '1'])).
% 65.15/8.87 thf('5', plain,
% 65.15/8.87 (( ec ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]: ( ( c @ V_1 @ V_2 ) & ( ~( o @ V_1 @ V_2 ) ) ) )),
% 65.15/8.87 define([status(thm)])).
% 65.15/8.87 thf('6', plain,
% 65.15/8.87 (( ntpp ) =
% 65.15/8.87 ( ^[X:reg,Y:reg]:
% 65.15/8.87 ( ( pp @ X @ Y ) &
% 65.15/8.87 ( ~( ?[Z:reg]: ( ( ec @ Z @ Y ) & ( ec @ Z @ X ) ) ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [ntpp, '5', '3', '1'])).
% 65.15/8.87 thf('7', plain,
% 65.15/8.87 (( ntpp ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]:
% 65.15/8.87 ( ( pp @ V_1 @ V_2 ) &
% 65.15/8.87 ( ~( ?[X4:reg]: ( ( ec @ X4 @ V_2 ) & ( ec @ X4 @ V_1 ) ) ) ) ) )),
% 65.15/8.87 define([status(thm)])).
% 65.15/8.87 thf(pp, axiom,(( pp ) =
% 65.15/8.87 (^[X:reg,Y:reg]: ( ( p @ X @ Y ) & ( ~( p @ Y @ X ) ) )))).
% 65.15/8.87 thf('8', plain,
% 65.15/8.87 (( pp ) = ( ^[X:reg,Y:reg]: ( ( p @ X @ Y ) & ( ~( p @ Y @ X ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [pp, '1'])).
% 65.15/8.87 thf('9', plain,
% 65.15/8.87 (( pp ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]: ( ( p @ V_1 @ V_2 ) & ( ~( p @ V_2 @ V_1 ) ) ) )),
% 65.15/8.87 define([status(thm)])).thf(ax3, axiom, (ntpp @ paris @ france)).
% 65.15/8.87 thf(zf_stmt_0, axiom,
% 65.15/8.87 (( ~( ?[X8:reg]:
% 65.15/8.87 ( ( ~( ?[X16:reg]:
% 65.15/8.87 ( ( ![X20:reg]: ( ( c @ X20 @ X16 ) => ( c @ X20 @ X8 ) ) ) &
% 65.15/8.87 ( ![X18:reg]: ( ( c @ X18 @ X16 ) => ( c @ X18 @ paris ) ) ) ) ) ) &
% 65.15/8.87 ( c @ X8 @ paris ) &
% 65.15/8.87 ( ~( ?[X10:reg]:
% 65.15/8.87 ( ( ![X14:reg]: ( ( c @ X14 @ X10 ) => ( c @ X14 @ X8 ) ) ) &
% 65.15/8.87 ( ![X12:reg]: ( ( c @ X12 @ X10 ) => ( c @ X12 @ france ) ) ) ) ) ) &
% 65.15/8.87 ( c @ X8 @ france ) ) ) ) &
% 65.15/8.87 ( ~( ![X6:reg]: ( ( c @ X6 @ france ) => ( c @ X6 @ paris ) ) ) ) &
% 65.15/8.87 ( ![X4:reg]: ( ( c @ X4 @ paris ) => ( c @ X4 @ france ) ) ))).
% 65.15/8.87 thf(zf_stmt_1, axiom,
% 65.15/8.87 (![X10:reg,X8:reg]:
% 65.15/8.87 ( ( zip_tseitin_7 @ X10 @ X8 ) =>
% 65.15/8.87 ( ( ![X12:reg]: ( ( c @ X12 @ X10 ) => ( c @ X12 @ france ) ) ) &
% 65.15/8.87 ( ![X14:reg]: ( ( c @ X14 @ X10 ) => ( c @ X14 @ X8 ) ) ) ) ))).
% 65.15/8.87 thf(zip_derived_cl25, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ france) | ~ (zip_tseitin_7 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_1])).
% 65.15/8.87 thf(c_symmetric, axiom, (![X:reg,Y:reg]: ( ( c @ X @ Y ) => ( c @ Y @ X ) ))).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zip_derived_cl25, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ france) | ~ (zip_tseitin_7 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_1])).
% 65.15/8.87 thf(zip_derived_cl219, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | ~ (zip_tseitin_7 @ X0 @ X2) | (c @ X1 @ france))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl25])).
% 65.15/8.87 thf(zip_derived_cl26, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ X2) | ~ (zip_tseitin_7 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_1])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zip_derived_cl26, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ X2) | ~ (zip_tseitin_7 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_1])).
% 65.15/8.87 thf(zip_derived_cl295, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | ~ (zip_tseitin_7 @ X0 @ X2) | (c @ X1 @ X2))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl26])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(dc, axiom,(( dc ) = (^[X:reg,Y:reg]: ( ~( c @ X @ Y ) )))).
% 65.15/8.87 thf('10', plain, (( dc ) = ( ^[X:reg,Y:reg]: ( ~( c @ X @ Y ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [dc])).
% 65.15/8.87 thf('11', plain, (( dc ) = ( ^[V_1:reg,V_2:reg]: ( ~( c @ V_1 @ V_2 ) ) )),
% 65.15/8.87 define([status(thm)])).
% 65.15/8.87 thf(con, conjecture, (( dc @ spain @ paris ) & ( dc @ catalunya @ paris ))).
% 65.15/8.87 thf(zf_stmt_2, conjecture,
% 65.15/8.87 (( ~( c @ catalunya @ paris ) ) & ( ~( c @ spain @ paris ) ))).
% 65.15/8.87 thf(zf_stmt_3, negated_conjecture,
% 65.15/8.87 (~( ( ~( c @ catalunya @ paris ) ) & ( ~( c @ spain @ paris ) ) )),
% 65.15/8.87 inference('cnf.neg', [status(esa)], [zf_stmt_2])).
% 65.15/8.87 thf(zip_derived_cl31, plain,
% 65.15/8.87 (( (c @ catalunya @ paris) | (c @ spain @ paris))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_3])).
% 65.15/8.87 thf(zip_derived_cl44, plain,
% 65.15/8.87 (( (c @ paris @ catalunya) | (c @ spain @ paris))),
% 65.15/8.87 inference('sup+', [status(thm)], [zip_derived_cl1, zip_derived_cl31])).
% 65.15/8.87 thf(tpp, axiom,(( tpp ) =
% 65.15/8.87 (^[X:reg,Y:reg]:
% 65.15/8.87 ( ( pp @ X @ Y ) & ( ?[Z:reg]: ( ( ec @ Z @ Y ) & ( ec @ Z @ X ) ) ) )))).
% 65.15/8.87 thf('12', plain,
% 65.15/8.87 (( tpp ) =
% 65.15/8.87 ( ^[X:reg,Y:reg]:
% 65.15/8.87 ( ( pp @ X @ Y ) & ( ?[Z:reg]: ( ( ec @ Z @ Y ) & ( ec @ Z @ X ) ) ) ) )),
% 65.15/8.87 inference('simplify_rw_rule', [status(thm)], [tpp, '5', '3', '1'])).
% 65.15/8.87 thf('13', plain,
% 65.15/8.87 (( tpp ) =
% 65.15/8.87 ( ^[V_1:reg,V_2:reg]:
% 65.15/8.87 ( ( pp @ V_1 @ V_2 ) &
% 65.15/8.87 ( ?[X4:reg]: ( ( ec @ X4 @ V_2 ) & ( ec @ X4 @ V_1 ) ) ) ) )),
% 65.15/8.87 define([status(thm)])).thf(ax1, axiom, (tpp @ catalunya @ spain)).
% 65.15/8.87 thf(zf_stmt_4, axiom,
% 65.15/8.87 (( ?[X8:reg]:
% 65.15/8.87 ( ( ~( ?[X16:reg]:
% 65.15/8.87 ( ( ![X20:reg]: ( ( c @ X20 @ X16 ) => ( c @ X20 @ X8 ) ) ) &
% 65.15/8.87 ( ![X18:reg]: ( ( c @ X18 @ X16 ) => ( c @ X18 @ catalunya ) ) ) ) ) ) &
% 65.15/8.87 ( c @ X8 @ catalunya ) &
% 65.15/8.87 ( ~( ?[X10:reg]:
% 65.15/8.87 ( ( ![X14:reg]: ( ( c @ X14 @ X10 ) => ( c @ X14 @ X8 ) ) ) &
% 65.15/8.87 ( ![X12:reg]: ( ( c @ X12 @ X10 ) => ( c @ X12 @ spain ) ) ) ) ) ) &
% 65.15/8.87 ( c @ X8 @ spain ) ) ) &
% 65.15/8.87 ( ~( ![X6:reg]: ( ( c @ X6 @ spain ) => ( c @ X6 @ catalunya ) ) ) ) &
% 65.15/8.87 ( ![X4:reg]: ( ( c @ X4 @ catalunya ) => ( c @ X4 @ spain ) ) ))).
% 65.15/8.87 thf(zf_stmt_5, type, zip_tseitin_3 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_6, axiom,
% 65.15/8.87 (![X12:reg,X10:reg]:
% 65.15/8.87 ( ( ( c @ X12 @ X10 ) => ( c @ X12 @ spain ) ) =>
% 65.15/8.87 ( zip_tseitin_3 @ X12 @ X10 ) ))).
% 65.15/8.87 thf(zf_stmt_7, type, zip_tseitin_2 : reg > reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_8, axiom,
% 65.15/8.87 (![X14:reg,X10:reg,X8:reg]:
% 65.15/8.87 ( ( ( c @ X14 @ X10 ) => ( c @ X14 @ X8 ) ) =>
% 65.15/8.87 ( zip_tseitin_2 @ X14 @ X10 @ X8 ) ))).
% 65.15/8.87 thf(zf_stmt_9, type, zip_tseitin_1 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_10, axiom,
% 65.15/8.87 (![X18:reg,X16:reg]:
% 65.15/8.87 ( ( ( c @ X18 @ X16 ) => ( c @ X18 @ catalunya ) ) =>
% 65.15/8.87 ( zip_tseitin_1 @ X18 @ X16 ) ))).
% 65.15/8.87 thf(zf_stmt_11, type, zip_tseitin_0 : reg > reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_12, axiom,
% 65.15/8.87 (![X20:reg,X16:reg,X8:reg]:
% 65.15/8.87 ( ( ( c @ X20 @ X16 ) => ( c @ X20 @ X8 ) ) =>
% 65.15/8.87 ( zip_tseitin_0 @ X20 @ X16 @ X8 ) ))).
% 65.15/8.87 thf(zf_stmt_13, axiom,
% 65.15/8.87 (( ![X4:reg]: ( ( c @ X4 @ catalunya ) => ( c @ X4 @ spain ) ) ) &
% 65.15/8.87 ( ~( ![X6:reg]: ( ( c @ X6 @ spain ) => ( c @ X6 @ catalunya ) ) ) ) &
% 65.15/8.87 ( ?[X8:reg]:
% 65.15/8.87 ( ( c @ X8 @ spain ) &
% 65.15/8.87 ( ~( ?[X10:reg]:
% 65.15/8.87 ( ( ![X12:reg]: ( zip_tseitin_3 @ X12 @ X10 ) ) &
% 65.15/8.87 ( ![X14:reg]: ( zip_tseitin_2 @ X14 @ X10 @ X8 ) ) ) ) ) &
% 65.15/8.87 ( c @ X8 @ catalunya ) &
% 65.15/8.87 ( ~( ?[X16:reg]:
% 65.15/8.87 ( ( ![X18:reg]: ( zip_tseitin_1 @ X18 @ X16 ) ) &
% 65.15/8.87 ( ![X20:reg]: ( zip_tseitin_0 @ X20 @ X16 @ X8 ) ) ) ) ) ) ))).
% 65.15/8.87 thf(zip_derived_cl16, plain,
% 65.15/8.87 (![X0 : reg]: ( (c @ X0 @ spain) | ~ (c @ X0 @ catalunya))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_13])).
% 65.15/8.87 thf(zip_derived_cl86, plain, (( (c @ spain @ paris) | (c @ paris @ spain))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl16])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zip_derived_cl94, plain, ( (c @ paris @ spain)),
% 65.15/8.87 inference('clc', [status(thm)], [zip_derived_cl86, zip_derived_cl1])).
% 65.15/8.87 thf(ax2, axiom, (ec @ spain @ france)).
% 65.15/8.87 thf(zf_stmt_14, axiom,
% 65.15/8.87 (( ~( ?[X4:reg]:
% 65.15/8.87 ( ( ![X8:reg]: ( ( c @ X8 @ X4 ) => ( c @ X8 @ spain ) ) ) &
% 65.15/8.87 ( ![X6:reg]: ( ( c @ X6 @ X4 ) => ( c @ X6 @ france ) ) ) ) ) ) &
% 65.15/8.87 ( c @ spain @ france ))).
% 65.15/8.87 thf(zf_stmt_15, axiom,
% 65.15/8.87 (![X6:reg,X4:reg]:
% 65.15/8.87 ( ( ( c @ X6 @ X4 ) => ( c @ X6 @ france ) ) =>
% 65.15/8.87 ( zip_tseitin_5 @ X6 @ X4 ) ))).
% 65.15/8.87 thf(zip_derived_cl20, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (zip_tseitin_5 @ X0 @ X1) | (c @ X0 @ X1))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_15])).
% 65.15/8.87 thf(zf_stmt_16, type, zip_tseitin_5 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_17, type, zip_tseitin_4 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_18, axiom,
% 65.15/8.87 (![X8:reg,X4:reg]:
% 65.15/8.87 ( ( ( c @ X8 @ X4 ) => ( c @ X8 @ spain ) ) => ( zip_tseitin_4 @ X8 @ X4 ) ))).
% 65.15/8.87 thf(zf_stmt_19, axiom,
% 65.15/8.87 (( c @ spain @ france ) &
% 65.15/8.87 ( ~( ?[X4:reg]:
% 65.15/8.87 ( ( ![X6:reg]: ( zip_tseitin_5 @ X6 @ X4 ) ) &
% 65.15/8.87 ( ![X8:reg]: ( zip_tseitin_4 @ X8 @ X4 ) ) ) ) ))).
% 65.15/8.87 thf(zip_derived_cl21, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 (~ (zip_tseitin_5 @ (sk__10 @ X0) @ X0)
% 65.15/8.87 | ~ (zip_tseitin_4 @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_19])).
% 65.15/8.87 thf(zip_derived_cl261, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 ( (c @ (sk__10 @ X0) @ X0) | ~ (zip_tseitin_4 @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl21])).
% 65.15/8.87 thf(zip_derived_cl17, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (zip_tseitin_4 @ X0 @ X1) | ~ (c @ X0 @ spain))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_18])).
% 65.15/8.87 thf(zip_derived_cl1070, plain,
% 65.15/8.87 (![X0 : reg]: ( (c @ (sk__10 @ X0) @ X0) | ~ (c @ (sk__11 @ X0) @ spain))),
% 65.15/8.87 inference('sup+', [status(thm)], [zip_derived_cl261, zip_derived_cl17])).
% 65.15/8.87 thf(zip_derived_cl17, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (zip_tseitin_4 @ X0 @ X1) | ~ (c @ X0 @ spain))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_18])).
% 65.15/8.87 thf(zip_derived_cl261, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 ( (c @ (sk__10 @ X0) @ X0) | ~ (zip_tseitin_4 @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl21])).
% 65.15/8.87 thf(zip_derived_cl18, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (zip_tseitin_4 @ X0 @ X1) | (c @ X0 @ X1))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_18])).
% 65.15/8.87 thf(zip_derived_cl1069, plain,
% 65.15/8.87 (![X0 : reg]: ( (c @ (sk__10 @ X0) @ X0) | (c @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('sup+', [status(thm)], [zip_derived_cl261, zip_derived_cl18])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zf_stmt_20, axiom,
% 65.15/8.87 (![X16:reg,X8:reg]:
% 65.15/8.87 ( ( zip_tseitin_6 @ X16 @ X8 ) =>
% 65.15/8.87 ( ( ![X18:reg]: ( ( c @ X18 @ X16 ) => ( c @ X18 @ paris ) ) ) &
% 65.15/8.87 ( ![X20:reg]: ( ( c @ X20 @ X16 ) => ( c @ X20 @ X8 ) ) ) ) ))).
% 65.15/8.87 thf(zip_derived_cl24, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ X2) | ~ (zip_tseitin_6 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_20])).
% 65.15/8.87 thf(zip_derived_cl189, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | ~ (zip_tseitin_6 @ X0 @ X2) | (c @ X1 @ X2))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl24])).
% 65.15/8.87 thf(zip_derived_cl24, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ X2) | ~ (zip_tseitin_6 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_20])).
% 65.15/8.87 thf(zf_stmt_21, type, zip_tseitin_7 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_22, type, zip_tseitin_6 : reg > reg > $o).
% 65.15/8.87 thf(zf_stmt_23, axiom,
% 65.15/8.87 (( ![X4:reg]: ( ( c @ X4 @ paris ) => ( c @ X4 @ france ) ) ) &
% 65.15/8.87 ( ~( ![X6:reg]: ( ( c @ X6 @ france ) => ( c @ X6 @ paris ) ) ) ) &
% 65.15/8.87 ( ~( ?[X8:reg]:
% 65.15/8.87 ( ( c @ X8 @ france ) &
% 65.15/8.87 ( ~( ?[X10:reg]: ( zip_tseitin_7 @ X10 @ X8 ) ) ) &
% 65.15/8.87 ( c @ X8 @ paris ) &
% 65.15/8.87 ( ~( ?[X16:reg]: ( zip_tseitin_6 @ X16 @ X8 ) ) ) ) ) ))).
% 65.15/8.87 thf(zip_derived_cl30, plain,
% 65.15/8.87 (![X0 : reg]: ( (c @ X0 @ france) | ~ (c @ X0 @ paris))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_23])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zip_derived_cl27, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 (~ (c @ X0 @ france)
% 65.15/8.87 | (zip_tseitin_7 @ (sk__13 @ X0) @ X0)
% 65.15/8.87 | ~ (c @ X0 @ paris)
% 65.15/8.87 | (zip_tseitin_6 @ (sk__14 @ X0) @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_23])).
% 65.15/8.87 thf(zip_derived_cl30, plain,
% 65.15/8.87 (![X0 : reg]: ( (c @ X0 @ france) | ~ (c @ X0 @ paris))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_23])).
% 65.15/8.87 thf(zip_derived_cl327, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 ( (zip_tseitin_6 @ (sk__14 @ X0) @ X0)
% 65.15/8.87 | ~ (c @ X0 @ paris)
% 65.15/8.87 | (zip_tseitin_7 @ (sk__13 @ X0) @ X0))),
% 65.15/8.87 inference('clc', [status(thm)], [zip_derived_cl27, zip_derived_cl30])).
% 65.15/8.87 thf(zip_derived_cl330, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 (~ (c @ paris @ X0)
% 65.15/8.87 | (zip_tseitin_7 @ (sk__13 @ X0) @ X0)
% 65.15/8.87 | (zip_tseitin_6 @ (sk__14 @ X0) @ X0))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl327])).
% 65.15/8.87 thf(zip_derived_cl23, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg, X2 : reg]:
% 65.15/8.87 (~ (c @ X0 @ X1) | (c @ X0 @ paris) | ~ (zip_tseitin_6 @ X1 @ X2))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_20])).
% 65.15/8.87 thf(zip_derived_cl18, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (zip_tseitin_4 @ X0 @ X1) | (c @ X0 @ X1))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_18])).
% 65.15/8.87 thf(zip_derived_cl1, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]: ( (c @ X0 @ X1) | ~ (c @ X1 @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [c_symmetric])).
% 65.15/8.87 thf(zip_derived_cl19, plain,
% 65.15/8.87 (![X0 : reg, X1 : reg]:
% 65.15/8.87 ( (zip_tseitin_5 @ X0 @ X1) | ~ (c @ X0 @ france))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_15])).
% 65.15/8.87 thf(zip_derived_cl21, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 (~ (zip_tseitin_5 @ (sk__10 @ X0) @ X0)
% 65.15/8.87 | ~ (zip_tseitin_4 @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('cnf', [status(esa)], [zf_stmt_19])).
% 65.15/8.87 thf(zip_derived_cl262, plain,
% 65.15/8.87 (![X0 : reg]:
% 65.15/8.87 (~ (c @ (sk__10 @ X0) @ france)
% 65.15/8.87 | ~ (zip_tseitin_4 @ (sk__11 @ X0) @ X0))),
% 65.15/8.87 inference('sup-', [status(thm)], [zip_derived_cl19, zip_derived_cl21])).
% 65.15/8.87 thf(zip_derived_cl17551, plain, ($false),
% 65.15/8.87 inference('eprover', [status(thm)],
% 65.15/8.87 [zip_derived_cl25, zip_derived_cl219, zip_derived_cl26,
% 65.15/8.87 zip_derived_cl295, zip_derived_cl94, zip_derived_cl1070,
% 65.15/8.87 zip_derived_cl17, zip_derived_cl1069, zip_derived_cl189,
% 65.15/8.87 zip_derived_cl24, zip_derived_cl30, zip_derived_cl330,
% 65.15/8.87 zip_derived_cl23, zip_derived_cl18, zip_derived_cl1,
% 65.15/8.87 zip_derived_cl262])).
% 65.15/8.87
% 65.15/8.87 % SZS output end Refutation
% 65.15/8.87
% 65.15/8.87
% 65.15/8.87 % Terminating...
% 65.15/8.92 % Runner terminated.
% 65.15/8.93 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------