%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT170^3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:21:46 AM UTC 2026
% Result : Theorem 110.83s 16.66s
% Output : CNFRefutation 110.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT170^3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n001.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 13:40:03 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running higher-order theorem proving
% 0.30/0.48 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p
% 110.83/16.66 % Version: 3.5.1-ho
% 110.83/16.66 % Preprocessing class: HMLMSMSMSSLNHSA.
% 110.83/16.66 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 110.83/16.66 % Starting sh2lt with 1500s (5) cores
% 110.83/16.66 % Starting new_ho_6 with 300s (1) cores
% 110.83/16.66 % Starting almost_fo_2 with 300s (1) cores
% 110.83/16.66 % Starting sh5l with 300s (1) cores
% 110.83/16.66 % sh2lt with pid 1245543 completed with status 0
% 110.83/16.66 % Result found by sh2lt
% 110.83/16.66 % Preprocessing class: HMLMSMSMSSLNHSA.
% 110.83/16.66 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 110.83/16.66 % Starting sh2lt with 1500s (5) cores
% 110.83/16.66 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 110.83/16.66 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 110.83/16.66 % Search class: HGHSM-FSLM32-DHSFFSBN
% 110.83/16.66 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 110.83/16.66 % Starting SubtermCWHack with 136s (1) cores
% 110.83/16.66 % Starting sh2lt with 151s (1) cores
% 110.83/16.66 % Starting sh4l with 214s (1) cores
% 110.83/16.66 % Starting pre_casc_4 with 204s (1) cores
% 110.83/16.66 % Starting lpo5_fix with 136s (1) cores
% 110.83/16.66 % sh2lt with pid 1245564 completed with status 0
% 110.83/16.66 % Result found by sh2lt
% 110.83/16.66 % Preprocessing class: HMLMSMSMSSLNHSA.
% 110.83/16.66 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 110.83/16.66 % Starting sh2lt with 1500s (5) cores
% 110.83/16.66 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 110.83/16.66 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 110.83/16.66 % Search class: HGHSM-FSLM32-DHSFFSBN
% 110.83/16.66 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 110.83/16.66 % Starting SubtermCWHack with 136s (1) cores
% 110.83/16.66 % Starting sh2lt with 151s (1) cores
% 110.83/16.66 % Preprocessing time : 0.018 s
% 110.83/16.66 % Presaturation interreduction done
% 110.83/16.66
% 110.83/16.66 % Proof found!
% 110.83/16.66 % SZS status Theorem
% 110.83/16.66 % SZS output start CNFRefutation
% 110.83/16.66 thf(decl_sort1, type, produc1572197287le_alt: $tType).
% 110.83/16.66 thf(decl_sort2, type, arrow_1196572341e_indi: $tType).
% 110.83/16.66 thf(decl_sort3, type, arrow_1389031998le_alt: $tType).
% 110.83/16.66 thf(decl_sort4, type, list_A1402527603le_alt: $tType).
% 110.83/16.66 thf(decl_26, type, arrow_1982173296le_Lin: (produc1572197287le_alt > $o) > $o).
% 110.83/16.66 thf(decl_27, type, arrow_1647925946e_Prof: (arrow_1196572341e_indi > produc1572197287le_alt > $o) > $o).
% 110.83/16.66 thf(decl_29, type, arrow_1865170000_below: (produc1572197287le_alt > $o) > arrow_1389031998le_alt > arrow_1389031998le_alt > produc1572197287le_alt > $o).
% 110.83/16.66 thf(decl_64, type, pi_Arr1309696186_alt_o: (arrow_1196572341e_indi > $o) > (arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o) > (arrow_1196572341e_indi > produc1572197287le_alt > $o) > $o).
% 110.83/16.66 thf(decl_89, type, append1092755459le_alt: list_A1402527603le_alt > list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(decl_99, type, butlas1188620858le_alt: list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(decl_108, type, distin1149997281le_alt: list_A1402527603le_alt > $o).
% 110.83/16.66 thf(decl_153, type, last_A2130988295le_alt: list_A1402527603le_alt > arrow_1389031998le_alt).
% 110.83/16.66 thf(decl_175, type, cons_A1142416030le_alt: arrow_1389031998le_alt > list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(decl_185, type, nil_Ar52383470le_alt: list_A1402527603le_alt).
% 110.83/16.66 thf(decl_207, type, rev_Ar2020079950le_alt: list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(decl_212, type, rotate1249022267le_alt: list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(decl_217, type, set_Ar1491127311le_alt: list_A1402527603le_alt > arrow_1389031998le_alt > $o).
% 110.83/16.66 thf(decl_278, type, top_to54564308indi_o: arrow_1196572341e_indi > $o).
% 110.83/16.66 thf(decl_287, type, produc897867031le_alt: arrow_1389031998le_alt > arrow_1389031998le_alt > produc1572197287le_alt).
% 110.83/16.66 thf(decl_359, type, member822980838_alt_o: (arrow_1196572341e_indi > produc1572197287le_alt > $o) > ((arrow_1196572341e_indi > produc1572197287le_alt > $o) > $o) > $o).
% 110.83/16.66 thf(decl_365, type, member1241905979_alt_o: (produc1572197287le_alt > $o) > ((produc1572197287le_alt > $o) > $o) > $o).
% 110.83/16.66 thf(decl_375, type, member998036369le_alt: arrow_1389031998le_alt > (arrow_1389031998le_alt > $o) > $o).
% 110.83/16.66 thf(decl_376, type, member1818997282e_indi: arrow_1196572341e_indi > (arrow_1196572341e_indi > $o) > $o).
% 110.83/16.66 thf(decl_383, type, member285112084le_alt: produc1572197287le_alt > (produc1572197287le_alt > $o) > $o).
% 110.83/16.66 thf(decl_400, type, p: arrow_1196572341e_indi > produc1572197287le_alt > $o).
% 110.83/16.66 thf(decl_401, type, a: arrow_1389031998le_alt).
% 110.83/16.66 thf(decl_402, type, b: arrow_1389031998le_alt).
% 110.83/16.66 thf(decl_403, type, c: arrow_1389031998le_alt).
% 110.83/16.66 thf(decl_404, type, esk1_0: arrow_1196572341e_indi).
% 110.83/16.66 thf(decl_575, type, epred18_0: arrow_1196572341e_indi > produc1572197287le_alt > $o).
% 110.83/16.66 thf(decl_578, type, epred21_0: arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o).
% 110.83/16.66 thf(decl_583, type, esk155_0: arrow_1389031998le_alt > list_A1402527603le_alt > list_A1402527603le_alt).
% 110.83/16.66 thf(fact_87_PiE, axiom, ![X223:arrow_1196572341e_indi, X224:arrow_1196572341e_indi > produc1572197287le_alt > $o, X225:arrow_1196572341e_indi > $o, X226:arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o]:(((member822980838_alt_o @ X224 @ (pi_Arr1309696186_alt_o @ X225 @ X226))=>(~((member1241905979_alt_o @ (X224 @ X223) @ (X226 @ X223)))=>~((member1818997282e_indi @ X223 @ X225))))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_87_PiE)).
% 110.83/16.66 thf(fact_12_in__below, axiom, ![X4:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o, X8:arrow_1389031998le_alt, X9:arrow_1389031998le_alt]:((((X8)!=(X9))=>((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)=>((member285112084le_alt @ (produc897867031le_alt @ X4 @ X5) @ (arrow_1865170000_below @ X6 @ X8 @ X9))<=>((((X4)!=(X5))&(((X5)=(X8))=>(member285112084le_alt @ (produc897867031le_alt @ X4 @ X9) @ X6)))&(((X5)!=(X8))=>((((X4)=(X8))=>(((X5)=(X9))|(member285112084le_alt @ (produc897867031le_alt @ X9 @ X5) @ X6)))&(((X4)!=(X8))=>(member285112084le_alt @ (produc897867031le_alt @ X4 @ X5) @ X6))))))))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_12_in__below)).
% 110.83/16.66 thf(fact_340_Prof__def, axiom, ((arrow_1647925946e_Prof)=(pi_Arr1309696186_alt_o @ top_to54564308indi_o @ (^[X1179:arrow_1196572341e_indi]:(arrow_1982173296le_Lin)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_340_Prof__def)).
% 110.83/16.66 thf(fact_367_iso__tuple__UNIV__I, axiom, ![X1233:arrow_1196572341e_indi]:((member1818997282e_indi @ X1233 @ top_to54564308indi_o)), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_367_iso__tuple__UNIV__I)).
% 110.83/16.66 thf(conj_0, conjecture, ![X1:arrow_1196572341e_indi]:(((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ X1))<=>(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ X1) @ c @ b)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', conj_0)).
% 110.83/16.66 thf(fact_623_rev__singleton__conv, axiom, ![X1912:list_A1402527603le_alt, X1913:arrow_1389031998le_alt]:((((rev_Ar2020079950le_alt @ X1912)=(cons_A1142416030le_alt @ X1913 @ nil_Ar52383470le_alt))<=>((X1912)=(cons_A1142416030le_alt @ X1913 @ nil_Ar52383470le_alt)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_623_rev__singleton__conv)).
% 110.83/16.66 thf(fact_628_rev_Osimps_I2_J, axiom, ![X1927:arrow_1389031998le_alt, X1928:list_A1402527603le_alt]:(((rev_Ar2020079950le_alt @ (cons_A1142416030le_alt @ X1927 @ X1928))=(append1092755459le_alt @ (rev_Ar2020079950le_alt @ X1928) @ (cons_A1142416030le_alt @ X1927 @ nil_Ar52383470le_alt)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_628_rev_Osimps_I2_J)).
% 110.83/16.66 thf(fact_708_distinct_Osimps_I2_J, axiom, ![X2151:arrow_1389031998le_alt, X2152:list_A1402527603le_alt]:(((distin1149997281le_alt @ (cons_A1142416030le_alt @ X2151 @ X2152))<=>(~((member998036369le_alt @ X2151 @ (set_Ar1491127311le_alt @ X2152)))&(distin1149997281le_alt @ X2152)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_708_distinct_Osimps_I2_J)).
% 110.83/16.66 thf(fact_442_rotate__simps, axiom, ![X1396:arrow_1389031998le_alt, X1397:list_A1402527603le_alt]:((((rotate1249022267le_alt @ nil_Ar52383470le_alt)=(nil_Ar52383470le_alt))&((rotate1249022267le_alt @ (cons_A1142416030le_alt @ X1396 @ X1397))=(append1092755459le_alt @ X1397 @ (cons_A1142416030le_alt @ X1396 @ nil_Ar52383470le_alt))))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_442_rotate__simps)).
% 110.83/16.66 thf(fact_0__096P_A_058_AProf_096, axiom, (member822980838_alt_o @ p @ arrow_1647925946e_Prof), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_0__096P_A_058_AProf_096)).
% 110.83/16.66 thf(fact_319_mem__def, axiom, ![X1137:produc1572197287le_alt, X1138:produc1572197287le_alt > $o]:(((member285112084le_alt @ X1137 @ X1138)<=>(X1138 @ X1137))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_319_mem__def)).
% 110.83/16.66 thf(fact_433_snoc__eq__iff__butlast, axiom, ![X1363:list_A1402527603le_alt, X1364:arrow_1389031998le_alt, X1365:list_A1402527603le_alt]:((((append1092755459le_alt @ X1363 @ (cons_A1142416030le_alt @ X1364 @ nil_Ar52383470le_alt))=(X1365))<=>((((X1365)!=(nil_Ar52383470le_alt))&((butlas1188620858le_alt @ X1365)=(X1363)))&((last_A2130988295le_alt @ X1365)=(X1364))))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_433_snoc__eq__iff__butlast)).
% 110.83/16.66 thf(fact_605_rev_Osimps_I1_J, axiom, ((rev_Ar2020079950le_alt @ nil_Ar52383470le_alt)=(nil_Ar52383470le_alt)), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_605_rev_Osimps_I1_J)).
% 110.83/16.66 thf(fact_697_set__rotate1, axiom, ![X2130:list_A1402527603le_alt]:(((set_Ar1491127311le_alt @ (rotate1249022267le_alt @ X2130))=(set_Ar1491127311le_alt @ X2130))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_697_set__rotate1)).
% 110.83/16.66 thf(fact_422_butlast__snoc, axiom, ![X1341:list_A1402527603le_alt, X1342:arrow_1389031998le_alt]:(((butlas1188620858le_alt @ (append1092755459le_alt @ X1341 @ (cons_A1142416030le_alt @ X1342 @ nil_Ar52383470le_alt)))=(X1341))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_422_butlast__snoc)).
% 110.83/16.66 thf(fact_4_dist, axiom, (distin1149997281le_alt @ (cons_A1142416030le_alt @ a @ (cons_A1142416030le_alt @ b @ (cons_A1142416030le_alt @ c @ nil_Ar52383470le_alt)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_4_dist)).
% 110.83/16.66 thf(fact_689_in__set__butlastD, axiom, ![X2114:arrow_1389031998le_alt, X2115:list_A1402527603le_alt]:(((member998036369le_alt @ X2114 @ (set_Ar1491127311le_alt @ (butlas1188620858le_alt @ X2115)))=>(member998036369le_alt @ X2114 @ (set_Ar1491127311le_alt @ X2115)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_689_in__set__butlastD)).
% 110.83/16.66 thf(fact_725_last__in__set, axiom, ![X2203:list_A1402527603le_alt]:((((X2203)!=(nil_Ar52383470le_alt))=>(member998036369le_alt @ (last_A2130988295le_alt @ X2203) @ (set_Ar1491127311le_alt @ X2203)))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_725_last__in__set)).
% 110.83/16.66 thf(fact_423_last__snoc, axiom, ![X1343:list_A1402527603le_alt, X1344:arrow_1389031998le_alt]:(((last_A2130988295le_alt @ (append1092755459le_alt @ X1343 @ (cons_A1142416030le_alt @ X1344 @ nil_Ar52383470le_alt)))=(X1344))), file('/export/starexec/sandbox/tmp/tmp.LRW0tyahYp/E---3.1_1245484.p', fact_423_last__snoc)).
% 110.83/16.66 thf(c_0_19, plain, ![X223:arrow_1196572341e_indi, X224:arrow_1196572341e_indi > produc1572197287le_alt > $o, X225:arrow_1196572341e_indi > $o, X226:arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o]:(((member822980838_alt_o @ X224 @ (pi_Arr1309696186_alt_o @ X225 @ X226))=>(~(member1241905979_alt_o @ (X224 @ X223) @ (X226 @ X223))=>~(member1818997282e_indi @ X223 @ X225)))), inference(fof_simplification,[status(thm)],[fact_87_PiE])).
% 110.83/16.66 thf(c_0_20, plain, ![X4:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o, X8:arrow_1389031998le_alt, X9:arrow_1389031998le_alt]:((((X8)!=(X9))=>((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)=>((member285112084le_alt @ (produc897867031le_alt @ X4 @ X5) @ (arrow_1865170000_below @ X6 @ X8 @ X9))<=>((((X4)!=(X5))&(((X5)=(X8))=>(member285112084le_alt @ (produc897867031le_alt @ X4 @ X9) @ X6)))&(((X5)!=(X8))=>((((X4)=(X8))=>(((X5)=(X9))|(member285112084le_alt @ (produc897867031le_alt @ X9 @ X5) @ X6)))&(((X4)!=(X8))=>(member285112084le_alt @ (produc897867031le_alt @ X4 @ X5) @ X6))))))))), inference(fof_simplification,[status(thm)],[fact_12_in__below])).
% 110.83/16.66 thf(c_0_21, plain, ![X4731:arrow_1196572341e_indi, X4732:arrow_1196572341e_indi > produc1572197287le_alt > $o, X4733:arrow_1196572341e_indi > $o, X4734:arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o]:((~(member822980838_alt_o @ X4732 @ (pi_Arr1309696186_alt_o @ X4733 @ X4734))|((member1241905979_alt_o @ (X4732 @ X4731) @ (X4734 @ X4731))|~(member1818997282e_indi @ X4731 @ X4733)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])).
% 110.83/16.66 thf(c_0_22, plain, ((arrow_1647925946e_Prof)=(pi_Arr1309696186_alt_o @ top_to54564308indi_o @ (^[Z0:arrow_1196572341e_indi]:(arrow_1982173296le_Lin)))), inference(fof_simplification,[status(thm)],[fact_340_Prof__def])).
% 110.83/16.66 thf(c_0_23, plain, ![X5393:arrow_1196572341e_indi]:(((epred21_0 @ X5393)=(arrow_1982173296le_Lin))), introduced(definition)).
% 110.83/16.66 thf(c_0_24, plain, ![X5492:arrow_1196572341e_indi]:(((epred21_0 @ X5492)=(arrow_1982173296le_Lin))), inference(variable_rename,[status(thm)],[])).
% 110.83/16.66 thf(c_0_25, plain, ![X4765:arrow_1196572341e_indi]:((member1818997282e_indi @ X4765 @ top_to54564308indi_o)), inference(variable_rename,[status(thm)],[fact_367_iso__tuple__UNIV__I])).
% 110.83/16.66 thf(c_0_26, negated_conjecture, ~(![X1:arrow_1196572341e_indi]:(((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ X1))<=>(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ X1) @ c @ b))))), inference(assume_negation,[status(cth)],[conj_0])).
% 110.83/16.66 thf(c_0_27, plain, ![X4468:list_A1402527603le_alt, X4469:arrow_1389031998le_alt]:(((((rev_Ar2020079950le_alt @ X4468)!=(cons_A1142416030le_alt @ X4469 @ nil_Ar52383470le_alt))|((X4468)=(cons_A1142416030le_alt @ X4469 @ nil_Ar52383470le_alt)))&(((X4468)!=(cons_A1142416030le_alt @ X4469 @ nil_Ar52383470le_alt))|((rev_Ar2020079950le_alt @ X4468)=(cons_A1142416030le_alt @ X4469 @ nil_Ar52383470le_alt))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_623_rev__singleton__conv])])])).
% 110.83/16.66 thf(c_0_28, plain, ![X4472:arrow_1389031998le_alt, X4473:list_A1402527603le_alt]:(((rev_Ar2020079950le_alt @ (cons_A1142416030le_alt @ X4472 @ X4473))=(append1092755459le_alt @ (rev_Ar2020079950le_alt @ X4473) @ (cons_A1142416030le_alt @ X4472 @ nil_Ar52383470le_alt)))), inference(variable_rename,[status(thm)],[fact_628_rev_Osimps_I2_J])).
% 110.83/16.66 thf(c_0_29, plain, ![X5482:list_A1402527603le_alt, X5483:arrow_1389031998le_alt]:(((esk155_0 @ X5483 @ X5482)=(append1092755459le_alt @ X5482 @ (cons_A1142416030le_alt @ X5483 @ nil_Ar52383470le_alt)))), inference(variable_rename,[status(thm)],[])).
% 110.83/16.66 thf(c_0_30, plain, ![X4274:arrow_1389031998le_alt, X4275:arrow_1389031998le_alt, X4276:produc1572197287le_alt > $o, X4277:arrow_1389031998le_alt, X4278:arrow_1389031998le_alt]:(((((((X4274)!=(X4275))|~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(((X4275)!=(X4277))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278))))&((((X4274)!=(X4277))|(((X4275)=(X4278))|(member285112084le_alt @ (produc897867031le_alt @ X4278 @ X4275) @ X4276))|((X4275)=(X4277))|~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(((X4274)=(X4277))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|((X4275)=(X4277))|~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))))&(((((X4275)!=(X4277))|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(((((X4274)!=(X4277))|((X4274)=(X4277))|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|((X4274)=(X4277))|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278))))&(((((X4274)!=(X4277))|((X4275)!=(X4278))|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|((X4275)!=(X4278))|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278))))&((((X4274)!=(X4277))|~(member285112084le_alt @ (produc897867031le_alt @ X4278 @ X4275) @ X4276)|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|~(member285112084le_alt @ (produc897867031le_alt @ X4278 @ X4275) @ X4276)|(((X4275)=(X4277))|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))))))&((((X4275)!=(X4277))|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(((((X4274)!=(X4277))|((X4274)=(X4277))|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|((X4274)=(X4277))|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278))))&(((((X4274)!=(X4277))|((X4275)!=(X4278))|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|((X4275)!=(X4278))|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278))))&((((X4274)!=(X4277))|~(member285112084le_alt @ (produc897867031le_alt @ X4278 @ X4275) @ X4276)|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))&(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ X4276)|~(member285112084le_alt @ (produc897867031le_alt @ X4278 @ X4275) @ X4276)|(~(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4278) @ X4276)|((X4274)=(X4275)))|(member285112084le_alt @ (produc897867031le_alt @ X4274 @ X4275) @ (arrow_1865170000_below @ X4276 @ X4277 @ X4278))|~(member1241905979_alt_o @ X4276 @ arrow_1982173296le_Lin)|((X4277)=(X4278)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])).
% 110.83/16.66 thf(c_0_31, plain, ![X38:arrow_1196572341e_indi > produc1572197287le_alt > $o, X1:arrow_1196572341e_indi, X226:arrow_1196572341e_indi > (produc1572197287le_alt > $o) > $o, X89:arrow_1196572341e_indi > $o]:(((member1241905979_alt_o @ (X38 @ X1) @ (X226 @ X1))|~((member822980838_alt_o @ X38 @ (pi_Arr1309696186_alt_o @ X89 @ X226)))|~((member1818997282e_indi @ X1 @ X89)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 110.83/16.66 thf(c_0_32, plain, ((arrow_1647925946e_Prof)=(pi_Arr1309696186_alt_o @ top_to54564308indi_o @ epred21_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_22]), c_0_23])).
% 110.83/16.66 thf(c_0_33, plain, ![X1:arrow_1196572341e_indi]:(((epred21_0 @ X1)=(arrow_1982173296le_Lin))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 110.83/16.66 thf(c_0_34, plain, ![X1:arrow_1196572341e_indi]:((member1818997282e_indi @ X1 @ top_to54564308indi_o)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 110.83/16.66 thf(c_0_35, negated_conjecture, ((~(member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0))|~(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ esk1_0) @ c @ b)))&((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0))|(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ esk1_0) @ c @ b)))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])).
% 110.83/16.66 thf(c_0_36, plain, ![X5496:arrow_1196572341e_indi]:(((epred18_0 @ X5496)=(arrow_1865170000_below @ (p @ X5496) @ c @ b))), inference(variable_rename,[status(thm)],[])).
% 110.83/16.66 thf(c_0_37, plain, ![X2151:arrow_1389031998le_alt, X2152:list_A1402527603le_alt]:(((distin1149997281le_alt @ (cons_A1142416030le_alt @ X2151 @ X2152))<=>(~(member998036369le_alt @ X2151 @ (set_Ar1491127311le_alt @ X2152))&(distin1149997281le_alt @ X2152)))), inference(fof_simplification,[status(thm)],[fact_708_distinct_Osimps_I2_J])).
% 110.83/16.66 thf(c_0_38, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:((((rev_Ar2020079950le_alt @ X11)=(cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt))|((X11)!=(cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 110.83/16.66 thf(c_0_39, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((rev_Ar2020079950le_alt @ (cons_A1142416030le_alt @ X2 @ X11))=(append1092755459le_alt @ (rev_Ar2020079950le_alt @ X11) @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 110.83/16.66 thf(c_0_40, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((esk155_0 @ X2 @ X11)=(append1092755459le_alt @ X11 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 110.83/16.66 thf(c_0_41, plain, ![X4844:arrow_1389031998le_alt, X4845:list_A1402527603le_alt]:((((rotate1249022267le_alt @ nil_Ar52383470le_alt)=(nil_Ar52383470le_alt))&((rotate1249022267le_alt @ (cons_A1142416030le_alt @ X4844 @ X4845))=(append1092755459le_alt @ X4845 @ (cons_A1142416030le_alt @ X4844 @ nil_Ar52383470le_alt))))), inference(variable_rename,[status(thm)],[fact_442_rotate__simps])).
% 110.83/16.66 thf(c_0_42, plain, ![X2:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X4:arrow_1389031998le_alt, X7:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o]:(((member285112084le_alt @ (produc897867031le_alt @ X5 @ X7) @ X6)|((X4)=(X7))|((X2)!=(X4))|~((member285112084le_alt @ (produc897867031le_alt @ X5 @ X2) @ (arrow_1865170000_below @ X6 @ X4 @ X7)))|~((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 110.83/16.66 thf(c_0_43, plain, ![X1:arrow_1196572341e_indi, X38:arrow_1196572341e_indi > produc1572197287le_alt > $o]:(((member1241905979_alt_o @ (X38 @ X1) @ arrow_1982173296le_Lin)|~((member822980838_alt_o @ X38 @ arrow_1647925946e_Prof)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33]), c_0_34])])).
% 110.83/16.66 thf(c_0_44, plain, (member822980838_alt_o @ p @ arrow_1647925946e_Prof), inference(split_conjunct,[status(thm)],[fact_0__096P_A_058_AProf_096])).
% 110.83/16.66 thf(c_0_45, plain, ![X4272:produc1572197287le_alt, X4273:produc1572197287le_alt > $o]:(((~(member285112084le_alt @ X4272 @ X4273)|(X4273 @ X4272))&(~(X4273 @ X4272)|(member285112084le_alt @ X4272 @ X4273)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_319_mem__def])])])).
% 110.83/16.66 thf(c_0_46, negated_conjecture, ((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0))|(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ esk1_0) @ c @ b))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 110.83/16.66 thf(c_0_47, plain, ![X1:arrow_1196572341e_indi]:(((epred18_0 @ X1)=(arrow_1865170000_below @ (p @ X1) @ c @ b))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 110.83/16.66 thf(c_0_48, plain, ![X1363:list_A1402527603le_alt, X1364:arrow_1389031998le_alt, X1365:list_A1402527603le_alt]:((((append1092755459le_alt @ X1363 @ (cons_A1142416030le_alt @ X1364 @ nil_Ar52383470le_alt))=(X1365))<=>((((X1365)!=(nil_Ar52383470le_alt))&((butlas1188620858le_alt @ X1365)=(X1363)))&((last_A2130988295le_alt @ X1365)=(X1364))))), inference(fof_simplification,[status(thm)],[fact_433_snoc__eq__iff__butlast])).
% 110.83/16.66 thf(c_0_49, plain, ![X4395:arrow_1389031998le_alt, X4396:list_A1402527603le_alt]:((((~(member998036369le_alt @ X4395 @ (set_Ar1491127311le_alt @ X4396))|~(distin1149997281le_alt @ (cons_A1142416030le_alt @ X4395 @ X4396)))&((distin1149997281le_alt @ X4396)|~(distin1149997281le_alt @ (cons_A1142416030le_alt @ X4395 @ X4396))))&((member998036369le_alt @ X4395 @ (set_Ar1491127311le_alt @ X4396))|~(distin1149997281le_alt @ X4396)|(distin1149997281le_alt @ (cons_A1142416030le_alt @ X4395 @ X4396))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])])).
% 110.83/16.66 thf(c_0_50, plain, ![X2:arrow_1389031998le_alt]:(((rev_Ar2020079950le_alt @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt))=(cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt))), inference(er,[status(thm)],[c_0_38])).
% 110.83/16.66 thf(c_0_51, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((rev_Ar2020079950le_alt @ (cons_A1142416030le_alt @ X2 @ X11))=(esk155_0 @ X2 @ (rev_Ar2020079950le_alt @ X11)))), inference(rw,[status(thm)],[c_0_39, c_0_40])).
% 110.83/16.66 thf(c_0_52, plain, ((rev_Ar2020079950le_alt @ nil_Ar52383470le_alt)=(nil_Ar52383470le_alt)), inference(split_conjunct,[status(thm)],[fact_605_rev_Osimps_I1_J])).
% 110.83/16.66 thf(c_0_53, plain, ![X4849:list_A1402527603le_alt]:(((set_Ar1491127311le_alt @ (rotate1249022267le_alt @ X4849))=(set_Ar1491127311le_alt @ X4849))), inference(variable_rename,[status(thm)],[fact_697_set__rotate1])).
% 110.83/16.66 thf(c_0_54, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((rotate1249022267le_alt @ (cons_A1142416030le_alt @ X2 @ X11))=(append1092755459le_alt @ X11 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 110.83/16.66 thf(c_0_55, plain, ![X4786:list_A1402527603le_alt, X4787:arrow_1389031998le_alt]:(((butlas1188620858le_alt @ (append1092755459le_alt @ X4786 @ (cons_A1142416030le_alt @ X4787 @ nil_Ar52383470le_alt)))=(X4786))), inference(variable_rename,[status(thm)],[fact_422_butlast__snoc])).
% 110.83/16.66 thf(c_0_56, plain, ![X2:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X4:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o]:((((X2)=(X4))|(member285112084le_alt @ (produc897867031le_alt @ X5 @ X4) @ X6)|~((member285112084le_alt @ (produc897867031le_alt @ X5 @ X2) @ (arrow_1865170000_below @ X6 @ X2 @ X4)))|~((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)))), inference(er,[status(thm)],[c_0_42])).
% 110.83/16.66 thf(c_0_57, plain, ![X1:arrow_1196572341e_indi]:((member1241905979_alt_o @ (p @ X1) @ arrow_1982173296le_Lin)), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 110.83/16.66 thf(c_0_58, plain, ![X71:produc1572197287le_alt, X6:produc1572197287le_alt > $o]:(((X6 @ X71)|~((member285112084le_alt @ X71 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 110.83/16.66 thf(c_0_59, negated_conjecture, ((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0))|(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (epred18_0 @ esk1_0))), inference(rw,[status(thm)],[c_0_46, c_0_47])).
% 110.83/16.66 thf(c_0_60, plain, ![X4788:list_A1402527603le_alt, X4789:arrow_1389031998le_alt, X4790:list_A1402527603le_alt]:(((((((X4790)!=(nil_Ar52383470le_alt))|((append1092755459le_alt @ X4788 @ (cons_A1142416030le_alt @ X4789 @ nil_Ar52383470le_alt))!=(X4790)))&(((butlas1188620858le_alt @ X4790)=(X4788))|((append1092755459le_alt @ X4788 @ (cons_A1142416030le_alt @ X4789 @ nil_Ar52383470le_alt))!=(X4790))))&(((last_A2130988295le_alt @ X4790)=(X4789))|((append1092755459le_alt @ X4788 @ (cons_A1142416030le_alt @ X4789 @ nil_Ar52383470le_alt))!=(X4790))))&(((X4790)=(nil_Ar52383470le_alt))|((butlas1188620858le_alt @ X4790)!=(X4788))|((last_A2130988295le_alt @ X4790)!=(X4789))|((append1092755459le_alt @ X4788 @ (cons_A1142416030le_alt @ X4789 @ nil_Ar52383470le_alt))=(X4790))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_48])])])])).
% 110.83/16.66 thf(c_0_61, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:((~((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ X11)))|~((distin1149997281le_alt @ (cons_A1142416030le_alt @ X2 @ X11))))), inference(split_conjunct,[status(thm)],[c_0_49])).
% 110.83/16.66 thf(c_0_62, plain, (distin1149997281le_alt @ (cons_A1142416030le_alt @ a @ (cons_A1142416030le_alt @ b @ (cons_A1142416030le_alt @ c @ nil_Ar52383470le_alt)))), inference(split_conjunct,[status(thm)],[fact_4_dist])).
% 110.83/16.66 thf(c_0_63, plain, ![X2:arrow_1389031998le_alt]:(((cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)=(esk155_0 @ X2 @ nil_Ar52383470le_alt))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51]), c_0_52])).
% 110.83/16.66 thf(c_0_64, plain, ![X11:list_A1402527603le_alt]:(((set_Ar1491127311le_alt @ (rotate1249022267le_alt @ X11))=(set_Ar1491127311le_alt @ X11))), inference(split_conjunct,[status(thm)],[c_0_53])).
% 110.83/16.66 thf(c_0_65, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((rotate1249022267le_alt @ (cons_A1142416030le_alt @ X2 @ X11))=(esk155_0 @ X2 @ X11))), inference(rw,[status(thm)],[c_0_54, c_0_40])).
% 110.83/16.66 thf(c_0_66, plain, ![X4795:arrow_1389031998le_alt, X4796:list_A1402527603le_alt]:((~(member998036369le_alt @ X4795 @ (set_Ar1491127311le_alt @ (butlas1188620858le_alt @ X4796)))|(member998036369le_alt @ X4795 @ (set_Ar1491127311le_alt @ X4796)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_689_in__set__butlastD])])])).
% 110.83/16.66 thf(c_0_67, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((butlas1188620858le_alt @ (append1092755459le_alt @ X11 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))=(X11))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 110.83/16.66 thf(c_0_68, plain, ![X2:arrow_1389031998le_alt, X4:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X7:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o]:((((X5)=(X2))|(member285112084le_alt @ (produc897867031le_alt @ X5 @ X2) @ (arrow_1865170000_below @ X6 @ X4 @ X7))|((X4)=(X7))|((X2)!=(X4))|~((member285112084le_alt @ (produc897867031le_alt @ X5 @ X7) @ X6))|~((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 110.83/16.66 thf(c_0_69, negated_conjecture, (~((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0)))|~((member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (arrow_1865170000_below @ (p @ esk1_0) @ c @ b)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 110.83/16.66 thf(c_0_70, plain, ![X2:arrow_1389031998le_alt, X1:arrow_1196572341e_indi]:((((b)=(c))|(member285112084le_alt @ (produc897867031le_alt @ X2 @ b) @ (p @ X1))|~((member285112084le_alt @ (produc897867031le_alt @ X2 @ c) @ (epred18_0 @ X1))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_47]), c_0_57])])).
% 110.83/16.66 thf(c_0_71, negated_conjecture, ((member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (epred18_0 @ esk1_0))|(p @ esk1_0 @ (produc897867031le_alt @ a @ b))), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 110.83/16.66 thf(c_0_72, plain, ![X6:produc1572197287le_alt > $o, X71:produc1572197287le_alt]:(((member285112084le_alt @ X71 @ X6)|~((X6 @ X71)))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 110.83/16.66 thf(c_0_73, plain, ![X2203:list_A1402527603le_alt]:((((X2203)!=(nil_Ar52383470le_alt))=>(member998036369le_alt @ (last_A2130988295le_alt @ X2203) @ (set_Ar1491127311le_alt @ X2203)))), inference(fof_simplification,[status(thm)],[fact_725_last__in__set])).
% 110.83/16.66 thf(c_0_74, plain, ![X4838:list_A1402527603le_alt, X4839:arrow_1389031998le_alt]:(((last_A2130988295le_alt @ (append1092755459le_alt @ X4838 @ (cons_A1142416030le_alt @ X4839 @ nil_Ar52383470le_alt)))=(X4839))), inference(variable_rename,[status(thm)],[fact_423_last__snoc])).
% 110.83/16.66 thf(c_0_75, plain, ![X2:arrow_1389031998le_alt, X12:list_A1402527603le_alt, X11:list_A1402527603le_alt]:((((X11)!=(nil_Ar52383470le_alt))|((append1092755459le_alt @ X12 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt))!=(X11)))), inference(split_conjunct,[status(thm)],[c_0_60])).
% 110.83/16.66 thf(c_0_76, plain, ~((member998036369le_alt @ a @ (set_Ar1491127311le_alt @ (cons_A1142416030le_alt @ b @ (esk155_0 @ c @ nil_Ar52383470le_alt))))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63])).
% 110.83/16.66 thf(c_0_77, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((set_Ar1491127311le_alt @ (cons_A1142416030le_alt @ X2 @ X11))=(set_Ar1491127311le_alt @ (esk155_0 @ X2 @ X11)))), inference(spm,[status(thm)],[c_0_64, c_0_65])).
% 110.83/16.66 thf(c_0_78, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ X11))|~((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ (butlas1188620858le_alt @ X11)))))), inference(split_conjunct,[status(thm)],[c_0_66])).
% 110.83/16.66 thf(c_0_79, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((butlas1188620858le_alt @ (esk155_0 @ X2 @ X11))=(X11))), inference(rw,[status(thm)],[c_0_67, c_0_40])).
% 110.83/16.66 thf(c_0_80, plain, ![X2:arrow_1389031998le_alt, X4:arrow_1389031998le_alt, X5:arrow_1389031998le_alt, X6:produc1572197287le_alt > $o]:((((X2)=(X4))|((X2)=(X5))|(member285112084le_alt @ (produc897867031le_alt @ X5 @ X2) @ (arrow_1865170000_below @ X6 @ X2 @ X4))|~((member285112084le_alt @ (produc897867031le_alt @ X5 @ X4) @ X6))|~((member1241905979_alt_o @ X6 @ arrow_1982173296le_Lin)))), inference(er,[status(thm)],[c_0_68])).
% 110.83/16.66 thf(c_0_81, negated_conjecture, (~((member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (epred18_0 @ esk1_0)))|~((member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0)))), inference(rw,[status(thm)],[c_0_69, c_0_47])).
% 110.83/16.66 thf(c_0_82, negated_conjecture, (((b)=(c))|(member285112084le_alt @ (produc897867031le_alt @ a @ b) @ (p @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_72])).
% 110.83/16.66 thf(c_0_83, plain, ![X4842:list_A1402527603le_alt]:((((X4842)=(nil_Ar52383470le_alt))|(member998036369le_alt @ (last_A2130988295le_alt @ X4842) @ (set_Ar1491127311le_alt @ X4842)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_73])])).
% 110.83/16.66 thf(c_0_84, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((last_A2130988295le_alt @ (append1092755459le_alt @ X11 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt)))=(X2))), inference(split_conjunct,[status(thm)],[c_0_74])).
% 110.83/16.66 thf(c_0_85, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((append1092755459le_alt @ X11 @ (cons_A1142416030le_alt @ X2 @ nil_Ar52383470le_alt))!=(nil_Ar52383470le_alt))), inference(er,[status(thm)],[c_0_75])).
% 110.83/16.66 thf(c_0_86, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((distin1149997281le_alt @ X11)|~((distin1149997281le_alt @ (cons_A1142416030le_alt @ X2 @ X11))))), inference(split_conjunct,[status(thm)],[c_0_49])).
% 110.83/16.66 thf(c_0_87, plain, ~((member998036369le_alt @ a @ (set_Ar1491127311le_alt @ (esk155_0 @ b @ (esk155_0 @ c @ nil_Ar52383470le_alt))))), inference(rw,[status(thm)],[c_0_76, c_0_77])).
% 110.83/16.66 thf(c_0_88, plain, ![X2:arrow_1389031998le_alt, X4:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ (esk155_0 @ X4 @ X11)))|~((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ X11))))), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 110.83/16.66 thf(c_0_89, negated_conjecture, ![X2:arrow_1389031998le_alt]:((((X2)=(b))|((X2)=(a))|(member285112084le_alt @ (produc897867031le_alt @ a @ X2) @ (arrow_1865170000_below @ (p @ esk1_0) @ X2 @ b))|(member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (epred18_0 @ esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_59]), c_0_57])])).
% 110.83/16.66 thf(c_0_90, negated_conjecture, (((b)=(c))|~((member285112084le_alt @ (produc897867031le_alt @ a @ c) @ (epred18_0 @ esk1_0)))), inference(spm,[status(thm)],[c_0_81, c_0_82])).
% 110.83/16.66 thf(c_0_91, plain, ![X11:list_A1402527603le_alt]:((((X11)=(nil_Ar52383470le_alt))|(member998036369le_alt @ (last_A2130988295le_alt @ X11) @ (set_Ar1491127311le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_83])).
% 110.83/16.66 thf(c_0_92, plain, ![X11:list_A1402527603le_alt, X2:arrow_1389031998le_alt]:(((last_A2130988295le_alt @ (esk155_0 @ X2 @ X11))=(X2))), inference(rw,[status(thm)],[c_0_84, c_0_40])).
% 110.83/16.66 thf(c_0_93, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:(((esk155_0 @ X2 @ X11)!=(nil_Ar52383470le_alt))), inference(rw,[status(thm)],[c_0_85, c_0_40])).
% 110.83/16.66 thf(c_0_94, plain, (distin1149997281le_alt @ (cons_A1142416030le_alt @ b @ (esk155_0 @ c @ nil_Ar52383470le_alt))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_62]), c_0_63])).
% 110.83/16.66 thf(c_0_95, plain, ~((member998036369le_alt @ a @ (set_Ar1491127311le_alt @ (esk155_0 @ c @ nil_Ar52383470le_alt)))), inference(spm,[status(thm)],[c_0_87, c_0_88])).
% 110.83/16.66 thf(c_0_96, plain, (((a)=(c))|((b)=(c))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_47]), c_0_90])).
% 110.83/16.66 thf(c_0_97, plain, ![X2:arrow_1389031998le_alt, X11:list_A1402527603le_alt]:((member998036369le_alt @ X2 @ (set_Ar1491127311le_alt @ (esk155_0 @ X2 @ X11)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_92]), c_0_93])).
% 110.83/16.66 thf(c_0_98, plain, ~((member998036369le_alt @ b @ (set_Ar1491127311le_alt @ (esk155_0 @ c @ nil_Ar52383470le_alt)))), inference(spm,[status(thm)],[c_0_61, c_0_94])).
% 110.83/16.66 thf(c_0_99, plain, ((b)=(c)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_96]), c_0_97])])).
% 110.83/16.66 thf(c_0_100, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99]), c_0_97])]), ['proof']).
% 110.83/16.66 % SZS output end CNFRefutation
% 110.83/16.66 % Parsed axioms : 1619
% 110.83/16.66 % Removed by relevancy pruning/SinE : 1247
% 110.83/16.66 % Initial clauses : 718
% 110.83/16.66 % Removed in clause preprocessing : 25
% 110.83/16.66 % Initial clauses in saturation : 693
% 110.83/16.66 % Processed clauses : 37106
% 110.83/16.66 % ...of these trivial : 183
% 110.83/16.66 % ...subsumed : 25907
% 110.83/16.66 % ...remaining for further processing : 11016
% 110.83/16.66 % Other redundant clauses eliminated : 12986
% 110.83/16.66 % Clauses deleted for lack of memory : 0
% 110.83/16.66 % Backward-subsumed : 476
% 110.83/16.66 % Backward-rewritten : 1700
% 110.83/16.66 % Generated clauses : 273772
% 110.83/16.66 % ...of the previous two non-redundant : 248312
% 110.83/16.66 % ...aggressively subsumed : 0
% 110.83/16.66 % Contextual simplify-reflections : 83
% 110.83/16.66 % Paramodulations : 251699
% 110.83/16.66 % Factorizations : 17
% 110.83/16.66 % NegExts : 2669
% 110.83/16.66 % Equation resolutions : 13015
% 110.83/16.66 % Disequality decompositions : 0
% 110.83/16.66 % Total rewrite steps : 70436
% 110.83/16.66 % ...of those cached : 64283
% 110.83/16.66 % Propositional unsat checks : 2
% 110.83/16.66 % Propositional check models : 0
% 110.83/16.66 % Propositional check unsatisfiable : 0
% 110.83/16.66 % Propositional clauses : 0
% 110.83/16.66 % Propositional clauses after purity: 0
% 110.83/16.66 % Propositional unsat core size : 0
% 110.83/16.66 % Propositional preprocessing time : 0.000
% 110.83/16.66 % Propositional encoding time : 0.546
% 110.83/16.66 % Propositional solver time : 0.258
% 110.83/16.66 % Success case prop preproc time : 0.000
% 110.83/16.66 % Success case prop encoding time : 0.000
% 110.83/16.66 % Success case prop solver time : 0.000
% 110.83/16.66 % Current number of processed clauses : 7806
% 110.83/16.66 % Positive orientable unit clauses : 463
% 110.83/16.66 % Positive unorientable unit clauses: 11
% 110.83/16.66 % Negative unit clauses : 492
% 110.83/16.66 % Non-unit-clauses : 6840
% 110.83/16.66 % Current number of unprocessed clauses: 210287
% 110.83/16.66 % ...number of literals in the above : 647896
% 110.83/16.66 % Current number of archived formulas : 0
% 110.83/16.66 % Current number of archived clauses : 3120
% 110.83/16.66 % Clause-clause subsumption calls (NU) : 15577150
% 110.83/16.66 % Rec. Clause-clause subsumption calls : 7938242
% 110.83/16.66 % Non-unit clause-clause subsumptions : 18591
% 110.83/16.66 % Unit Clause-clause subsumption calls : 333684
% 110.83/16.66 % Rewrite failures with RHS unbound : 2284
% 110.83/16.66 % BW rewrite match attempts : 14883
% 110.83/16.66 % BW rewrite match successes : 180
% 110.83/16.66 % Condensation attempts : 0
% 110.83/16.66 % Condensation successes : 0
% 110.83/16.66 % Termbank termtop insertions : 12576965
% 110.83/16.66 % Search garbage collected termcells : 25921
% 110.83/16.66
% 110.83/16.66 % -------------------------------------------------
% 110.83/16.66 % User time : 15.493 s
% 110.83/16.66 % System time : 0.282 s
% 110.83/16.66 % Total time : 15.775 s
% 110.83/16.66 % Maximum resident set size: 10384 pages
% 110.83/16.66
% 110.83/16.66 % -------------------------------------------------
% 110.83/16.66 % User time : 77.528 s
% 110.83/16.66 % System time : 1.567 s
% 110.83/16.66 % Total time : 79.095 s
% 110.83/16.66 % Maximum resident set size: 8448 pages
% 110.83/16.66 % E exiting
%------------------------------------------------------------------------------