%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ028-6 : TPTP v9.2.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.tUXBDEHSs3 true
% Computer : n008.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:49:31 PM UTC 2025
% Result : Unsatisfiable 15.63s 2.92s
% Output : Refutation 15.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.15 % Problem : PUZ028-6 : TPTP v9.2.0. Released v2.0.0.
% 0.13/0.16 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.tUXBDEHSs3 true
% 0.17/0.39 % Computer : n008.cluster.edu
% 0.17/0.39 % Model : x86_64 x86_64
% 0.17/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.39 % Memory : 8042.1875MB
% 0.17/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.39 % CPULimit : 300
% 0.17/0.39 % WCLimit : 300
% 0.17/0.39 % DateTime : Wed Oct 1 15:10:08 EDT 2025
% 0.17/0.39 % CPUTime :
% 0.17/0.39 % Running portfolio for 300 s
% 0.17/0.39 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.39 % Number of cores: 8
% 0.17/0.39 % Python version: Python 3.6.8
% 0.17/0.39 % Running in FO mode
% 0.40/0.72 % Total configuration time : 435
% 0.40/0.72 % Estimated wc time : 1092
% 0.40/0.72 % Estimated cpu time (7 cpus) : 156.0
% 0.42/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.42/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.42/0.84 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.42/0.84 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.42/0.84 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.42/0.85 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.42/0.85 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.42/0.89 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 15.63/2.92 % Solved by fo/fo13.sh.
% 15.63/2.92 % done 2985 iterations in 2.037s
% 15.63/2.92 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 15.63/2.92 % SZS output start Refutation
% 15.63/2.92 thf(n1_type, type, n1: $i).
% 15.63/2.92 thf(n3_type, type, n3: $i).
% 15.63/2.92 thf(not_equal_type, type, not_equal: $i > $i > $o).
% 15.63/2.92 thf(person_type, type, person: $i > $o).
% 15.63/2.92 thf(n2_type, type, n2: $i).
% 15.63/2.92 thf(not_familiar_type, type, not_familiar: $i > $i > $o).
% 15.63/2.92 thf(familiar_type, type, familiar: $i > $i > $o).
% 15.63/2.92 thf(n4_type, type, n4: $i).
% 15.63/2.92 thf(n5_type, type, n5: $i).
% 15.63/2.92 thf(n6_type, type, n6: $i).
% 15.63/2.92 thf(not_equal_6_5, axiom, (not_equal @ n6 @ n5)).
% 15.63/2.92 thf(zip_derived_cl35, plain, ( (not_equal @ n6 @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_6_5])).
% 15.63/2.92 thf(familiar_or_not, axiom,
% 15.63/2.92 (( familiar @ X @ Y ) | ( not_familiar @ X @ Y ) | ( ~( person @ X ) ) |
% 15.63/2.92 ( ~( person @ Y ) ) | ( ~( not_equal @ X @ Y ) ))).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl78, plain,
% 15.63/2.92 (( (familiar @ n6 @ n5)
% 15.63/2.92 | (not_familiar @ n6 @ n5)
% 15.63/2.92 | ~ (person @ n6)
% 15.63/2.92 | ~ (person @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl36])).
% 15.63/2.92 thf(person_6, axiom, (person @ n6)).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(person_5, axiom, (person @ n5)).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl108, plain,
% 15.63/2.92 (( (familiar @ n6 @ n5) | (not_familiar @ n6 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl78, zip_derived_cl5, zip_derived_cl4])).
% 15.63/2.92 thf(not_equal_1_5, axiom, (not_equal @ n1 @ n5)).
% 15.63/2.92 thf(zip_derived_cl9, plain, ( (not_equal @ n1 @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_1_5])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl52, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5)
% 15.63/2.92 | (not_familiar @ n1 @ n5)
% 15.63/2.92 | ~ (person @ n1)
% 15.63/2.92 | ~ (person @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl9, zip_derived_cl36])).
% 15.63/2.92 thf(person_1, axiom, (person @ n1)).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl82, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (not_familiar @ n1 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl52, zip_derived_cl0, zip_derived_cl4])).
% 15.63/2.92 thf(symmetry_of_not_familiar, axiom,
% 15.63/2.92 (( ~( not_familiar @ X1 @ X2 ) ) | ( not_familiar @ X2 @ X1 ))).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl115, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (not_familiar @ n5 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_5_3, axiom, (not_equal @ n5 @ n3)).
% 15.63/2.92 thf(zip_derived_cl28, plain, ( (not_equal @ n5 @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_5_3])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl71, plain,
% 15.63/2.92 (( (familiar @ n5 @ n3)
% 15.63/2.92 | (not_familiar @ n5 @ n3)
% 15.63/2.92 | ~ (person @ n5)
% 15.63/2.92 | ~ (person @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl28, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(person_3, axiom, (person @ n3)).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl101, plain,
% 15.63/2.92 (( (familiar @ n5 @ n3) | (not_familiar @ n5 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl71, zip_derived_cl4, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl211, plain,
% 15.63/2.92 (( (familiar @ n5 @ n3) | (not_familiar @ n3 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_5_2, axiom, (not_equal @ n5 @ n2)).
% 15.63/2.92 thf(zip_derived_cl27, plain, ( (not_equal @ n5 @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_5_2])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl70, plain,
% 15.63/2.92 (( (familiar @ n5 @ n2)
% 15.63/2.92 | (not_familiar @ n5 @ n2)
% 15.63/2.92 | ~ (person @ n5)
% 15.63/2.92 | ~ (person @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(person_2, axiom, (person @ n2)).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl100, plain,
% 15.63/2.92 (( (familiar @ n5 @ n2) | (not_familiar @ n5 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl70, zip_derived_cl4, zip_derived_cl1])).
% 15.63/2.92 thf(not_equal_2_3, axiom, (not_equal @ n2 @ n3)).
% 15.63/2.92 thf(zip_derived_cl12, plain, ( (not_equal @ n2 @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_2_3])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl55, plain,
% 15.63/2.92 (( (familiar @ n2 @ n3)
% 15.63/2.92 | (not_familiar @ n2 @ n3)
% 15.63/2.92 | ~ (person @ n2)
% 15.63/2.92 | ~ (person @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl12, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl85, plain,
% 15.63/2.92 (( (familiar @ n2 @ n3) | (not_familiar @ n2 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl55, zip_derived_cl1, zip_derived_cl2])).
% 15.63/2.92 thf(three_not_familiar, conjecture,
% 15.63/2.92 (~( ( ~( not_familiar @ X3 @ X1 ) ) | ( ~( not_familiar @ X2 @ X3 ) ) |
% 15.63/2.92 ( ~( not_familiar @ X1 @ X2 ) ) ))).
% 15.63/2.92 thf(zf_stmt_0, negated_conjecture,
% 15.63/2.92 (( ~( not_familiar @ X3 @ X1 ) ) | ( ~( not_familiar @ X2 @ X3 ) ) |
% 15.63/2.92 ( ~( not_familiar @ X1 @ X2 ) )),
% 15.63/2.92 inference('cnf.neg', [status(esa)], [three_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl123, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n3)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl207, plain,
% 15.63/2.92 (( (familiar @ n5 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n3 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl123])).
% 15.63/2.92 thf(zip_derived_cl1226, plain,
% 15.63/2.92 (( (familiar @ n5 @ n3) | (familiar @ n5 @ n2) | (familiar @ n2 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl207])).
% 15.63/2.92 thf(not_equal_5_6, axiom, (not_equal @ n5 @ n6)).
% 15.63/2.92 thf(zip_derived_cl30, plain, ( (not_equal @ n5 @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_5_6])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl73, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6)
% 15.63/2.92 | (not_familiar @ n5 @ n6)
% 15.63/2.92 | ~ (person @ n5)
% 15.63/2.92 | ~ (person @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl30, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl103, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (not_familiar @ n5 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl73, zip_derived_cl4, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl221, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (not_familiar @ n6 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl100, plain,
% 15.63/2.92 (( (familiar @ n5 @ n2) | (not_familiar @ n5 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl70, zip_derived_cl4, zip_derived_cl1])).
% 15.63/2.92 thf(not_equal_2_6, axiom, (not_equal @ n2 @ n6)).
% 15.63/2.92 thf(zip_derived_cl15, plain, ( (not_equal @ n2 @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_2_6])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl58, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6)
% 15.63/2.92 | (not_familiar @ n2 @ n6)
% 15.63/2.92 | ~ (person @ n2)
% 15.63/2.92 | ~ (person @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl88, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (not_familiar @ n2 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl58, zip_derived_cl1, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl134, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl88, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl210, plain,
% 15.63/2.92 (( (familiar @ n5 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl134])).
% 15.63/2.92 thf(zip_derived_cl1242, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (familiar @ n5 @ n2) | (familiar @ n2 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl210])).
% 15.63/2.92 thf(not_equal_4_6, axiom, (not_equal @ n4 @ n6)).
% 15.63/2.92 thf(zip_derived_cl25, plain, ( (not_equal @ n4 @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_4_6])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl68, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6)
% 15.63/2.92 | (not_familiar @ n4 @ n6)
% 15.63/2.92 | ~ (person @ n4)
% 15.63/2.92 | ~ (person @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl36])).
% 15.63/2.92 thf(person_4, axiom, (person @ n4)).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl98, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6) | (not_familiar @ n4 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl68, zip_derived_cl3, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl180, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6) | (not_familiar @ n6 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl98, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_4_2, axiom, (not_equal @ n4 @ n2)).
% 15.63/2.92 thf(zip_derived_cl22, plain, ( (not_equal @ n4 @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_4_2])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl65, plain,
% 15.63/2.92 (( (familiar @ n4 @ n2)
% 15.63/2.92 | (not_familiar @ n4 @ n2)
% 15.63/2.92 | ~ (person @ n4)
% 15.63/2.92 | ~ (person @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl22, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl95, plain,
% 15.63/2.92 (( (familiar @ n4 @ n2) | (not_familiar @ n4 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl65, zip_derived_cl3, zip_derived_cl1])).
% 15.63/2.92 thf(zip_derived_cl134, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl88, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl174, plain,
% 15.63/2.92 (( (familiar @ n4 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl134])).
% 15.63/2.92 thf(zip_derived_cl1112, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6) | (familiar @ n4 @ n2) | (familiar @ n2 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl180, zip_derived_cl174])).
% 15.63/2.92 thf(not_equal_6_1, axiom, (not_equal @ n6 @ n1)).
% 15.63/2.92 thf(zip_derived_cl31, plain, ( (not_equal @ n6 @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_6_1])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl74, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1)
% 15.63/2.92 | (not_familiar @ n6 @ n1)
% 15.63/2.92 | ~ (person @ n6)
% 15.63/2.92 | ~ (person @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl104, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl74, zip_derived_cl5, zip_derived_cl0])).
% 15.63/2.92 thf(not_equal_1_3, axiom, (not_equal @ n1 @ n3)).
% 15.63/2.92 thf(zip_derived_cl7, plain, ( (not_equal @ n1 @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_1_3])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl50, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (not_familiar @ n1 @ n3)
% 15.63/2.92 | ~ (person @ n1)
% 15.63/2.92 | ~ (person @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl80, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (not_familiar @ n1 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl50, zip_derived_cl0, zip_derived_cl2])).
% 15.63/2.92 thf(not_equal_3_6, axiom, (not_equal @ n3 @ n6)).
% 15.63/2.92 thf(zip_derived_cl20, plain, ( (not_equal @ n3 @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_3_6])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl63, plain,
% 15.63/2.92 (( (familiar @ n3 @ n6)
% 15.63/2.92 | (not_familiar @ n3 @ n6)
% 15.63/2.92 | ~ (person @ n3)
% 15.63/2.92 | ~ (person @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl93, plain,
% 15.63/2.92 (( (familiar @ n3 @ n6) | (not_familiar @ n3 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl63, zip_derived_cl2, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl160, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n3 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl93, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl191, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl160])).
% 15.63/2.92 thf(zip_derived_cl1163, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (familiar @ n1 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl191])).
% 15.63/2.92 thf(not_equal_6_4, axiom, (not_equal @ n6 @ n4)).
% 15.63/2.92 thf(zip_derived_cl34, plain, ( (not_equal @ n6 @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_6_4])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl77, plain,
% 15.63/2.92 (( (familiar @ n6 @ n4)
% 15.63/2.92 | (not_familiar @ n6 @ n4)
% 15.63/2.92 | ~ (person @ n6)
% 15.63/2.92 | ~ (person @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl107, plain,
% 15.63/2.92 (( (familiar @ n6 @ n4) | (not_familiar @ n6 @ n4))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl77, zip_derived_cl5, zip_derived_cl3])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl264, plain,
% 15.63/2.92 (( (familiar @ n6 @ n4) | (not_familiar @ n4 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl107, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl104, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl74, zip_derived_cl5, zip_derived_cl0])).
% 15.63/2.92 thf(not_equal_1_4, axiom, (not_equal @ n1 @ n4)).
% 15.63/2.92 thf(zip_derived_cl8, plain, ( (not_equal @ n1 @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_1_4])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl51, plain,
% 15.63/2.92 (( (familiar @ n1 @ n4)
% 15.63/2.92 | (not_familiar @ n1 @ n4)
% 15.63/2.92 | ~ (person @ n1)
% 15.63/2.92 | ~ (person @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl8, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl81, plain,
% 15.63/2.92 (( (familiar @ n1 @ n4) | (not_familiar @ n1 @ n4))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl51, zip_derived_cl0, zip_derived_cl3])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl114, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n4)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n4 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl81, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl227, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n4)
% 15.63/2.92 | ~ (not_familiar @ n4 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl114])).
% 15.63/2.92 thf(zip_derived_cl1292, plain,
% 15.63/2.92 (( (familiar @ n6 @ n4) | (familiar @ n6 @ n1) | (familiar @ n1 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl264, zip_derived_cl227])).
% 15.63/2.92 thf(not_equal_4_3, axiom, (not_equal @ n4 @ n3)).
% 15.63/2.92 thf(zip_derived_cl23, plain, ( (not_equal @ n4 @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_4_3])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl66, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3)
% 15.63/2.92 | (not_familiar @ n4 @ n3)
% 15.63/2.92 | ~ (person @ n4)
% 15.63/2.92 | ~ (person @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl96, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3) | (not_familiar @ n4 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl66, zip_derived_cl3, zip_derived_cl2])).
% 15.63/2.92 thf(not_equal_3_1, axiom, (not_equal @ n3 @ n1)).
% 15.63/2.92 thf(zip_derived_cl16, plain, ( (not_equal @ n3 @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_3_1])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl59, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1)
% 15.63/2.92 | (not_familiar @ n3 @ n1)
% 15.63/2.92 | ~ (person @ n3)
% 15.63/2.92 | ~ (person @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl89, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1) | (not_familiar @ n3 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl59, zip_derived_cl2, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl114, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n4)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n4 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl81, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl139, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n4)
% 15.63/2.92 | ~ (not_familiar @ n4 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl89, zip_derived_cl114])).
% 15.63/2.92 thf(zip_derived_cl625, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3) | (familiar @ n3 @ n1) | (familiar @ n1 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl139])).
% 15.63/2.92 thf(three_familiar, conjecture,
% 15.63/2.92 (~( ( ~( familiar @ X3 @ X1 ) ) | ( ~( familiar @ X2 @ X3 ) ) |
% 15.63/2.92 ( ~( familiar @ X1 @ X2 ) ) ))).
% 15.63/2.92 thf(zf_stmt_1, negated_conjecture,
% 15.63/2.92 (( ~( familiar @ X3 @ X1 ) ) | ( ~( familiar @ X2 @ X3 ) ) |
% 15.63/2.92 ( ~( familiar @ X1 @ X2 ) )),
% 15.63/2.92 inference('cnf.neg', [status(esa)], [three_familiar])).
% 15.63/2.92 thf(zip_derived_cl39, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (familiar @ X0 @ X1)
% 15.63/2.92 | ~ (familiar @ X2 @ X0)
% 15.63/2.92 | ~ (familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.92 thf(zip_derived_cl930, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n4)
% 15.63/2.92 | (familiar @ n3 @ n1)
% 15.63/2.92 | ~ (familiar @ X0 @ n4)
% 15.63/2.92 | ~ (familiar @ n3 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl625, zip_derived_cl39])).
% 15.63/2.92 thf(zip_derived_cl2638, plain,
% 15.63/2.92 (( (familiar @ n1 @ n4)
% 15.63/2.92 | (familiar @ n6 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n4)
% 15.63/2.92 | (familiar @ n3 @ n1)
% 15.63/2.92 | ~ (familiar @ n3 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl1292, zip_derived_cl930])).
% 15.63/2.92 thf(zip_derived_cl2655, plain,
% 15.63/2.92 ((~ (familiar @ n3 @ n6)
% 15.63/2.92 | (familiar @ n3 @ n1)
% 15.63/2.92 | (familiar @ n6 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n4))),
% 15.63/2.92 inference('simplify', [status(thm)], [zip_derived_cl2638])).
% 15.63/2.92 thf(zip_derived_cl104, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl74, zip_derived_cl5, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl223, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (not_familiar @ n1 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_6_3, axiom, (not_equal @ n6 @ n3)).
% 15.63/2.92 thf(zip_derived_cl33, plain, ( (not_equal @ n6 @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_6_3])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl76, plain,
% 15.63/2.92 (( (familiar @ n6 @ n3)
% 15.63/2.92 | (not_familiar @ n6 @ n3)
% 15.63/2.92 | ~ (person @ n6)
% 15.63/2.92 | ~ (person @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl33, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl106, plain,
% 15.63/2.92 (( (familiar @ n6 @ n3) | (not_familiar @ n6 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl76, zip_derived_cl5, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl89, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1) | (not_familiar @ n3 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl59, zip_derived_cl2, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl136, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n3 @ n1)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n1 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl89, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl259, plain,
% 15.63/2.92 (( (familiar @ n6 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n1 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl136])).
% 15.63/2.92 thf(zip_derived_cl1404, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (familiar @ n6 @ n3) | (familiar @ n3 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl223, zip_derived_cl259])).
% 15.63/2.92 thf(symmetry_of_familiar, axiom,
% 15.63/2.92 (( ~( familiar @ X1 @ X2 ) ) | ( familiar @ X2 @ X1 ))).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl1405, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1) | (familiar @ n6 @ n1) | (familiar @ n3 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl1404, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl11813, plain,
% 15.63/2.92 (( (familiar @ n1 @ n4) | (familiar @ n6 @ n1) | (familiar @ n3 @ n1))),
% 15.63/2.92 inference('clc', [status(thm)], [zip_derived_cl2655, zip_derived_cl1405])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl11814, plain,
% 15.63/2.92 (( (familiar @ n3 @ n1) | (familiar @ n1 @ n4) | (familiar @ n1 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl11813, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl11819, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (familiar @ n1 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl11814, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl103, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (not_familiar @ n5 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl73, zip_derived_cl4, zip_derived_cl5])).
% 15.63/2.92 thf(not_equal_6_2, axiom, (not_equal @ n6 @ n2)).
% 15.63/2.92 thf(zip_derived_cl32, plain, ( (not_equal @ n6 @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_6_2])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl75, plain,
% 15.63/2.92 (( (familiar @ n6 @ n2)
% 15.63/2.92 | (not_familiar @ n6 @ n2)
% 15.63/2.92 | ~ (person @ n6)
% 15.63/2.92 | ~ (person @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl105, plain,
% 15.63/2.92 (( (familiar @ n6 @ n2) | (not_familiar @ n6 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl75, zip_derived_cl5, zip_derived_cl1])).
% 15.63/2.92 thf(not_equal_2_5, axiom, (not_equal @ n2 @ n5)).
% 15.63/2.92 thf(zip_derived_cl14, plain, ( (not_equal @ n2 @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_2_5])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl57, plain,
% 15.63/2.92 (( (familiar @ n2 @ n5)
% 15.63/2.92 | (not_familiar @ n2 @ n5)
% 15.63/2.92 | ~ (person @ n2)
% 15.63/2.92 | ~ (person @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl14, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl87, plain,
% 15.63/2.92 (( (familiar @ n2 @ n5) | (not_familiar @ n2 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl57, zip_derived_cl1, zip_derived_cl4])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl132, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n5)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl255, plain,
% 15.63/2.92 (( (familiar @ n6 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n5)
% 15.63/2.92 | ~ (not_familiar @ n5 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl105, zip_derived_cl132])).
% 15.63/2.92 thf(zip_derived_cl1391, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (familiar @ n6 @ n2) | (familiar @ n2 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl255])).
% 15.63/2.92 thf(zip_derived_cl103, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (not_familiar @ n5 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl73, zip_derived_cl4, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl106, plain,
% 15.63/2.92 (( (familiar @ n6 @ n3) | (not_familiar @ n6 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl76, zip_derived_cl5, zip_derived_cl2])).
% 15.63/2.92 thf(not_equal_3_5, axiom, (not_equal @ n3 @ n5)).
% 15.63/2.92 thf(zip_derived_cl19, plain, ( (not_equal @ n3 @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_3_5])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl62, plain,
% 15.63/2.92 (( (familiar @ n3 @ n5)
% 15.63/2.92 | (not_familiar @ n3 @ n5)
% 15.63/2.92 | ~ (person @ n3)
% 15.63/2.92 | ~ (person @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl19, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl92, plain,
% 15.63/2.92 (( (familiar @ n3 @ n5) | (not_familiar @ n3 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl62, zip_derived_cl2, zip_derived_cl4])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl148, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n3 @ n5)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl262, plain,
% 15.63/2.92 (( (familiar @ n6 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n5)
% 15.63/2.92 | ~ (not_familiar @ n5 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl148])).
% 15.63/2.92 thf(zip_derived_cl1419, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (familiar @ n6 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl262])).
% 15.63/2.92 thf(zip_derived_cl221, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (not_familiar @ n6 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_5_4, axiom, (not_equal @ n5 @ n4)).
% 15.63/2.92 thf(zip_derived_cl29, plain, ( (not_equal @ n5 @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_5_4])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl72, plain,
% 15.63/2.92 (( (familiar @ n5 @ n4)
% 15.63/2.92 | (not_familiar @ n5 @ n4)
% 15.63/2.92 | ~ (person @ n5)
% 15.63/2.92 | ~ (person @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl102, plain,
% 15.63/2.92 (( (familiar @ n5 @ n4) | (not_familiar @ n5 @ n4))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl72, zip_derived_cl4, zip_derived_cl3])).
% 15.63/2.92 thf(zip_derived_cl98, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6) | (not_familiar @ n4 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl68, zip_derived_cl3, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl181, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n4 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n4)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl98, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl245, plain,
% 15.63/2.92 (( (familiar @ n5 @ n4)
% 15.63/2.92 | (familiar @ n4 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl181])).
% 15.63/2.92 thf(zip_derived_cl1358, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (familiar @ n5 @ n4) | (familiar @ n4 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl245])).
% 15.63/2.92 thf(zip_derived_cl88, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (not_familiar @ n2 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl58, zip_derived_cl1, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl133, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (not_familiar @ n6 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl88, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl85, plain,
% 15.63/2.92 (( (familiar @ n2 @ n3) | (not_familiar @ n2 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl55, zip_derived_cl1, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl160, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n3 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl93, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl192, plain,
% 15.63/2.92 (( (familiar @ n2 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl160])).
% 15.63/2.92 thf(zip_derived_cl1174, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (familiar @ n2 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl133, zip_derived_cl192])).
% 15.63/2.92 thf(zip_derived_cl104, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl74, zip_derived_cl5, zip_derived_cl0])).
% 15.63/2.92 thf(not_equal_1_2, axiom, (not_equal @ n1 @ n2)).
% 15.63/2.92 thf(zip_derived_cl6, plain, ( (not_equal @ n1 @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_1_2])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl49, plain,
% 15.63/2.92 (( (familiar @ n1 @ n2)
% 15.63/2.92 | (not_familiar @ n1 @ n2)
% 15.63/2.92 | ~ (person @ n1)
% 15.63/2.92 | ~ (person @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl79, plain,
% 15.63/2.92 (( (familiar @ n1 @ n2) | (not_familiar @ n1 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl49, zip_derived_cl0, zip_derived_cl1])).
% 15.63/2.92 thf(zip_derived_cl134, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl88, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl155, plain,
% 15.63/2.92 (( (familiar @ n1 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl134])).
% 15.63/2.92 thf(zip_derived_cl1025, plain,
% 15.63/2.92 (( (familiar @ n6 @ n1) | (familiar @ n1 @ n2) | (familiar @ n2 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl155])).
% 15.63/2.92 thf(zip_derived_cl1358, plain,
% 15.63/2.92 (( (familiar @ n5 @ n6) | (familiar @ n5 @ n4) | (familiar @ n4 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl245])).
% 15.63/2.92 thf(not_equal_1_6, axiom, (not_equal @ n1 @ n6)).
% 15.63/2.92 thf(zip_derived_cl10, plain, ( (not_equal @ n1 @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_1_6])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl53, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6)
% 15.63/2.92 | (not_familiar @ n1 @ n6)
% 15.63/2.92 | ~ (person @ n1)
% 15.63/2.92 | ~ (person @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl5, plain, ( (person @ n6)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_6])).
% 15.63/2.92 thf(zip_derived_cl83, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (not_familiar @ n1 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl53, zip_derived_cl0, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl117, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl191, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl160])).
% 15.63/2.92 thf(zip_derived_cl1164, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (familiar @ n1 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl117, zip_derived_cl191])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl1169, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n6) | (familiar @ n6 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl1164, zip_derived_cl37])).
% 15.63/2.92 thf(not_equal_3_2, axiom, (not_equal @ n3 @ n2)).
% 15.63/2.92 thf(zip_derived_cl17, plain, ( (not_equal @ n3 @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_3_2])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl60, plain,
% 15.63/2.92 (( (familiar @ n3 @ n2)
% 15.63/2.92 | (not_familiar @ n3 @ n2)
% 15.63/2.92 | ~ (person @ n3)
% 15.63/2.92 | ~ (person @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl17, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl90, plain,
% 15.63/2.92 (( (familiar @ n3 @ n2) | (not_familiar @ n3 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl60, zip_derived_cl2, zip_derived_cl1])).
% 15.63/2.92 thf(not_equal_2_1, axiom, (not_equal @ n2 @ n1)).
% 15.63/2.92 thf(zip_derived_cl11, plain, ( (not_equal @ n2 @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_2_1])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl54, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1)
% 15.63/2.92 | (not_familiar @ n2 @ n1)
% 15.63/2.92 | ~ (person @ n2)
% 15.63/2.92 | ~ (person @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl84, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1) | (not_familiar @ n2 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl54, zip_derived_cl1, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl80, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (not_familiar @ n1 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl50, zip_derived_cl0, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl112, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl126, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n3 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl112])).
% 15.63/2.92 thf(zip_derived_cl386, plain,
% 15.63/2.92 (( (familiar @ n3 @ n2) | (familiar @ n2 @ n1) | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl90, zip_derived_cl126])).
% 15.63/2.92 thf(zip_derived_cl39, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (familiar @ X0 @ X1)
% 15.63/2.92 | ~ (familiar @ X2 @ X0)
% 15.63/2.92 | ~ (familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.92 thf(zip_derived_cl534, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ X0 @ n3)
% 15.63/2.92 | ~ (familiar @ n2 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl386, zip_derived_cl39])).
% 15.63/2.92 thf(zip_derived_cl1745, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ n2 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl1169, zip_derived_cl534])).
% 15.63/2.92 thf(zip_derived_cl1761, plain,
% 15.63/2.92 ((~ (familiar @ n2 @ n6)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n1 @ n6))),
% 15.63/2.92 inference('simplify', [status(thm)], [zip_derived_cl1745])).
% 15.63/2.92 thf(zip_derived_cl133, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (not_familiar @ n6 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl88, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl84, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1) | (not_familiar @ n2 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl54, zip_derived_cl1, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl83, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (not_familiar @ n1 @ n6))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl53, zip_derived_cl0, zip_derived_cl5])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl118, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n6)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl129, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n6)
% 15.63/2.92 | ~ (not_familiar @ n6 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl118])).
% 15.63/2.92 thf(zip_derived_cl516, plain,
% 15.63/2.92 (( (familiar @ n2 @ n6) | (familiar @ n2 @ n1) | (familiar @ n1 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl133, zip_derived_cl129])).
% 15.63/2.92 thf(zip_derived_cl8466, plain,
% 15.63/2.92 (( (familiar @ n1 @ n6) | (familiar @ n1 @ n3) | (familiar @ n2 @ n1))),
% 15.63/2.92 inference('clc', [status(thm)], [zip_derived_cl1761, zip_derived_cl516])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl8467, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n6) | (familiar @ n1 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl8466, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl8473, plain,
% 15.63/2.92 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n3) | (familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl8467, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl115, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (not_familiar @ n5 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl80, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (not_familiar @ n1 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl50, zip_derived_cl0, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl148, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n3 @ n5)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl188, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n3 @ n5)
% 15.63/2.92 | ~ (not_familiar @ n5 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl148])).
% 15.63/2.92 thf(zip_derived_cl1144, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (familiar @ n1 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl115, zip_derived_cl188])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl1147, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n5) | (familiar @ n5 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl1144, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl534, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ X0 @ n3)
% 15.63/2.92 | ~ (familiar @ n2 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl386, zip_derived_cl39])).
% 15.63/2.92 thf(zip_derived_cl1735, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ n2 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl1147, zip_derived_cl534])).
% 15.63/2.92 thf(zip_derived_cl1759, plain,
% 15.63/2.92 ((~ (familiar @ n2 @ n5)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n1 @ n5))),
% 15.63/2.92 inference('simplify', [status(thm)], [zip_derived_cl1735])).
% 15.63/2.92 thf(zip_derived_cl87, plain,
% 15.63/2.92 (( (familiar @ n2 @ n5) | (not_familiar @ n2 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl57, zip_derived_cl1, zip_derived_cl4])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl131, plain,
% 15.63/2.92 (( (familiar @ n2 @ n5) | (not_familiar @ n5 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl84, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1) | (not_familiar @ n2 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl54, zip_derived_cl1, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl82, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (not_familiar @ n1 @ n5))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl52, zip_derived_cl0, zip_derived_cl4])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl116, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n5)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl128, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n5)
% 15.63/2.92 | ~ (not_familiar @ n5 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl116])).
% 15.63/2.92 thf(zip_derived_cl480, plain,
% 15.63/2.92 (( (familiar @ n2 @ n5) | (familiar @ n2 @ n1) | (familiar @ n1 @ n5))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl131, zip_derived_cl128])).
% 15.63/2.92 thf(zip_derived_cl7947, plain,
% 15.63/2.92 (( (familiar @ n1 @ n5) | (familiar @ n1 @ n3) | (familiar @ n2 @ n1))),
% 15.63/2.92 inference('clc', [status(thm)], [zip_derived_cl1759, zip_derived_cl480])).
% 15.63/2.92 thf(zip_derived_cl37, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.92 thf(zip_derived_cl7948, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n5) | (familiar @ n1 @ n2))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl7947, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl39, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (familiar @ X0 @ X1)
% 15.63/2.92 | ~ (familiar @ X2 @ X0)
% 15.63/2.92 | ~ (familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.92 thf(zip_derived_cl7953, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n2)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (familiar @ X0 @ n1)
% 15.63/2.92 | ~ (familiar @ n5 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl7948, zip_derived_cl39])).
% 15.63/2.92 thf(zip_derived_cl8552, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n1 @ n2)
% 15.63/2.92 | (familiar @ n1 @ n2)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (familiar @ n5 @ n6))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl8473, zip_derived_cl7953])).
% 15.63/2.92 thf(zip_derived_cl8554, plain,
% 15.63/2.92 ((~ (familiar @ n5 @ n6) | (familiar @ n1 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('simplify', [status(thm)], [zip_derived_cl8552])).
% 15.63/2.92 thf(zip_derived_cl8565, plain,
% 15.63/2.92 (( (familiar @ n4 @ n6)
% 15.63/2.92 | (familiar @ n5 @ n4)
% 15.63/2.92 | (familiar @ n1 @ n2)
% 15.63/2.92 | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl1358, zip_derived_cl8554])).
% 15.63/2.92 thf(zip_derived_cl8473, plain,
% 15.63/2.92 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n3) | (familiar @ n6 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl8467, zip_derived_cl37])).
% 15.63/2.92 thf(zip_derived_cl96, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3) | (not_familiar @ n4 @ n3))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl66, zip_derived_cl3, zip_derived_cl2])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl175, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3) | (not_familiar @ n3 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl38])).
% 15.63/2.92 thf(not_equal_4_1, axiom, (not_equal @ n4 @ n1)).
% 15.63/2.92 thf(zip_derived_cl21, plain, ( (not_equal @ n4 @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [not_equal_4_1])).
% 15.63/2.92 thf(zip_derived_cl36, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 ( (familiar @ X0 @ X1)
% 15.63/2.92 | (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (person @ X0)
% 15.63/2.92 | ~ (person @ X1)
% 15.63/2.92 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.92 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.92 thf(zip_derived_cl64, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1)
% 15.63/2.92 | (not_familiar @ n4 @ n1)
% 15.63/2.92 | ~ (person @ n4)
% 15.63/2.92 | ~ (person @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl21, zip_derived_cl36])).
% 15.63/2.92 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.92 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.92 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.92 thf(zip_derived_cl94, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1) | (not_familiar @ n4 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl64, zip_derived_cl3, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl112, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl164, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | ~ (not_familiar @ n3 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl94, zip_derived_cl112])).
% 15.63/2.92 thf(zip_derived_cl1068, plain,
% 15.63/2.92 (( (familiar @ n4 @ n3) | (familiar @ n4 @ n1) | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl175, zip_derived_cl164])).
% 15.63/2.92 thf(zip_derived_cl534, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ X0 @ n3)
% 15.63/2.92 | ~ (familiar @ n2 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl386, zip_derived_cl39])).
% 15.63/2.92 thf(zip_derived_cl1727, plain,
% 15.63/2.92 (( (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n4 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (familiar @ n2 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)],
% 15.63/2.92 [zip_derived_cl1068, zip_derived_cl534])).
% 15.63/2.92 thf(zip_derived_cl1757, plain,
% 15.63/2.92 ((~ (familiar @ n2 @ n4)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | (familiar @ n4 @ n1)
% 15.63/2.92 | (familiar @ n1 @ n3))),
% 15.63/2.92 inference('simplify', [status(thm)], [zip_derived_cl1727])).
% 15.63/2.92 thf(zip_derived_cl94, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1) | (not_familiar @ n4 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl64, zip_derived_cl3, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl38, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.92 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.92 thf(zip_derived_cl161, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1) | (not_familiar @ n1 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl94, zip_derived_cl38])).
% 15.63/2.92 thf(zip_derived_cl95, plain,
% 15.63/2.92 (( (familiar @ n4 @ n2) | (not_familiar @ n4 @ n2))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl65, zip_derived_cl3, zip_derived_cl1])).
% 15.63/2.92 thf(zip_derived_cl84, plain,
% 15.63/2.92 (( (familiar @ n2 @ n1) | (not_familiar @ n2 @ n1))),
% 15.63/2.92 inference('demod', [status(thm)],
% 15.63/2.92 [zip_derived_cl54, zip_derived_cl1, zip_derived_cl0])).
% 15.63/2.92 thf(zip_derived_cl40, plain,
% 15.63/2.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.92 (~ (not_familiar @ X0 @ X1)
% 15.63/2.92 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.92 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.92 thf(zip_derived_cl120, plain,
% 15.63/2.92 (![X0 : $i]:
% 15.63/2.92 ( (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.92 | ~ (not_familiar @ n1 @ X0))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl40])).
% 15.63/2.92 thf(zip_derived_cl170, plain,
% 15.63/2.92 (( (familiar @ n4 @ n2)
% 15.63/2.92 | (familiar @ n2 @ n1)
% 15.63/2.92 | ~ (not_familiar @ n1 @ n4))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl120])).
% 15.63/2.92 thf(zip_derived_cl1092, plain,
% 15.63/2.92 (( (familiar @ n4 @ n1) | (familiar @ n4 @ n2) | (familiar @ n2 @ n1))),
% 15.63/2.92 inference('s_sup-', [status(thm)], [zip_derived_cl161, zip_derived_cl170])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl1093, plain,
% 15.63/2.93 (( (familiar @ n2 @ n1) | (familiar @ n4 @ n1) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1092, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl7754, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n4 @ n1) | (familiar @ n2 @ n1))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl1757, zip_derived_cl1093])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl7755, plain,
% 15.63/2.93 (( (familiar @ n2 @ n1) | (familiar @ n1 @ n3) | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7754, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl7757, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (familiar @ n1 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7755, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl7760, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7757, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl8551, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl8473, zip_derived_cl7760])).
% 15.63/2.93 thf(zip_derived_cl8553, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n6) | (familiar @ n1 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl8551])).
% 15.63/2.93 thf(zip_derived_cl8980, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n2) | (familiar @ n5 @ n4))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl8565, zip_derived_cl8553])).
% 15.63/2.93 thf(zip_derived_cl7757, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (familiar @ n1 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7755, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl7759, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n3) | (familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7757, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl7953, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl7948, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl8111, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n5 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl7759, zip_derived_cl7953])).
% 15.63/2.93 thf(zip_derived_cl8133, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n4) | (familiar @ n1 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl8111])).
% 15.63/2.93 thf(zip_derived_cl8981, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl8980, zip_derived_cl8133])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl8983, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8981, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9024, plain,
% 15.63/2.93 (( (familiar @ n2 @ n6)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1025, zip_derived_cl8983])).
% 15.63/2.93 thf(zip_derived_cl9035, plain,
% 15.63/2.93 ((~ (familiar @ n3 @ n6) | (familiar @ n1 @ n2) | (familiar @ n2 @ n6))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9024])).
% 15.63/2.93 thf(zip_derived_cl9260, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n6)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1174, zip_derived_cl9035])).
% 15.63/2.93 thf(zip_derived_cl9262, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n2 @ n6) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9260])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl9278, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n1 @ n2) | (familiar @ n6 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9262, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl131, plain,
% 15.63/2.93 (( (familiar @ n2 @ n5) | (not_familiar @ n5 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl85, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (not_familiar @ n2 @ n3))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl55, zip_derived_cl1, zip_derived_cl2])).
% 15.63/2.93 thf(zip_derived_cl148, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n3 @ n5)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl189, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n3 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n5 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl148])).
% 15.63/2.93 thf(zip_derived_cl1150, plain,
% 15.63/2.93 (( (familiar @ n2 @ n5) | (familiar @ n2 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl131, zip_derived_cl189])).
% 15.63/2.93 thf(not_equal_5_1, axiom, (not_equal @ n5 @ n1)).
% 15.63/2.93 thf(zip_derived_cl26, plain, ( (not_equal @ n5 @ n1)),
% 15.63/2.93 inference('cnf', [status(esa)], [not_equal_5_1])).
% 15.63/2.93 thf(zip_derived_cl36, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 ( (familiar @ X0 @ X1)
% 15.63/2.93 | (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (person @ X0)
% 15.63/2.93 | ~ (person @ X1)
% 15.63/2.93 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.93 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.93 thf(zip_derived_cl69, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1)
% 15.63/2.93 | (not_familiar @ n5 @ n1)
% 15.63/2.93 | ~ (person @ n5)
% 15.63/2.93 | ~ (person @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl26, zip_derived_cl36])).
% 15.63/2.93 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.93 thf(zip_derived_cl0, plain, ( (person @ n1)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_1])).
% 15.63/2.93 thf(zip_derived_cl99, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl69, zip_derived_cl4, zip_derived_cl0])).
% 15.63/2.93 thf(zip_derived_cl79, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (not_familiar @ n1 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl49, zip_derived_cl0, zip_derived_cl1])).
% 15.63/2.93 thf(zip_derived_cl132, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n5)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.93 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl153, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl132])).
% 15.63/2.93 thf(zip_derived_cl981, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (familiar @ n1 @ n2) | (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl153])).
% 15.63/2.93 thf(zip_derived_cl8983, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8981, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9017, plain,
% 15.63/2.93 (( (familiar @ n2 @ n5)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl981, zip_derived_cl8983])).
% 15.63/2.93 thf(zip_derived_cl9034, plain,
% 15.63/2.93 ((~ (familiar @ n3 @ n5) | (familiar @ n1 @ n2) | (familiar @ n2 @ n5))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9017])).
% 15.63/2.93 thf(zip_derived_cl9159, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n5)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1150, zip_derived_cl9034])).
% 15.63/2.93 thf(zip_derived_cl9161, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n2 @ n5) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9159])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl9178, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9161, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9592, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n5 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl9278, zip_derived_cl9178])).
% 15.63/2.93 thf(zip_derived_cl9607, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n6) | (familiar @ n2 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9592])).
% 15.63/2.93 thf(zip_derived_cl9626, plain,
% 15.63/2.93 (( (familiar @ n4 @ n6)
% 15.63/2.93 | (familiar @ n5 @ n4)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1358, zip_derived_cl9607])).
% 15.63/2.93 thf(zip_derived_cl9278, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n1 @ n2) | (familiar @ n6 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9262, zip_derived_cl37])).
% 15.63/2.93 thf(not_equal_3_4, axiom, (not_equal @ n3 @ n4)).
% 15.63/2.93 thf(zip_derived_cl18, plain, ( (not_equal @ n3 @ n4)),
% 15.63/2.93 inference('cnf', [status(esa)], [not_equal_3_4])).
% 15.63/2.93 thf(zip_derived_cl36, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 ( (familiar @ X0 @ X1)
% 15.63/2.93 | (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (person @ X0)
% 15.63/2.93 | ~ (person @ X1)
% 15.63/2.93 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.93 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.93 thf(zip_derived_cl61, plain,
% 15.63/2.93 (( (familiar @ n3 @ n4)
% 15.63/2.93 | (not_familiar @ n3 @ n4)
% 15.63/2.93 | ~ (person @ n3)
% 15.63/2.93 | ~ (person @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl36])).
% 15.63/2.93 thf(zip_derived_cl2, plain, ( (person @ n3)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_3])).
% 15.63/2.93 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.93 thf(zip_derived_cl91, plain,
% 15.63/2.93 (( (familiar @ n3 @ n4) | (not_familiar @ n3 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl61, zip_derived_cl2, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl95, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2) | (not_familiar @ n4 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl65, zip_derived_cl3, zip_derived_cl1])).
% 15.63/2.93 thf(zip_derived_cl123, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.93 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl171, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl123])).
% 15.63/2.93 thf(zip_derived_cl1095, plain,
% 15.63/2.93 (( (familiar @ n3 @ n4) | (familiar @ n4 @ n2) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl91, zip_derived_cl171])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl1099, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n3 @ n4) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1095, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl94, plain,
% 15.63/2.93 (( (familiar @ n4 @ n1) | (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl64, zip_derived_cl3, zip_derived_cl0])).
% 15.63/2.93 thf(zip_derived_cl79, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (not_familiar @ n1 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl49, zip_derived_cl0, zip_derived_cl1])).
% 15.63/2.93 thf(not_equal_2_4, axiom, (not_equal @ n2 @ n4)).
% 15.63/2.93 thf(zip_derived_cl13, plain, ( (not_equal @ n2 @ n4)),
% 15.63/2.93 inference('cnf', [status(esa)], [not_equal_2_4])).
% 15.63/2.93 thf(zip_derived_cl36, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 ( (familiar @ X0 @ X1)
% 15.63/2.93 | (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (person @ X0)
% 15.63/2.93 | ~ (person @ X1)
% 15.63/2.93 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.93 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.93 thf(zip_derived_cl56, plain,
% 15.63/2.93 (( (familiar @ n2 @ n4)
% 15.63/2.93 | (not_familiar @ n2 @ n4)
% 15.63/2.93 | ~ (person @ n2)
% 15.63/2.93 | ~ (person @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl36])).
% 15.63/2.93 thf(zip_derived_cl1, plain, ( (person @ n2)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_2])).
% 15.63/2.93 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.93 thf(zip_derived_cl86, plain,
% 15.63/2.93 (( (familiar @ n2 @ n4) | (not_familiar @ n2 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl56, zip_derived_cl1, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl40, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.93 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.93 thf(zip_derived_cl125, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n4)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.93 | ~ (not_familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl86, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl151, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n4)
% 15.63/2.93 | ~ (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl125])).
% 15.63/2.93 thf(zip_derived_cl877, plain,
% 15.63/2.93 (( (familiar @ n4 @ n1) | (familiar @ n1 @ n2) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl94, zip_derived_cl151])).
% 15.63/2.93 thf(zip_derived_cl8983, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8981, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9012, plain,
% 15.63/2.93 (( (familiar @ n2 @ n4)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl877, zip_derived_cl8983])).
% 15.63/2.93 thf(zip_derived_cl9033, plain,
% 15.63/2.93 ((~ (familiar @ n3 @ n4) | (familiar @ n1 @ n2) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9012])).
% 15.63/2.93 thf(zip_derived_cl9078, plain,
% 15.63/2.93 (( (familiar @ n2 @ n4)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1099, zip_derived_cl9033])).
% 15.63/2.93 thf(zip_derived_cl9080, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n2 @ n3) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9078])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl9097, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9080, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9447, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl9278, zip_derived_cl9097])).
% 15.63/2.93 thf(zip_derived_cl9462, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n6) | (familiar @ n2 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9447])).
% 15.63/2.93 thf(zip_derived_cl10277, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n2 @ n3) | (familiar @ n5 @ n4))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl9626, zip_derived_cl9462])).
% 15.63/2.93 thf(zip_derived_cl9080, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n2 @ n3) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9078])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl9096, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n1 @ n2) | (familiar @ n4 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9080, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl9178, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl9161, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl9572, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ n5 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl9096, zip_derived_cl9178])).
% 15.63/2.93 thf(zip_derived_cl9599, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n4) | (familiar @ n2 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl9572])).
% 15.63/2.93 thf(zip_derived_cl10278, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10277, zip_derived_cl9599])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl10279, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n3 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10278, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl117, plain,
% 15.63/2.93 (( (familiar @ n1 @ n6) | (not_familiar @ n6 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl155, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n6)
% 15.63/2.93 | ~ (not_familiar @ n6 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl134])).
% 15.63/2.93 thf(zip_derived_cl1026, plain,
% 15.63/2.93 (( (familiar @ n1 @ n6) | (familiar @ n1 @ n2) | (familiar @ n2 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl117, zip_derived_cl155])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl1050, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n6)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n6 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1026, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10316, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n6)
% 15.63/2.93 | ~ (familiar @ n6 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10279, zip_derived_cl1050])).
% 15.63/2.93 thf(zip_derived_cl10322, plain,
% 15.63/2.93 ((~ (familiar @ n6 @ n3) | (familiar @ n1 @ n6) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl10316])).
% 15.63/2.93 thf(zip_derived_cl8981, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl8980, zip_derived_cl8133])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl8982, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n3 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8981, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl9006, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8982, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10660, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n6 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10322, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl10670, plain,
% 15.63/2.93 (( (familiar @ n3 @ n5) | (familiar @ n5 @ n6) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1419, zip_derived_cl10660])).
% 15.63/2.93 thf(zip_derived_cl106, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (not_familiar @ n6 @ n3))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl76, zip_derived_cl5, zip_derived_cl2])).
% 15.63/2.93 thf(zip_derived_cl38, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.93 thf(zip_derived_cl257, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (not_familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl107, plain,
% 15.63/2.93 (( (familiar @ n6 @ n4) | (not_familiar @ n6 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl77, zip_derived_cl5, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl96, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (not_familiar @ n4 @ n3))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl66, zip_derived_cl3, zip_derived_cl2])).
% 15.63/2.93 thf(zip_derived_cl40, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.93 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.93 thf(zip_derived_cl176, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n4 @ n3)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n4)
% 15.63/2.93 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl268, plain,
% 15.63/2.93 (( (familiar @ n6 @ n4)
% 15.63/2.93 | (familiar @ n4 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl107, zip_derived_cl176])).
% 15.63/2.93 thf(zip_derived_cl1444, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (familiar @ n6 @ n4) | (familiar @ n4 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl257, zip_derived_cl268])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl1445, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (familiar @ n6 @ n3) | (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1444, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl10660, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n6 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10322, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl10671, plain,
% 15.63/2.93 (( (familiar @ n4 @ n6) | (familiar @ n4 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1445, zip_derived_cl10660])).
% 15.63/2.93 thf(zip_derived_cl10279, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n3 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10278, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl81, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (not_familiar @ n1 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl51, zip_derived_cl0, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl38, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.93 thf(zip_derived_cl113, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl81, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl151, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n4)
% 15.63/2.93 | ~ (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl125])).
% 15.63/2.93 thf(zip_derived_cl878, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (familiar @ n1 @ n2) | (familiar @ n2 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl113, zip_derived_cl151])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl1024, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl878, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10314, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (familiar @ n4 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10279, zip_derived_cl1024])).
% 15.63/2.93 thf(zip_derived_cl10320, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n3) | (familiar @ n1 @ n4) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl10314])).
% 15.63/2.93 thf(zip_derived_cl9006, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8982, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10397, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n4 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10320, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl10866, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n4 @ n6))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl10671, zip_derived_cl10397])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl10867, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n6 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10866, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl211, plain,
% 15.63/2.93 (( (familiar @ n5 @ n3) | (not_familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl102, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | (not_familiar @ n5 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl72, zip_derived_cl4, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl176, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n4 @ n3)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n4)
% 15.63/2.93 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl237, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4)
% 15.63/2.93 | (familiar @ n4 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl176])).
% 15.63/2.93 thf(zip_derived_cl1332, plain,
% 15.63/2.93 (( (familiar @ n5 @ n3) | (familiar @ n5 @ n4) | (familiar @ n4 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl237])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl1333, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (familiar @ n5 @ n3) | (familiar @ n4 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1332, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl10279, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n3 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10278, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl115, plain,
% 15.63/2.93 (( (familiar @ n1 @ n5) | (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl153, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl79, zip_derived_cl132])).
% 15.63/2.93 thf(zip_derived_cl982, plain,
% 15.63/2.93 (( (familiar @ n1 @ n5) | (familiar @ n1 @ n2) | (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl115, zip_derived_cl153])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl1034, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n5)
% 15.63/2.93 | ~ (familiar @ X0 @ n2)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl982, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10315, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n5)
% 15.63/2.93 | ~ (familiar @ n5 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10279, zip_derived_cl1034])).
% 15.63/2.93 thf(zip_derived_cl10321, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n3) | (familiar @ n1 @ n5) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl10315])).
% 15.63/2.93 thf(zip_derived_cl9006, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl8982, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10417, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n5 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10321, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl10427, plain,
% 15.63/2.93 (( (familiar @ n4 @ n5) | (familiar @ n4 @ n3) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1333, zip_derived_cl10417])).
% 15.63/2.93 thf(zip_derived_cl10397, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n4 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10320, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl10498, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n4 @ n5))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl10427, zip_derived_cl10397])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl10500, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n2)
% 15.63/2.93 | ~ (familiar @ X0 @ n4)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10498, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl10972, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n1 @ n2) | ~ (familiar @ n5 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10867, zip_derived_cl10500])).
% 15.63/2.93 thf(zip_derived_cl10976, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n6) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl10972])).
% 15.63/2.93 thf(zip_derived_cl10985, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n3 @ n5) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10670, zip_derived_cl10976])).
% 15.63/2.93 thf(zip_derived_cl10986, plain,
% 15.63/2.93 (( (familiar @ n3 @ n5) | (familiar @ n1 @ n2))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl10985])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl10987, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | (familiar @ n5 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl10986, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl10417, plain,
% 15.63/2.93 (( (familiar @ n1 @ n2) | ~ (familiar @ n5 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl10321, zip_derived_cl9006])).
% 15.63/2.93 thf(zip_derived_cl11046, plain, ( (familiar @ n1 @ n2)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl10987, zip_derived_cl10417])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl11047, plain, ( (familiar @ n2 @ n1)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl11055, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n2) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11082, plain,
% 15.63/2.93 (( (familiar @ n2 @ n5) | (familiar @ n5 @ n6) | ~ (familiar @ n1 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1391, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl11882, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | (familiar @ n2 @ n5)
% 15.63/2.93 | (familiar @ n5 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11819, zip_derived_cl11082])).
% 15.63/2.93 thf(zip_derived_cl102, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | (not_familiar @ n5 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl72, zip_derived_cl4, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl38, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.93 thf(zip_derived_cl218, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | (not_familiar @ n4 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl99, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl69, zip_derived_cl4, zip_derived_cl0])).
% 15.63/2.93 thf(zip_derived_cl114, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.93 | ~ (not_familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl81, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl201, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (not_familiar @ n4 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl114])).
% 15.63/2.93 thf(zip_derived_cl1200, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | (familiar @ n5 @ n1) | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl218, zip_derived_cl201])).
% 15.63/2.93 thf(zip_derived_cl930, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n4)
% 15.63/2.93 | (familiar @ n3 @ n1)
% 15.63/2.93 | ~ (familiar @ X0 @ n4)
% 15.63/2.93 | ~ (familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl625, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl2626, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4)
% 15.63/2.93 | (familiar @ n5 @ n1)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | (familiar @ n3 @ n1)
% 15.63/2.93 | ~ (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1200, zip_derived_cl930])).
% 15.63/2.93 thf(zip_derived_cl2653, plain,
% 15.63/2.93 ((~ (familiar @ n3 @ n5)
% 15.63/2.93 | (familiar @ n3 @ n1)
% 15.63/2.93 | (familiar @ n5 @ n1)
% 15.63/2.93 | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl2626])).
% 15.63/2.93 thf(zip_derived_cl99, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl69, zip_derived_cl4, zip_derived_cl0])).
% 15.63/2.93 thf(zip_derived_cl38, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.93 thf(zip_derived_cl197, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (not_familiar @ n1 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl101, plain,
% 15.63/2.93 (( (familiar @ n5 @ n3) | (not_familiar @ n5 @ n3))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl71, zip_derived_cl4, zip_derived_cl2])).
% 15.63/2.93 thf(zip_derived_cl136, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n3 @ n1)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl89, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl213, plain,
% 15.63/2.93 (( (familiar @ n5 @ n3)
% 15.63/2.93 | (familiar @ n3 @ n1)
% 15.63/2.93 | ~ (not_familiar @ n1 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl136])).
% 15.63/2.93 thf(zip_derived_cl1244, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (familiar @ n5 @ n3) | (familiar @ n3 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl197, zip_derived_cl213])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl1249, plain,
% 15.63/2.93 (( (familiar @ n3 @ n1) | (familiar @ n5 @ n1) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl1244, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl11243, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (familiar @ n5 @ n1) | (familiar @ n3 @ n1))),
% 15.63/2.93 inference('clc', [status(thm)], [zip_derived_cl2653, zip_derived_cl1249])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl11244, plain,
% 15.63/2.93 (( (familiar @ n3 @ n1) | (familiar @ n1 @ n4) | (familiar @ n1 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11243, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl11247, plain,
% 15.63/2.93 (( (familiar @ n1 @ n5) | (familiar @ n1 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11244, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl11254, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n4) | (familiar @ n5 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11247, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl11046, plain, ( (familiar @ n1 @ n2)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl10987, zip_derived_cl10417])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl11048, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n1) | ~ (familiar @ n2 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11314, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (familiar @ n1 @ n3) | ~ (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11254, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl12137, plain,
% 15.63/2.93 (( (familiar @ n5 @ n6) | (familiar @ n1 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl11882, zip_derived_cl11314])).
% 15.63/2.93 thf(zip_derived_cl11819, plain,
% 15.63/2.93 (( (familiar @ n1 @ n6) | (familiar @ n1 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11814, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl11824, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n4) | (familiar @ n6 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11819, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl11247, plain,
% 15.63/2.93 (( (familiar @ n1 @ n5) | (familiar @ n1 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11244, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl11255, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11247, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11907, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n4)
% 15.63/2.93 | ~ (familiar @ n5 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11824, zip_derived_cl11255])).
% 15.63/2.93 thf(zip_derived_cl11908, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n6) | (familiar @ n1 @ n3) | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl11907])).
% 15.63/2.93 thf(zip_derived_cl12138, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl12137, zip_derived_cl11908])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl12140, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12138, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl12191, plain,
% 15.63/2.93 (( (familiar @ n3 @ n6)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1163, zip_derived_cl12140])).
% 15.63/2.93 thf(zip_derived_cl12200, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n6) | (familiar @ n1 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl12191])).
% 15.63/2.93 thf(zip_derived_cl12446, plain,
% 15.63/2.93 (( (familiar @ n2 @ n6)
% 15.63/2.93 | (familiar @ n4 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1112, zip_derived_cl12200])).
% 15.63/2.93 thf(zip_derived_cl1163, plain,
% 15.63/2.93 (( (familiar @ n6 @ n1) | (familiar @ n1 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl191])).
% 15.63/2.93 thf(zip_derived_cl11048, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n1) | ~ (familiar @ n2 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11067, plain,
% 15.63/2.93 (( (familiar @ n3 @ n6) | (familiar @ n1 @ n3) | ~ (familiar @ n2 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1163, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl13043, plain,
% 15.63/2.93 (( (familiar @ n3 @ n6) | (familiar @ n1 @ n3) | (familiar @ n4 @ n2))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl12446, zip_derived_cl11067])).
% 15.63/2.93 thf(zip_derived_cl11047, plain, ( (familiar @ n2 @ n1)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl12140, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12138, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl12181, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | ~ (familiar @ n4 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl12140])).
% 15.63/2.93 thf(zip_derived_cl13044, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n3 @ n6))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl13043, zip_derived_cl12181])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl13045, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n6 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13044, zip_derived_cl37])).
% 15.63/2.93 thf(not_equal_4_5, axiom, (not_equal @ n4 @ n5)).
% 15.63/2.93 thf(zip_derived_cl24, plain, ( (not_equal @ n4 @ n5)),
% 15.63/2.93 inference('cnf', [status(esa)], [not_equal_4_5])).
% 15.63/2.93 thf(zip_derived_cl36, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 ( (familiar @ X0 @ X1)
% 15.63/2.93 | (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (person @ X0)
% 15.63/2.93 | ~ (person @ X1)
% 15.63/2.93 | ~ (not_equal @ X0 @ X1))),
% 15.63/2.93 inference('cnf', [status(esa)], [familiar_or_not])).
% 15.63/2.93 thf(zip_derived_cl67, plain,
% 15.63/2.93 (( (familiar @ n4 @ n5)
% 15.63/2.93 | (not_familiar @ n4 @ n5)
% 15.63/2.93 | ~ (person @ n4)
% 15.63/2.93 | ~ (person @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl24, zip_derived_cl36])).
% 15.63/2.93 thf(zip_derived_cl3, plain, ( (person @ n4)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_4])).
% 15.63/2.93 thf(zip_derived_cl4, plain, ( (person @ n5)),
% 15.63/2.93 inference('cnf', [status(esa)], [person_5])).
% 15.63/2.93 thf(zip_derived_cl97, plain,
% 15.63/2.93 (( (familiar @ n4 @ n5) | (not_familiar @ n4 @ n5))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl67, zip_derived_cl3, zip_derived_cl4])).
% 15.63/2.93 thf(zip_derived_cl38, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1) | (not_familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_not_familiar])).
% 15.63/2.93 thf(zip_derived_cl178, plain,
% 15.63/2.93 (( (familiar @ n4 @ n5) | (not_familiar @ n5 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl95, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2) | (not_familiar @ n4 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl65, zip_derived_cl3, zip_derived_cl1])).
% 15.63/2.93 thf(zip_derived_cl132, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n5)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.93 | ~ (not_familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl173, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n5 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl132])).
% 15.63/2.93 thf(zip_derived_cl1110, plain,
% 15.63/2.93 (( (familiar @ n4 @ n5) | (familiar @ n4 @ n2) | (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl178, zip_derived_cl173])).
% 15.63/2.93 thf(zip_derived_cl99, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl69, zip_derived_cl4, zip_derived_cl0])).
% 15.63/2.93 thf(zip_derived_cl188, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n3 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n5 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl148])).
% 15.63/2.93 thf(zip_derived_cl1143, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (familiar @ n1 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl188])).
% 15.63/2.93 thf(zip_derived_cl12140, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n1)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12138, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl12186, plain,
% 15.63/2.93 (( (familiar @ n3 @ n5)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n4 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1143, zip_derived_cl12140])).
% 15.63/2.93 thf(zip_derived_cl12199, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n5) | (familiar @ n1 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl12186])).
% 15.63/2.93 thf(zip_derived_cl12343, plain,
% 15.63/2.93 (( (familiar @ n2 @ n5)
% 15.63/2.93 | (familiar @ n4 @ n2)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1110, zip_derived_cl12199])).
% 15.63/2.93 thf(zip_derived_cl1143, plain,
% 15.63/2.93 (( (familiar @ n5 @ n1) | (familiar @ n1 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl188])).
% 15.63/2.93 thf(zip_derived_cl11048, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n1) | ~ (familiar @ n2 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11063, plain,
% 15.63/2.93 (( (familiar @ n3 @ n5) | (familiar @ n1 @ n3) | ~ (familiar @ n2 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1143, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl12685, plain,
% 15.63/2.93 (( (familiar @ n3 @ n5) | (familiar @ n1 @ n3) | (familiar @ n4 @ n2))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl12343, zip_derived_cl11063])).
% 15.63/2.93 thf(zip_derived_cl12181, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | ~ (familiar @ n4 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl12140])).
% 15.63/2.93 thf(zip_derived_cl12686, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n3 @ n5))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl12685, zip_derived_cl12181])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl12688, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12686, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl13129, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n3) | ~ (familiar @ n5 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13045, zip_derived_cl12688])).
% 15.63/2.93 thf(zip_derived_cl13133, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n6) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13129])).
% 15.63/2.93 thf(zip_derived_cl13135, plain,
% 15.63/2.93 (( (familiar @ n2 @ n6) | (familiar @ n5 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1242, zip_derived_cl13133])).
% 15.63/2.93 thf(zip_derived_cl13045, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n6 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13044, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl12138, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n4))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl12137, zip_derived_cl11908])).
% 15.63/2.93 thf(zip_derived_cl1095, plain,
% 15.63/2.93 (( (familiar @ n3 @ n4) | (familiar @ n4 @ n2) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl91, zip_derived_cl171])).
% 15.63/2.93 thf(zip_derived_cl11055, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n2) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl11074, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n3 @ n4) | ~ (familiar @ n1 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1095, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl12164, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n2 @ n3) | (familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12138, zip_derived_cl11074])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl12237, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12164, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl13127, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13045, zip_derived_cl12237])).
% 15.63/2.93 thf(zip_derived_cl13131, plain,
% 15.63/2.93 ((~ (familiar @ n4 @ n6) | (familiar @ n2 @ n3) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13127])).
% 15.63/2.93 thf(zip_derived_cl1358, plain,
% 15.63/2.93 (( (familiar @ n5 @ n6) | (familiar @ n5 @ n4) | (familiar @ n4 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl245])).
% 15.63/2.93 thf(zip_derived_cl13133, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n6) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13129])).
% 15.63/2.93 thf(zip_derived_cl13138, plain,
% 15.63/2.93 (( (familiar @ n4 @ n6) | (familiar @ n5 @ n4) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl1358, zip_derived_cl13133])).
% 15.63/2.93 thf(zip_derived_cl12164, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n2 @ n3) | (familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12138, zip_derived_cl11074])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl12236, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n1 @ n3) | (familiar @ n4 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12164, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl12688, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12686, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl12764, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ n5 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12236, zip_derived_cl12688])).
% 15.63/2.93 thf(zip_derived_cl12789, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n4) | (familiar @ n2 @ n3) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl12764])).
% 15.63/2.93 thf(zip_derived_cl13242, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3)
% 15.63/2.93 | (familiar @ n4 @ n6)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13138, zip_derived_cl12789])).
% 15.63/2.93 thf(zip_derived_cl13245, plain,
% 15.63/2.93 (( (familiar @ n2 @ n3) | (familiar @ n4 @ n6) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13242])).
% 15.63/2.93 thf(zip_derived_cl13860, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl13131, zip_derived_cl13245])).
% 15.63/2.93 thf(zip_derived_cl12688, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n3)
% 15.63/2.93 | ~ (familiar @ n5 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl12686, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl13875, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n3) | ~ (familiar @ n5 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13860, zip_derived_cl12688])).
% 15.63/2.93 thf(zip_derived_cl13882, plain,
% 15.63/2.93 ((~ (familiar @ n5 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13875])).
% 15.63/2.93 thf(zip_derived_cl13896, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n2 @ n6) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13135, zip_derived_cl13882])).
% 15.63/2.93 thf(zip_derived_cl13898, plain,
% 15.63/2.93 (( (familiar @ n2 @ n6) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13896])).
% 15.63/2.93 thf(zip_derived_cl13045, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n6 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13044, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl13114, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n3)
% 15.63/2.93 | ~ (familiar @ X0 @ n6)
% 15.63/2.93 | ~ (familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13045, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl13964, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n1 @ n3) | ~ (familiar @ n3 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13898, zip_derived_cl13114])).
% 15.63/2.93 thf(zip_derived_cl13984, plain,
% 15.63/2.93 ((~ (familiar @ n3 @ n2) | (familiar @ n1 @ n3))),
% 15.63/2.93 inference('simplify', [status(thm)], [zip_derived_cl13964])).
% 15.63/2.93 thf(zip_derived_cl13860, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl13131, zip_derived_cl13245])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl13861, plain,
% 15.63/2.93 (( (familiar @ n1 @ n3) | (familiar @ n3 @ n2))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13860, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl13986, plain, ( (familiar @ n1 @ n3)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl13984, zip_derived_cl13861])).
% 15.63/2.93 thf(zip_derived_cl37, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i]: (~ (familiar @ X0 @ X1) | (familiar @ X1 @ X0))),
% 15.63/2.93 inference('cnf', [status(esa)], [symmetry_of_familiar])).
% 15.63/2.93 thf(zip_derived_cl13987, plain, ( (familiar @ n3 @ n1)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13986, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl11048, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n1) | ~ (familiar @ n2 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11046, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14004, plain, (~ (familiar @ n2 @ n3)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl14053, plain,
% 15.63/2.93 (( (familiar @ n5 @ n3) | (familiar @ n5 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl1226, zip_derived_cl14004])).
% 15.63/2.93 thf(zip_derived_cl13987, plain, ( (familiar @ n3 @ n1)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13986, zip_derived_cl37])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl14003, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n3) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14391, plain,
% 15.63/2.93 (( (familiar @ n5 @ n2) | ~ (familiar @ n1 @ n5))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14053, zip_derived_cl14003])).
% 15.63/2.93 thf(zip_derived_cl11055, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n2) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14520, plain, (~ (familiar @ n1 @ n5)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl14391, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl14522, plain, ( (not_familiar @ n5 @ n1)),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl115, zip_derived_cl14520])).
% 15.63/2.93 thf(zip_derived_cl118, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n1 @ n6)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n1)
% 15.63/2.93 | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl257, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (not_familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl105, plain,
% 15.63/2.93 (( (familiar @ n6 @ n2) | (not_familiar @ n6 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl75, zip_derived_cl5, zip_derived_cl1])).
% 15.63/2.93 thf(zip_derived_cl123, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n2 @ n3)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n2)
% 15.63/2.93 | ~ (not_familiar @ n3 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl253, plain,
% 15.63/2.93 (( (familiar @ n6 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n3 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl105, zip_derived_cl123])).
% 15.63/2.93 thf(zip_derived_cl1380, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (familiar @ n6 @ n2) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl257, zip_derived_cl253])).
% 15.63/2.93 thf(zip_derived_cl14004, plain, (~ (familiar @ n2 @ n3)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl14055, plain,
% 15.63/2.93 (( (familiar @ n6 @ n3) | (familiar @ n6 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl1380, zip_derived_cl14004])).
% 15.63/2.93 thf(zip_derived_cl14003, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n3) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14394, plain,
% 15.63/2.93 (( (familiar @ n6 @ n2) | ~ (familiar @ n1 @ n6))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14055, zip_derived_cl14003])).
% 15.63/2.93 thf(zip_derived_cl11055, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n2) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14671, plain, (~ (familiar @ n1 @ n6)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl14394, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl14674, plain,
% 15.63/2.93 (![X0 : $i]: (~ (not_familiar @ X0 @ n1) | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl118, zip_derived_cl14671])).
% 15.63/2.93 thf(zip_derived_cl14697, plain, (~ (not_familiar @ n6 @ n5)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14522, zip_derived_cl14674])).
% 15.63/2.93 thf(zip_derived_cl14701, plain, ( (familiar @ n6 @ n5)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl108, zip_derived_cl14697])).
% 15.63/2.93 thf(zip_derived_cl82, plain,
% 15.63/2.93 (( (familiar @ n1 @ n5) | (not_familiar @ n1 @ n5))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl52, zip_derived_cl0, zip_derived_cl4])).
% 15.63/2.93 thf(zip_derived_cl14520, plain, (~ (familiar @ n1 @ n5)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl14391, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl14521, plain, ( (not_familiar @ n1 @ n5)),
% 15.63/2.93 inference('demod', [status(thm)], [zip_derived_cl82, zip_derived_cl14520])).
% 15.63/2.93 thf(zip_derived_cl102, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | (not_familiar @ n5 @ n4))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl72, zip_derived_cl4, zip_derived_cl3])).
% 15.63/2.93 thf(zip_derived_cl40, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (not_familiar @ X0 @ X1)
% 15.63/2.93 | ~ (not_familiar @ X2 @ X0)
% 15.63/2.93 | ~ (not_familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.63/2.93 thf(zip_derived_cl219, plain,
% 15.63/2.93 (![X0 : $i]:
% 15.63/2.93 ( (familiar @ n5 @ n4)
% 15.63/2.93 | ~ (not_familiar @ X0 @ n5)
% 15.63/2.93 | ~ (not_familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl40])).
% 15.63/2.93 thf(zip_derived_cl14571, plain,
% 15.63/2.93 (( (familiar @ n5 @ n4) | ~ (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14521, zip_derived_cl219])).
% 15.63/2.93 thf(zip_derived_cl113, plain,
% 15.63/2.93 (( (familiar @ n1 @ n4) | (not_familiar @ n4 @ n1))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl81, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl175, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (not_familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl171, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2)
% 15.63/2.93 | (familiar @ n2 @ n3)
% 15.63/2.93 | ~ (not_familiar @ n3 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl123])).
% 15.63/2.93 thf(zip_derived_cl1096, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (familiar @ n4 @ n2) | (familiar @ n2 @ n3))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl175, zip_derived_cl171])).
% 15.63/2.93 thf(zip_derived_cl14004, plain, (~ (familiar @ n2 @ n3)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl11048])).
% 15.63/2.93 thf(zip_derived_cl14034, plain,
% 15.63/2.93 (( (familiar @ n4 @ n3) | (familiar @ n4 @ n2))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl1096, zip_derived_cl14004])).
% 15.63/2.93 thf(zip_derived_cl14003, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n3) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl13987, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14207, plain,
% 15.63/2.93 (( (familiar @ n4 @ n2) | ~ (familiar @ n1 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14034, zip_derived_cl14003])).
% 15.63/2.93 thf(zip_derived_cl11055, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n2) | ~ (familiar @ n1 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl11047, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14413, plain, (~ (familiar @ n1 @ n4)),
% 15.63/2.93 inference('clc', [status(thm)],
% 15.63/2.93 [zip_derived_cl14207, zip_derived_cl11055])).
% 15.63/2.93 thf(zip_derived_cl14415, plain, ( (not_familiar @ n4 @ n1)),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl113, zip_derived_cl14413])).
% 15.63/2.93 thf(zip_derived_cl14577, plain, ( (familiar @ n5 @ n4)),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl14571, zip_derived_cl14415])).
% 15.63/2.93 thf(zip_derived_cl39, plain,
% 15.63/2.93 (![X0 : $i, X1 : $i, X2 : $i]:
% 15.63/2.93 (~ (familiar @ X0 @ X1)
% 15.63/2.93 | ~ (familiar @ X2 @ X0)
% 15.63/2.93 | ~ (familiar @ X1 @ X2))),
% 15.63/2.93 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.63/2.93 thf(zip_derived_cl14608, plain,
% 15.63/2.93 (![X0 : $i]: (~ (familiar @ X0 @ n5) | ~ (familiar @ n4 @ X0))),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14577, zip_derived_cl39])).
% 15.63/2.93 thf(zip_derived_cl14833, plain, (~ (familiar @ n4 @ n6)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14701, zip_derived_cl14608])).
% 15.63/2.93 thf(zip_derived_cl180, plain,
% 15.63/2.93 (( (familiar @ n4 @ n6) | (not_familiar @ n6 @ n4))),
% 15.63/2.93 inference('s_sup-', [status(thm)], [zip_derived_cl98, zip_derived_cl38])).
% 15.63/2.93 thf(zip_derived_cl14415, plain, ( (not_familiar @ n4 @ n1)),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl113, zip_derived_cl14413])).
% 15.63/2.93 thf(zip_derived_cl14674, plain,
% 15.63/2.93 (![X0 : $i]: (~ (not_familiar @ X0 @ n1) | ~ (not_familiar @ n6 @ X0))),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl118, zip_derived_cl14671])).
% 15.63/2.93 thf(zip_derived_cl14696, plain, (~ (not_familiar @ n6 @ n4)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl14415, zip_derived_cl14674])).
% 15.63/2.93 thf(zip_derived_cl14700, plain, ( (familiar @ n4 @ n6)),
% 15.63/2.93 inference('s_sup-', [status(thm)],
% 15.63/2.93 [zip_derived_cl180, zip_derived_cl14696])).
% 15.63/2.93 thf(zip_derived_cl14835, plain, ($false),
% 15.63/2.93 inference('demod', [status(thm)],
% 15.63/2.93 [zip_derived_cl14833, zip_derived_cl14700])).
% 15.63/2.93
% 15.63/2.93 % SZS output end Refutation
% 15.63/2.93
% 15.63/2.93
% 15.63/2.93 % Terminating...
% 16.42/3.03 % Runner terminated.
% 16.42/3.05 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------