%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYN691-1 : TPTP v9.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.zeMnX0S0dr true
% Computer : n023.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 05:05:34 PM UTC 2025
% Result : Unsatisfiable 0.65s 0.92s
% Output : Refutation 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN691-1 : TPTP v9.2.0. Released v2.5.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.zeMnX0S0dr true
% 0.15/0.35 % Computer : n023.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed Oct 1 13:36:53 EDT 2025
% 0.15/0.35 % CPUTime :
% 0.15/0.35 % Running portfolio for 300 s
% 0.15/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 % Number of cores: 8
% 0.21/0.35 % Python version: Python 3.6.8
% 0.21/0.36 % Running in FO mode
% 0.59/0.71 % Total configuration time : 435
% 0.59/0.71 % Estimated wc time : 1092
% 0.59/0.71 % Estimated cpu time (7 cpus) : 156.0
% 0.63/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.63/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.63/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.63/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.63/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.63/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.63/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.65/0.92 % Solved by fo/fo5.sh.
% 0.65/0.92 % done 187 iterations in 0.094s
% 0.65/0.92 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.65/0.92 % SZS output start Refutation
% 0.65/0.92 thf(p39_type, type, p39: $i > $i > $o).
% 0.65/0.92 thf(f21_type, type, f21: $i > $i > $i).
% 0.65/0.92 thf(f13_type, type, f13: $i > $i > $i).
% 0.65/0.92 thf(f17_type, type, f17: $i > $i > $i).
% 0.65/0.92 thf(c40_type, type, c40: $i).
% 0.65/0.92 thf(f36_type, type, f36: $i > $i > $i).
% 0.65/0.92 thf(f7_type, type, f7: $i > $i > $i).
% 0.65/0.92 thf(c48_type, type, c48: $i).
% 0.65/0.92 thf(c47_type, type, c47: $i).
% 0.65/0.92 thf(p2_type, type, p2: $i > $i > $o).
% 0.65/0.92 thf(c44_type, type, c44: $i).
% 0.65/0.92 thf(f26_type, type, f26: $i > $i > $i).
% 0.65/0.92 thf(p3_type, type, p3: $i > $i > $o).
% 0.65/0.92 thf(f5_type, type, f5: $i > $i > $i).
% 0.65/0.92 thf(f10_type, type, f10: $i > $i > $i).
% 0.65/0.92 thf(p22_type, type, p22: $i > $i > $o).
% 0.65/0.92 thf(c41_type, type, c41: $i).
% 0.65/0.92 thf(c46_type, type, c46: $i).
% 0.65/0.92 thf(c43_type, type, c43: $i).
% 0.65/0.92 thf(c49_type, type, c49: $i).
% 0.65/0.92 thf(f38_type, type, f38: $i > $i > $i).
% 0.65/0.92 thf(f19_type, type, f19: $i > $i > $i).
% 0.65/0.92 thf(f30_type, type, f30: $i > $i > $i).
% 0.65/0.92 thf(f34_type, type, f34: $i > $i > $i).
% 0.65/0.92 thf(p4_type, type, p4: $i > $i > $o).
% 0.65/0.92 thf(c45_type, type, c45: $i).
% 0.65/0.92 thf(c42_type, type, c42: $i).
% 0.65/0.92 thf(f15_type, type, f15: $i > $i > $i).
% 0.65/0.92 thf(f28_type, type, f28: $i > $i > $i).
% 0.65/0.92 thf(not_p39_43, conjecture,
% 0.65/0.92 (p39 @
% 0.65/0.92 ( f5 @ c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ c43 ) @ c44 ) @ c45 ) ) @ c46)).
% 0.65/0.92 thf(zf_stmt_0, negated_conjecture,
% 0.65/0.92 (~( p39 @
% 0.65/0.92 ( f5 @ c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ c43 ) @ c44 ) @ c45 ) ) @
% 0.65/0.92 c46 )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [not_p39_43])).
% 0.65/0.92 thf(zip_derived_cl42, plain,
% 0.65/0.92 (~ (p39 @ (f5 @ c40 @ (f10 @ (f13 @ (f15 @ c42 @ c43) @ c44) @ c45)) @
% 0.65/0.92 c46)),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.65/0.92 thf(p39_46, conjecture,
% 0.65/0.92 (~( p39 @
% 0.65/0.92 ( f5 @
% 0.65/0.92 c40 @
% 0.65/0.92 ( f7 @ c41 @ ( f10 @ ( f13 @ ( f15 @ c42 @ c43 ) @ c44 ) @ c45 ) ) ) @
% 0.65/0.92 c46 ))).
% 0.65/0.92 thf(zf_stmt_1, negated_conjecture,
% 0.65/0.92 (p39 @
% 0.65/0.92 ( f5 @
% 0.65/0.92 c40 @ ( f7 @ c41 @ ( f10 @ ( f13 @ ( f15 @ c42 @ c43 ) @ c44 ) @ c45 ) ) ) @
% 0.65/0.92 c46),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p39_46])).
% 0.65/0.92 thf(zip_derived_cl45, plain,
% 0.65/0.92 ( (p39 @
% 0.65/0.92 (f5 @ c40 @ (f7 @ c41 @ (f10 @ (f13 @ (f15 @ c42 @ c43) @ c44) @ c45))) @
% 0.65/0.92 c46)),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.65/0.92 thf(p2_17, conjecture, (~( p2 @ X31 @ X31 ))).
% 0.65/0.92 thf(zf_stmt_2, negated_conjecture, (p2 @ X31 @ X31),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p2_17])).
% 0.65/0.92 thf(zip_derived_cl16, plain, (![X0 : $i]: (p2 @ X0 @ X0)),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.65/0.92 thf(p3_67, conjecture,
% 0.65/0.92 (~( p3 @
% 0.65/0.92 ( f7 @ c41 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f10 @
% 0.65/0.92 ( f13 @
% 0.65/0.92 ( f15 @ c42 @ ( f17 @ ( f19 @ ( f21 @ c47 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f26 @ ( f28 @ ( f30 @ c48 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f34 @ ( f36 @ ( f38 @ c49 @ X47 ) @ X48 ) @ X49 ) ) ))).
% 0.65/0.92 thf(zf_stmt_3, negated_conjecture,
% 0.65/0.92 (p3 @
% 0.65/0.92 ( f7 @ c41 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f10 @
% 0.65/0.92 ( f13 @
% 0.65/0.92 ( f15 @ c42 @ ( f17 @ ( f19 @ ( f21 @ c47 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f26 @ ( f28 @ ( f30 @ c48 @ X47 ) @ X48 ) @ X49 ) ) @
% 0.65/0.92 ( f34 @ ( f36 @ ( f38 @ c49 @ X47 ) @ X48 ) @ X49 ) )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p3_67])).
% 0.65/0.92 thf(zip_derived_cl66, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.65/0.92 (p3 @ (f7 @ c41 @ (f10 @ (f13 @ (f15 @ c42 @ X0) @ X1) @ X2)) @
% 0.65/0.92 (f10 @
% 0.65/0.92 (f13 @ (f15 @ c42 @ (f17 @ (f19 @ (f21 @ c47 @ X0) @ X1) @ X2)) @
% 0.65/0.92 (f26 @ (f28 @ (f30 @ c48 @ X0) @ X1) @ X2)) @
% 0.65/0.92 (f34 @ (f36 @ (f38 @ c49 @ X0) @ X1) @ X2)))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.65/0.92 thf(p4_50, conjecture,
% 0.65/0.92 (~( ( ~( p3 @ X119 @ X121 ) ) | ( ~( p2 @ X118 @ X120 ) ) |
% 0.65/0.92 ( p4 @ ( f5 @ X118 @ X119 ) @ ( f5 @ X120 @ X121 ) ) ))).
% 0.65/0.92 thf(zf_stmt_4, negated_conjecture,
% 0.65/0.92 (( ~( p3 @ X119 @ X121 ) ) | ( ~( p2 @ X118 @ X120 ) ) |
% 0.65/0.92 ( p4 @ ( f5 @ X118 @ X119 ) @ ( f5 @ X120 @ X121 ) )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p4_50])).
% 0.65/0.92 thf(zip_derived_cl49, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (~ (p3 @ X0 @ X1)
% 0.65/0.92 | ~ (p2 @ X2 @ X3)
% 0.65/0.92 | (p4 @ (f5 @ X2 @ X0) @ (f5 @ X3 @ X1)))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.65/0.92 thf(zip_derived_cl233, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 0.65/0.92 ( (p4 @
% 0.65/0.92 (f5 @ X4 @ (f7 @ c41 @ (f10 @ (f13 @ (f15 @ c42 @ X2) @ X1) @ X0))) @
% 0.65/0.92 (f5 @ X3 @
% 0.65/0.92 (f10 @
% 0.65/0.92 (f13 @
% 0.65/0.92 (f15 @ c42 @ (f17 @ (f19 @ (f21 @ c47 @ X2) @ X1) @ X0)) @
% 0.65/0.92 (f26 @ (f28 @ (f30 @ c48 @ X2) @ X1) @ X0)) @
% 0.65/0.92 (f34 @ (f36 @ (f38 @ c49 @ X2) @ X1) @ X0))))
% 0.65/0.92 | ~ (p2 @ X4 @ X3))),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl49])).
% 0.65/0.92 thf(zip_derived_cl238, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (p4 @
% 0.65/0.92 (f5 @ X0 @ (f7 @ c41 @ (f10 @ (f13 @ (f15 @ c42 @ X3) @ X2) @ X1))) @
% 0.65/0.92 (f5 @ X0 @
% 0.65/0.92 (f10 @
% 0.65/0.92 (f13 @ (f15 @ c42 @ (f17 @ (f19 @ (f21 @ c47 @ X3) @ X2) @ X1)) @
% 0.65/0.92 (f26 @ (f28 @ (f30 @ c48 @ X3) @ X2) @ X1)) @
% 0.65/0.92 (f34 @ (f36 @ (f38 @ c49 @ X3) @ X2) @ X1))))),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl233])).
% 0.65/0.92 thf(p22_15, conjecture, (~( p22 @ X37 @ X37 ))).
% 0.65/0.92 thf(zf_stmt_5, negated_conjecture, (p22 @ X37 @ X37),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p22_15])).
% 0.65/0.92 thf(zip_derived_cl14, plain, (![X0 : $i]: (p22 @ X0 @ X0)),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.65/0.92 thf(p39_45, conjecture,
% 0.65/0.92 (~( ( ~( p22 @ X109 @ X108 ) ) | ( ~( p4 @ X110 @ X107 ) ) |
% 0.65/0.92 ( ~( p39 @ X110 @ X109 ) ) | ( p39 @ X107 @ X108 ) ))).
% 0.65/0.92 thf(zf_stmt_6, negated_conjecture,
% 0.65/0.92 (( ~( p22 @ X109 @ X108 ) ) | ( ~( p4 @ X110 @ X107 ) ) |
% 0.65/0.92 ( ~( p39 @ X110 @ X109 ) ) | ( p39 @ X107 @ X108 )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p39_45])).
% 0.65/0.92 thf(zip_derived_cl44, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (~ (p22 @ X0 @ X1)
% 0.65/0.92 | ~ (p4 @ X2 @ X3)
% 0.65/0.92 | ~ (p39 @ X2 @ X0)
% 0.65/0.92 | (p39 @ X3 @ X1))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.65/0.92 thf(zip_derived_cl192, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.65/0.92 ( (p39 @ X1 @ X0) | ~ (p39 @ X2 @ X0) | ~ (p4 @ X2 @ X1))),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl14, zip_derived_cl44])).
% 0.65/0.92 thf(zip_derived_cl261, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 0.65/0.92 (~ (p39 @
% 0.65/0.92 (f5 @ X3 @ (f7 @ c41 @ (f10 @ (f13 @ (f15 @ c42 @ X2) @ X1) @ X0))) @
% 0.65/0.92 X4)
% 0.65/0.92 | (p39 @
% 0.65/0.92 (f5 @ X3 @
% 0.65/0.92 (f10 @
% 0.65/0.92 (f13 @
% 0.65/0.92 (f15 @ c42 @ (f17 @ (f19 @ (f21 @ c47 @ X2) @ X1) @ X0)) @
% 0.65/0.92 (f26 @ (f28 @ (f30 @ c48 @ X2) @ X1) @ X0)) @
% 0.65/0.92 (f34 @ (f36 @ (f38 @ c49 @ X2) @ X1) @ X0))) @
% 0.65/0.92 X4))),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl238, zip_derived_cl192])).
% 0.65/0.92 thf(zip_derived_cl264, plain,
% 0.65/0.92 ( (p39 @
% 0.65/0.92 (f5 @ c40 @
% 0.65/0.92 (f10 @
% 0.65/0.92 (f13 @
% 0.65/0.92 (f15 @ c42 @ (f17 @ (f19 @ (f21 @ c47 @ c43) @ c44) @ c45)) @
% 0.65/0.92 (f26 @ (f28 @ (f30 @ c48 @ c43) @ c44) @ c45)) @
% 0.65/0.92 (f34 @ (f36 @ (f38 @ c49 @ c43) @ c44) @ c45))) @
% 0.65/0.92 c46)),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl45, zip_derived_cl261])).
% 0.65/0.92 thf(p39_63, conjecture,
% 0.65/0.92 (~( ( ~( p39 @
% 0.65/0.92 ( f5 @
% 0.65/0.92 c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X103 ) @ X105 ) @ X106 ) ) @
% 0.65/0.92 X104 ) ) |
% 0.65/0.92 ( p39 @ X103 @ X104 ) ))).
% 0.65/0.92 thf(zf_stmt_7, negated_conjecture,
% 0.65/0.92 (( ~( p39 @
% 0.65/0.92 ( f5 @ c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X103 ) @ X105 ) @ X106 ) ) @
% 0.65/0.92 X104 ) ) |
% 0.65/0.92 ( p39 @ X103 @ X104 )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p39_63])).
% 0.65/0.92 thf(zip_derived_cl62, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (~ (p39 @ (f5 @ c40 @ (f10 @ (f13 @ (f15 @ c42 @ X0) @ X1) @ X2)) @ X3)
% 0.65/0.92 | (p39 @ X0 @ X3))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.65/0.92 thf(zip_derived_cl266, plain,
% 0.65/0.92 ( (p39 @ (f17 @ (f19 @ (f21 @ c47 @ c43) @ c44) @ c45) @ c46)),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl264, zip_derived_cl62])).
% 0.65/0.92 thf(p39_44, conjecture,
% 0.65/0.92 (~( ( ~( p39 @ ( f17 @ ( f19 @ ( f21 @ c47 @ X47 ) @ X48 ) @ X49 ) @ X50 ) ) |
% 0.65/0.92 ( p39 @ X47 @ X50 ) ))).
% 0.65/0.92 thf(zf_stmt_8, negated_conjecture,
% 0.65/0.92 (( ~( p39 @ ( f17 @ ( f19 @ ( f21 @ c47 @ X47 ) @ X48 ) @ X49 ) @ X50 ) ) |
% 0.65/0.92 ( p39 @ X47 @ X50 )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p39_44])).
% 0.65/0.92 thf(zip_derived_cl43, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (~ (p39 @ (f17 @ (f19 @ (f21 @ c47 @ X0) @ X1) @ X2) @ X3)
% 0.65/0.92 | (p39 @ X0 @ X3))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.65/0.92 thf(zip_derived_cl268, plain, ( (p39 @ c43 @ c46)),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl266, zip_derived_cl43])).
% 0.65/0.92 thf(p39_64, conjecture,
% 0.65/0.92 (~( ( ~( p39 @ X103 @ X104 ) ) |
% 0.65/0.92 ( p39 @
% 0.65/0.92 ( f5 @ c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X103 ) @ X105 ) @ X106 ) ) @
% 0.65/0.92 X104 ) ))).
% 0.65/0.92 thf(zf_stmt_9, negated_conjecture,
% 0.65/0.92 (( ~( p39 @ X103 @ X104 ) ) |
% 0.65/0.92 ( p39 @
% 0.65/0.92 ( f5 @ c40 @ ( f10 @ ( f13 @ ( f15 @ c42 @ X103 ) @ X105 ) @ X106 ) ) @
% 0.65/0.92 X104 )),
% 0.65/0.92 inference('cnf.neg', [status(esa)], [p39_64])).
% 0.65/0.92 thf(zip_derived_cl63, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.65/0.92 (~ (p39 @ X0 @ X1)
% 0.65/0.92 | (p39 @ (f5 @ c40 @ (f10 @ (f13 @ (f15 @ c42 @ X0) @ X2) @ X3)) @
% 0.65/0.92 X1))),
% 0.65/0.92 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.65/0.92 thf(zip_derived_cl271, plain,
% 0.65/0.92 (![X0 : $i, X1 : $i]:
% 0.65/0.92 (p39 @ (f5 @ c40 @ (f10 @ (f13 @ (f15 @ c42 @ c43) @ X1) @ X0)) @ c46)),
% 0.65/0.92 inference('sup-', [status(thm)], [zip_derived_cl268, zip_derived_cl63])).
% 0.65/0.92 thf(zip_derived_cl272, plain, ($false),
% 0.65/0.92 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl271])).
% 0.65/0.92
% 0.65/0.92 % SZS output end Refutation
% 0.65/0.92
% 0.65/0.92
% 0.65/0.92 % Terminating...
% 1.94/1.02 % Runner terminated.
% 1.94/1.03 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------