%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : KRS116+1 : TPTP v9.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.vsrWtiZhY8 true
% Computer : n027.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:40:37 PM UTC 2025
% Result : Unsatisfiable 0.59s 0.79s
% Output : Refutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS116+1 : TPTP v9.2.0. Released v3.1.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.vsrWtiZhY8 true
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 11:52:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.56/0.64 % Total configuration time : 435
% 0.56/0.64 % Estimated wc time : 1092
% 0.56/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.58/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.58/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.58/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.58/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.59/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.59/0.79 % Solved by fo/fo6_bce.sh.
% 0.59/0.79 % BCE start: 58
% 0.59/0.79 % BCE eliminated: 1
% 0.59/0.79 % PE start: 57
% 0.59/0.79 logic: neq
% 0.59/0.79 % PE eliminated: 16
% 0.59/0.79 % done 74 iterations in 0.040s
% 0.59/0.79 % SZS status Unsatisfiable for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.59/0.79 % SZS output start Refutation
% 0.59/0.79 thf(ca_type, type, ca: $i > $o).
% 0.59/0.79 thf(cc_type, type, cc: $i > $o).
% 0.59/0.79 thf(cowlThing_type, type, cowlThing: $i > $o).
% 0.59/0.79 thf(sk__10_type, type, sk__10: $i > $i).
% 0.59/0.79 thf(sk__type, type, sk_: $i > $i).
% 0.59/0.79 thf(caxcomp_type, type, caxcomp: $i > $o).
% 0.59/0.79 thf(ca_Vx5_type, type, ca_Vx5: $i > $o).
% 0.59/0.79 thf(ca_Vx6_type, type, ca_Vx6: $i > $o).
% 0.59/0.79 thf(rinvR_type, type, rinvR: $i > $i > $o).
% 0.59/0.79 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 0.59/0.79 thf(i2003_11_14_17_21_33997_type, type, i2003_11_14_17_21_33997: $i).
% 0.59/0.79 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 0.59/0.79 thf(ca_Vx4_type, type, ca_Vx4: $i > $o).
% 0.59/0.79 thf(sk__9_type, type, sk__9: $i > $i).
% 0.59/0.79 thf(rr_type, type, rr: $i > $i > $o).
% 0.59/0.79 thf(rinvS_type, type, rinvS: $i > $i > $o).
% 0.59/0.79 thf(ca_Vx7_type, type, ca_Vx7: $i > $o).
% 0.59/0.79 thf(sk__2_type, type, sk__2: $i > $i).
% 0.59/0.79 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $o).
% 0.59/0.79 thf(rp_type, type, rp: $i > $i > $o).
% 0.59/0.79 thf(ca_Ax2_type, type, ca_Ax2: $i > $o).
% 0.59/0.79 thf(cUnsatisfiable_type, type, cUnsatisfiable: $i > $o).
% 0.59/0.79 thf(ra_Px1_type, type, ra_Px1: $i > $i > $o).
% 0.59/0.79 thf(ca_Vx3_type, type, ca_Vx3: $i > $o).
% 0.59/0.79 thf(rinvP_type, type, rinvP: $i > $i > $o).
% 0.59/0.79 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $o).
% 0.59/0.79 thf(rs_type, type, rs: $i > $i > $o).
% 0.59/0.79 thf(axiom_7, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Ax2 @ X ) <=>
% 0.59/0.79 ( ( ![Y:$i]: ( ( rp @ X @ Y ) => ( ca_Vx4 @ Y ) ) ) &
% 0.59/0.79 ( ?[Y:$i]: ( ( rp @ X @ Y ) & ( cowlThing @ Y ) ) ) &
% 0.59/0.79 ( ?[Y:$i]: ( ( rr @ X @ Y ) & ( cowlThing @ Y ) ) ) &
% 0.59/0.79 ( ![Y:$i]: ( ( rr @ X @ Y ) => ( cc @ Y ) ) ) &
% 0.59/0.79 ( ![Y:$i]: ( ( rp @ X @ Y ) => ( ca_Vx5 @ Y ) ) ) &
% 0.59/0.79 ( ![Y:$i]: ( ( rp @ X @ Y ) => ( ca_Vx3 @ Y ) ) ) ) ))).
% 0.59/0.79 thf(zf_stmt_0, type, zip_tseitin_3 : $i > $i > $o).
% 0.59/0.79 thf(zf_stmt_1, axiom,
% 0.59/0.79 (![Y:$i,X:$i]:
% 0.59/0.79 ( ( zip_tseitin_3 @ Y @ X ) <=> ( ( rp @ X @ Y ) => ( ca_Vx3 @ Y ) ) ))).
% 0.59/0.79 thf(zf_stmt_2, type, zip_tseitin_2 : $i > $i > $o).
% 0.59/0.79 thf(zf_stmt_3, axiom,
% 0.59/0.79 (![Y:$i,X:$i]:
% 0.59/0.79 ( ( zip_tseitin_2 @ Y @ X ) <=> ( ( rp @ X @ Y ) => ( ca_Vx5 @ Y ) ) ))).
% 0.59/0.79 thf(zf_stmt_4, type, zip_tseitin_1 : $i > $i > $o).
% 0.59/0.79 thf(zf_stmt_5, axiom,
% 0.59/0.79 (![Y:$i,X:$i]:
% 0.59/0.79 ( ( zip_tseitin_1 @ Y @ X ) <=> ( ( rr @ X @ Y ) => ( cc @ Y ) ) ))).
% 0.59/0.79 thf(zf_stmt_6, type, zip_tseitin_0 : $i > $i > $o).
% 0.59/0.79 thf(zf_stmt_7, axiom,
% 0.59/0.79 (![Y:$i,X:$i]:
% 0.59/0.79 ( ( zip_tseitin_0 @ Y @ X ) <=> ( ( rp @ X @ Y ) => ( ca_Vx4 @ Y ) ) ))).
% 0.59/0.79 thf(zf_stmt_8, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Ax2 @ X ) <=>
% 0.59/0.79 ( ( ![Y:$i]: ( zip_tseitin_3 @ Y @ X ) ) &
% 0.59/0.79 ( ![Y:$i]: ( zip_tseitin_2 @ Y @ X ) ) &
% 0.59/0.79 ( ![Y:$i]: ( zip_tseitin_1 @ Y @ X ) ) &
% 0.59/0.79 ( ?[Y:$i]: ( ( cowlThing @ Y ) & ( rr @ X @ Y ) ) ) &
% 0.59/0.79 ( ?[Y:$i]: ( ( cowlThing @ Y ) & ( rp @ X @ Y ) ) ) &
% 0.59/0.79 ( ![Y:$i]: ( zip_tseitin_0 @ Y @ X ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl31, plain,
% 0.59/0.79 (![X0 : $i]: ( (rp @ X0 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.59/0.79 thf(zip_derived_cl23, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rp @ X0 @ X1) | (ca_Vx3 @ X1) | ~ (zip_tseitin_3 @ X1 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.59/0.79 thf(zip_derived_cl222, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Ax2 @ X0)
% 0.59/0.79 | (ca_Vx3 @ (sk__9 @ X0))
% 0.59/0.79 | ~ (zip_tseitin_3 @ (sk__9 @ X0) @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl23])).
% 0.59/0.79 thf(zip_derived_cl26, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: ( (zip_tseitin_3 @ X0 @ X1) | ~ (ca_Ax2 @ X1))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.59/0.79 thf(zip_derived_cl287, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Vx3 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('clc', [status(thm)], [zip_derived_cl222, zip_derived_cl26])).
% 0.59/0.79 thf(zip_derived_cl31, plain,
% 0.59/0.79 (![X0 : $i]: ( (rp @ X0 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.59/0.79 thf(zip_derived_cl20, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rp @ X0 @ X1) | (ca_Vx5 @ X1) | ~ (zip_tseitin_2 @ X1 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.59/0.79 thf(zip_derived_cl221, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Ax2 @ X0)
% 0.59/0.79 | (ca_Vx5 @ (sk__9 @ X0))
% 0.59/0.79 | ~ (zip_tseitin_2 @ (sk__9 @ X0) @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl20])).
% 0.59/0.79 thf(zip_derived_cl27, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: ( (zip_tseitin_2 @ X0 @ X1) | ~ (ca_Ax2 @ X1))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.59/0.79 thf(zip_derived_cl275, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Vx5 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('clc', [status(thm)], [zip_derived_cl221, zip_derived_cl27])).
% 0.59/0.79 thf(axiom_8, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Vx3 @ X ) <=> ( ?[Y:$i]: ( ( cowlThing @ Y ) & ( rr @ X @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl36, plain,
% 0.59/0.79 (![X0 : $i]: ( (rr @ X0 @ (sk__10 @ X0)) | ~ (ca_Vx3 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_8])).
% 0.59/0.79 thf(axiom_10, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Vx5 @ X ) <=> ( ![Y:$i]: ( ( rr @ X @ Y ) => ( cc @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl41, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: (~ (rr @ X0 @ X1) | (cc @ X1) | ~ (ca_Vx5 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_10])).
% 0.59/0.79 thf(zip_derived_cl227, plain,
% 0.59/0.79 (![X0 : $i]: (~ (ca_Vx3 @ X0) | (cc @ (sk__10 @ X0)) | ~ (ca_Vx5 @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl36, zip_derived_cl41])).
% 0.59/0.79 thf(zip_derived_cl36, plain,
% 0.59/0.79 (![X0 : $i]: ( (rr @ X0 @ (sk__10 @ X0)) | ~ (ca_Vx3 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_8])).
% 0.59/0.79 thf(axiom_14, axiom,
% 0.59/0.79 (![X:$i,Y:$i]: ( ( rinvR @ X @ Y ) <=> ( rr @ Y @ X ) ))).
% 0.59/0.79 thf(zip_derived_cl53, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: ( (rinvR @ X0 @ X1) | ~ (rr @ X1 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_14])).
% 0.59/0.79 thf(axiom_6, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( cc @ X ) <=> ( ![Y:$i]: ( ( rinvR @ X @ Y ) => ( ca_Vx7 @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl11, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rinvR @ X0 @ X1) | (ca_Vx7 @ X1) | ~ (cc @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_6])).
% 0.59/0.79 thf(zip_derived_cl80, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: (~ (rr @ X1 @ X0) | ~ (cc @ X0) | (ca_Vx7 @ X1))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl53, zip_derived_cl11])).
% 0.59/0.79 thf(zip_derived_cl229, plain,
% 0.59/0.79 (![X0 : $i]: (~ (ca_Vx3 @ X0) | ~ (cc @ (sk__10 @ X0)) | (ca_Vx7 @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl36, zip_derived_cl80])).
% 0.59/0.79 thf(zip_derived_cl258, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Vx5 @ X0) | ~ (ca_Vx3 @ X0) | ~ (ca_Vx3 @ X0) | (ca_Vx7 @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl227, zip_derived_cl229])).
% 0.59/0.79 thf(zip_derived_cl259, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Vx7 @ X0) | ~ (ca_Vx3 @ X0) | ~ (ca_Vx5 @ X0))),
% 0.59/0.79 inference('simplify', [status(thm)], [zip_derived_cl258])).
% 0.59/0.79 thf(zip_derived_cl276, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Ax2 @ X0)
% 0.59/0.79 | (ca_Vx7 @ (sk__9 @ X0))
% 0.59/0.79 | ~ (ca_Vx3 @ (sk__9 @ X0)))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl275, zip_derived_cl259])).
% 0.59/0.79 thf(zip_derived_cl288, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Ax2 @ X0) | ~ (ca_Ax2 @ X0) | (ca_Vx7 @ (sk__9 @ X0)))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl276])).
% 0.59/0.79 thf(zip_derived_cl289, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Vx7 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('simplify', [status(thm)], [zip_derived_cl288])).
% 0.59/0.79 thf(zip_derived_cl31, plain,
% 0.59/0.79 (![X0 : $i]: ( (rp @ X0 @ (sk__9 @ X0)) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.59/0.79 thf(axiom_13, axiom,
% 0.59/0.79 (![X:$i,Y:$i]: ( ( rinvP @ X @ Y ) <=> ( rp @ Y @ X ) ))).
% 0.59/0.79 thf(zip_derived_cl51, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: ( (rinvP @ X0 @ X1) | ~ (rp @ X1 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_13])).
% 0.59/0.79 thf(axiom_12, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Vx7 @ X ) <=> ( ![Y:$i]: ( ( rinvP @ X @ Y ) => ( ca_Vx6 @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl47, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rinvP @ X0 @ X1) | (ca_Vx6 @ X1) | ~ (ca_Vx7 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_12])).
% 0.59/0.79 thf(zip_derived_cl82, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rp @ X1 @ X0) | ~ (ca_Vx7 @ X0) | (ca_Vx6 @ X1))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl51, zip_derived_cl47])).
% 0.59/0.79 thf(zip_derived_cl224, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (ca_Ax2 @ X0) | ~ (ca_Vx7 @ (sk__9 @ X0)) | (ca_Vx6 @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl82])).
% 0.59/0.79 thf(zip_derived_cl290, plain,
% 0.59/0.79 (![X0 : $i]: (~ (ca_Ax2 @ X0) | ~ (ca_Ax2 @ X0) | (ca_Vx6 @ X0))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl289, zip_derived_cl224])).
% 0.59/0.79 thf(zip_derived_cl291, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Vx6 @ X0) | ~ (ca_Ax2 @ X0))),
% 0.59/0.79 inference('simplify', [status(thm)], [zip_derived_cl290])).
% 0.59/0.79 thf(axiom_17, axiom, (cUnsatisfiable @ i2003_11_14_17_21_33997)).
% 0.59/0.79 thf(zip_derived_cl57, plain, ( (cUnsatisfiable @ i2003_11_14_17_21_33997)),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_17])).
% 0.59/0.79 thf(axiom_3, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( cUnsatisfiable @ X ) =>
% 0.59/0.79 ( ?[Y:$i]: ( ( ca_Ax2 @ Y ) & ( rs @ X @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl6, plain,
% 0.59/0.79 (![X0 : $i]: ( (rs @ X0 @ (sk_ @ X0)) | ~ (cUnsatisfiable @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_3])).
% 0.59/0.79 thf(axiom_15, axiom,
% 0.59/0.79 (![X:$i,Y:$i]: ( ( rinvS @ X @ Y ) <=> ( rs @ Y @ X ) ))).
% 0.59/0.79 thf(zip_derived_cl55, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: ( (rinvS @ X0 @ X1) | ~ (rs @ X1 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_15])).
% 0.59/0.79 thf(zip_derived_cl74, plain,
% 0.59/0.79 (![X0 : $i]: (~ (cUnsatisfiable @ X0) | (rinvS @ (sk_ @ X0) @ X0))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl6, zip_derived_cl55])).
% 0.59/0.79 thf(axiom_11, axiom,
% 0.59/0.79 (![X:$i]:
% 0.59/0.79 ( ( ca_Vx6 @ X ) <=> ( ![Y:$i]: ( ( rinvS @ X @ Y ) => ( caxcomp @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl44, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]:
% 0.59/0.79 (~ (rinvS @ X0 @ X1) | (caxcomp @ X1) | ~ (ca_Vx6 @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_11])).
% 0.59/0.79 thf(zip_derived_cl78, plain,
% 0.59/0.79 (![X0 : $i]:
% 0.59/0.79 (~ (cUnsatisfiable @ X0) | ~ (ca_Vx6 @ (sk_ @ X0)) | (caxcomp @ X0))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl74, zip_derived_cl44])).
% 0.59/0.79 thf(zip_derived_cl85, plain,
% 0.59/0.79 (( (caxcomp @ i2003_11_14_17_21_33997)
% 0.59/0.79 | ~ (ca_Vx6 @ (sk_ @ i2003_11_14_17_21_33997)))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl57, zip_derived_cl78])).
% 0.59/0.79 thf(axiom_5, axiom,
% 0.59/0.79 (![X:$i]: ( ( caxcomp @ X ) <=> ( ?[Y0:$i]: ( ra_Px1 @ X @ Y0 ) ) ))).
% 0.59/0.79 thf(zip_derived_cl9, plain,
% 0.59/0.79 (![X0 : $i]: ( (ra_Px1 @ X0 @ (sk__2 @ X0)) | ~ (caxcomp @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_5])).
% 0.59/0.79 thf(zip_derived_cl88, plain,
% 0.59/0.79 ((~ (ca_Vx6 @ (sk_ @ i2003_11_14_17_21_33997))
% 0.59/0.79 | (ra_Px1 @ i2003_11_14_17_21_33997 @
% 0.59/0.79 (sk__2 @ i2003_11_14_17_21_33997)))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl85, zip_derived_cl9])).
% 0.59/0.79 thf(zip_derived_cl57, plain, ( (cUnsatisfiable @ i2003_11_14_17_21_33997)),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_17])).
% 0.59/0.79 thf(axiom_2, axiom, (![X:$i]: ( ( cUnsatisfiable @ X ) => ( ca @ X ) ))).
% 0.59/0.79 thf(zip_derived_cl4, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca @ X0) | ~ (cUnsatisfiable @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_2])).
% 0.59/0.79 thf(axiom_4, axiom,
% 0.59/0.79 (![X:$i]: ( ( ca @ X ) <=> ( ~( ?[Y:$i]: ( ra_Px1 @ X @ Y ) ) ) ))).
% 0.59/0.79 thf(zip_derived_cl7, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: (~ (ra_Px1 @ X0 @ X1) | ~ (ca @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_4])).
% 0.59/0.79 thf(zip_derived_cl75, plain,
% 0.59/0.79 (![X0 : $i, X1 : $i]: (~ (cUnsatisfiable @ X1) | ~ (ra_Px1 @ X1 @ X0))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl4, zip_derived_cl7])).
% 0.59/0.79 thf(zip_derived_cl84, plain,
% 0.59/0.79 (![X0 : $i]: ~ (ra_Px1 @ i2003_11_14_17_21_33997 @ X0)),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl57, zip_derived_cl75])).
% 0.59/0.79 thf(zip_derived_cl207, plain, (~ (ca_Vx6 @ (sk_ @ i2003_11_14_17_21_33997))),
% 0.59/0.79 inference('clc', [status(thm)], [zip_derived_cl88, zip_derived_cl84])).
% 0.59/0.79 thf(zip_derived_cl292, plain, (~ (ca_Ax2 @ (sk_ @ i2003_11_14_17_21_33997))),
% 0.59/0.79 inference('s_sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl207])).
% 0.59/0.79 thf(zip_derived_cl57, plain, ( (cUnsatisfiable @ i2003_11_14_17_21_33997)),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_17])).
% 0.59/0.79 thf(zip_derived_cl5, plain,
% 0.59/0.79 (![X0 : $i]: ( (ca_Ax2 @ (sk_ @ X0)) | ~ (cUnsatisfiable @ X0))),
% 0.59/0.79 inference('cnf', [status(esa)], [axiom_3])).
% 0.59/0.79 thf(zip_derived_cl83, plain, ( (ca_Ax2 @ (sk_ @ i2003_11_14_17_21_33997))),
% 0.59/0.79 inference('dp-resolution', [status(thm)],
% 0.59/0.79 [zip_derived_cl57, zip_derived_cl5])).
% 0.59/0.79 thf(zip_derived_cl294, plain, ($false),
% 0.59/0.79 inference('demod', [status(thm)], [zip_derived_cl292, zip_derived_cl83])).
% 0.59/0.79
% 0.59/0.79 % SZS output end Refutation
% 0.59/0.79
% 0.59/0.79
% 0.59/0.79 % Terminating...
% 0.63/0.86 % Runner terminated.
% 0.63/0.86 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------