%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT170^2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 29.06s 5.37s
% Output : CNFRefutation 29.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT170^2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n002.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Tue Sep 29 13:36:50 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.25 Running higher-order theorem proving
% 0.30/0.39 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p
% 29.06/5.37 % Version: 3.5.1-ho
% 29.06/5.37 % Preprocessing class: HMLMSMSMSSLNHSA.
% 29.06/5.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 29.06/5.37 % Starting sh2lt with 1500s (5) cores
% 29.06/5.37 % Starting new_ho_6 with 300s (1) cores
% 29.06/5.37 % Starting almost_fo_2 with 300s (1) cores
% 29.06/5.37 % Starting sh5l with 300s (1) cores
% 29.06/5.37 % sh2lt with pid 1281422 completed with status 0
% 29.06/5.37 % Result found by sh2lt
% 29.06/5.37 % Preprocessing class: HMLMSMSMSSLNHSA.
% 29.06/5.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 29.06/5.37 % Starting sh2lt with 1500s (5) cores
% 29.06/5.37 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 29.06/5.37 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 29.06/5.37 % Search class: HGHSM-FSLM32-DHSFFSBN
% 29.06/5.37 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 29.06/5.37 % Starting SubtermCWHack with 136s (1) cores
% 29.06/5.37 % Starting sh2lt with 151s (1) cores
% 29.06/5.37 % Starting sh4l with 214s (1) cores
% 29.06/5.37 % Starting pre_casc_4 with 204s (1) cores
% 29.06/5.37 % Starting lpo5_fix with 136s (1) cores
% 29.06/5.37 % sh2lt with pid 1281440 completed with status 0
% 29.06/5.37 % Result found by sh2lt
% 29.06/5.37 % Preprocessing class: HMLMSMSMSSLNHSA.
% 29.06/5.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 29.06/5.37 % Starting sh2lt with 1500s (5) cores
% 29.06/5.37 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 29.06/5.37 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 29.06/5.37 % Search class: HGHSM-FSLM32-DHSFFSBN
% 29.06/5.37 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 29.06/5.37 % Starting SubtermCWHack with 136s (1) cores
% 29.06/5.37 % Starting sh2lt with 151s (1) cores
% 29.06/5.37 % Preprocessing time : 0.012 s
% 29.06/5.37 % Presaturation interreduction done
% 29.06/5.37
% 29.06/5.37 % Proof found!
% 29.06/5.37 % SZS status Theorem
% 29.06/5.37 % SZS output start CNFRefutation
% 29.06/5.37 thf(decl_sort1, type, produc1501160679le_alt: $tType).
% 29.06/5.37 thf(decl_sort2, type, arrow_1429601828e_indi: $tType).
% 29.06/5.37 thf(decl_sort3, type, arrow_475358991le_alt: $tType).
% 29.06/5.37 thf(decl_sort4, type, list_A2115238852le_alt: $tType).
% 29.06/5.37 thf(decl_26, type, arrow_823908191le_Lin: (produc1501160679le_alt > $o) > $o).
% 29.06/5.37 thf(decl_27, type, arrow_734252939e_Prof: (arrow_1429601828e_indi > produc1501160679le_alt > $o) > $o).
% 29.06/5.38 thf(decl_29, type, arrow_2098199487_below: (produc1501160679le_alt > $o) > arrow_475358991le_alt > arrow_475358991le_alt > produc1501160679le_alt > $o).
% 29.06/5.38 thf(decl_61, type, pi_Arr1929480907_alt_o: (arrow_1429601828e_indi > $o) > (arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o) > (arrow_1429601828e_indi > produc1501160679le_alt > $o) > $o).
% 29.06/5.38 thf(decl_77, type, append179082452le_alt: list_A2115238852le_alt > list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_86, type, butlas274947851le_alt: list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_94, type, distin236324274le_alt: list_A2115238852le_alt > $o).
% 29.06/5.38 thf(decl_119, type, hd_Arr1965683346le_alt: list_A2115238852le_alt > arrow_475358991le_alt).
% 29.06/5.38 thf(decl_127, type, insert2120566741le_alt: arrow_475358991le_alt > list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_135, type, last_A1217315288le_alt: list_A2115238852le_alt > arrow_475358991le_alt).
% 29.06/5.38 thf(decl_155, type, cons_A228743023le_alt: arrow_475358991le_alt > list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_164, type, nil_Ar1286194111le_alt: list_A2115238852le_alt).
% 29.06/5.38 thf(decl_183, type, rev_Ar1106406943le_alt: list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_187, type, rotate335349260le_alt: list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_192, type, set_Ar577454304le_alt: list_A2115238852le_alt > arrow_475358991le_alt > $o).
% 29.06/5.38 thf(decl_210, type, tl_Arr465451158le_alt: list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(decl_226, type, top_to988227749indi_o: arrow_1429601828e_indi > $o).
% 29.06/5.38 thf(decl_234, type, produc1347929815le_alt: arrow_475358991le_alt > arrow_475358991le_alt > produc1501160679le_alt).
% 29.06/5.38 thf(decl_256, type, collec22405327e_indi: (arrow_1429601828e_indi > $o) > arrow_1429601828e_indi > $o).
% 29.06/5.38 thf(decl_282, type, member526088951_alt_o: (arrow_1429601828e_indi > produc1501160679le_alt > $o) > ((arrow_1429601828e_indi > produc1501160679le_alt > $o) > $o) > $o).
% 29.06/5.38 thf(decl_284, type, member377231867_alt_o: (produc1501160679le_alt > $o) > ((produc1501160679le_alt > $o) > $o) > $o).
% 29.06/5.38 thf(decl_293, type, member84363362le_alt: arrow_475358991le_alt > (arrow_475358991le_alt > $o) > $o).
% 29.06/5.38 thf(decl_294, type, member2052026769e_indi: arrow_1429601828e_indi > (arrow_1429601828e_indi > $o) > $o).
% 29.06/5.38 thf(decl_300, type, member214075476le_alt: produc1501160679le_alt > (produc1501160679le_alt > $o) > $o).
% 29.06/5.38 thf(decl_315, type, p: arrow_1429601828e_indi > produc1501160679le_alt > $o).
% 29.06/5.38 thf(decl_316, type, a: arrow_475358991le_alt).
% 29.06/5.38 thf(decl_317, type, b: arrow_475358991le_alt).
% 29.06/5.38 thf(decl_318, type, c: arrow_475358991le_alt).
% 29.06/5.38 thf(decl_319, type, esk1_0: arrow_1429601828e_indi).
% 29.06/5.38 thf(decl_423, type, epred20_0: arrow_1429601828e_indi > produc1501160679le_alt > $o).
% 29.06/5.38 thf(decl_426, type, epred23_0: arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o).
% 29.06/5.38 thf(decl_427, type, epred24_1: list_A2115238852le_alt > arrow_475358991le_alt > $o).
% 29.06/5.38 thf(decl_431, type, epred28_0: arrow_1429601828e_indi > $o).
% 29.06/5.38 thf(decl_432, type, esk86_0: arrow_475358991le_alt > list_A2115238852le_alt > list_A2115238852le_alt).
% 29.06/5.38 thf(fact_492_rev__singleton__conv, axiom, ![X1476:list_A2115238852le_alt, X1477:arrow_475358991le_alt]:((((rev_Ar1106406943le_alt @ X1476)=(cons_A228743023le_alt @ X1477 @ nil_Ar1286194111le_alt))<=>((X1476)=(cons_A228743023le_alt @ X1477 @ nil_Ar1286194111le_alt)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_492_rev__singleton__conv)).
% 29.06/5.38 thf(fact_495_rev_Osimps_I2_J, axiom, ![X1483:arrow_475358991le_alt, X1484:list_A2115238852le_alt]:(((rev_Ar1106406943le_alt @ (cons_A228743023le_alt @ X1483 @ X1484))=(append179082452le_alt @ (rev_Ar1106406943le_alt @ X1484) @ (cons_A228743023le_alt @ X1483 @ nil_Ar1286194111le_alt)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_495_rev_Osimps_I2_J)).
% 29.06/5.38 thf(fact_344_UNIV__def, axiom, ((top_to988227749indi_o)=(collec22405327e_indi @ (^[X1062:arrow_1429601828e_indi]:(($true))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_344_UNIV__def)).
% 29.06/5.38 thf(fact_273_Collect__def, axiom, ![X941:arrow_1429601828e_indi > $o]:(((collec22405327e_indi @ X941)=(X941))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_273_Collect__def)).
% 29.06/5.38 thf(fact_464_rotate1__hd__tl, axiom, ![X1422:list_A2115238852le_alt]:((((X1422)!=(nil_Ar1286194111le_alt))=>((rotate335349260le_alt @ X1422)=(append179082452le_alt @ (tl_Arr465451158le_alt @ X1422) @ (cons_A228743023le_alt @ (hd_Arr1965683346le_alt @ X1422) @ nil_Ar1286194111le_alt))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_464_rotate1__hd__tl)).
% 29.06/5.38 thf(fact_489_rev_Osimps_I1_J, axiom, ((rev_Ar1106406943le_alt @ nil_Ar1286194111le_alt)=(nil_Ar1286194111le_alt)), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_489_rev_Osimps_I1_J)).
% 29.06/5.38 thf(fact_78_PiE, axiom, ![X193:arrow_1429601828e_indi, X194:arrow_1429601828e_indi > produc1501160679le_alt > $o, X195:arrow_1429601828e_indi > $o, X196:arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o]:(((member526088951_alt_o @ X194 @ (pi_Arr1929480907_alt_o @ X195 @ X196))=>(~((member377231867_alt_o @ (X194 @ X193) @ (X196 @ X193)))=>~((member2052026769e_indi @ X193 @ X195))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_78_PiE)).
% 29.06/5.38 thf(fact_289_Prof__def, axiom, ((arrow_734252939e_Prof)=(pi_Arr1929480907_alt_o @ top_to988227749indi_o @ (^[X977:arrow_1429601828e_indi]:(arrow_823908191le_Lin)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_289_Prof__def)).
% 29.06/5.38 thf(fact_316_UNIV__I, axiom, ![X1032:arrow_1429601828e_indi]:((member2052026769e_indi @ X1032 @ top_to988227749indi_o)), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_316_UNIV__I)).
% 29.06/5.38 thf(fact_37_list_Osimps_I2_J, axiom, ![X53:arrow_475358991le_alt, X54:list_A2115238852le_alt]:(((nil_Ar1286194111le_alt)!=(cons_A228743023le_alt @ X53 @ X54))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_37_list_Osimps_I2_J)).
% 29.06/5.38 thf(fact_12_in__below, axiom, ![X4:arrow_475358991le_alt, X5:arrow_475358991le_alt, X6:produc1501160679le_alt > $o, X8:arrow_475358991le_alt, X9:arrow_475358991le_alt]:((((X8)!=(X9))=>((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)=>((member214075476le_alt @ (produc1347929815le_alt @ X4 @ X5) @ (arrow_2098199487_below @ X6 @ X8 @ X9))<=>((((X4)!=(X5))&(((X5)=(X8))=>(member214075476le_alt @ (produc1347929815le_alt @ X4 @ X9) @ X6)))&(((X5)!=(X8))=>((((X4)=(X8))=>(((X5)=(X9))|(member214075476le_alt @ (produc1347929815le_alt @ X9 @ X5) @ X6)))&(((X4)!=(X8))=>(member214075476le_alt @ (produc1347929815le_alt @ X4 @ X5) @ X6))))))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_12_in__below)).
% 29.06/5.38 thf(conj_0, conjecture, ![X1:arrow_1429601828e_indi]:(((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ X1))<=>(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_below @ (p @ X1) @ c @ b)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', conj_0)).
% 29.06/5.38 thf(fact_452_tl_Osimps_I2_J, axiom, ![X1384:arrow_475358991le_alt, X1385:list_A2115238852le_alt]:(((tl_Arr465451158le_alt @ (cons_A228743023le_alt @ X1384 @ X1385))=(X1385))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_452_tl_Osimps_I2_J)).
% 29.06/5.38 thf(fact_467_hd_Osimps, axiom, ![X1434:arrow_475358991le_alt, X1435:list_A2115238852le_alt]:(((hd_Arr1965683346le_alt @ (cons_A228743023le_alt @ X1434 @ X1435))=(X1434))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_467_hd_Osimps)).
% 29.06/5.38 thf(fact_365_snoc__eq__iff__butlast, axiom, ![X1088:list_A2115238852le_alt, X1089:arrow_475358991le_alt, X1090:list_A2115238852le_alt]:((((append179082452le_alt @ X1088 @ (cons_A228743023le_alt @ X1089 @ nil_Ar1286194111le_alt))=(X1090))<=>((((X1090)!=(nil_Ar1286194111le_alt))&((butlas274947851le_alt @ X1090)=(X1088)))&((last_A1217315288le_alt @ X1090)=(X1089))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_365_snoc__eq__iff__butlast)).
% 29.06/5.38 thf(fact_556_distinct_Osimps_I2_J, axiom, ![X1654:arrow_475358991le_alt, X1655:list_A2115238852le_alt]:(((distin236324274le_alt @ (cons_A228743023le_alt @ X1654 @ X1655))<=>(~((member84363362le_alt @ X1654 @ (set_Ar577454304le_alt @ X1655)))&(distin236324274le_alt @ X1655)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_556_distinct_Osimps_I2_J)).
% 29.06/5.38 thf(fact_406_distinct1__rotate, axiom, ![X1214:list_A2115238852le_alt]:(((distin236324274le_alt @ (rotate335349260le_alt @ X1214))<=>(distin236324274le_alt @ X1214))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_406_distinct1__rotate)).
% 29.06/5.38 thf(fact_294_last__ConsR, axiom, ![X991:arrow_475358991le_alt, X992:list_A2115238852le_alt]:((((X992)!=(nil_Ar1286194111le_alt))=>((last_A1217315288le_alt @ (cons_A228743023le_alt @ X991 @ X992))=(last_A1217315288le_alt @ X992)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_294_last__ConsR)).
% 29.06/5.38 thf(fact_0__096P_A_058_AProf_096, axiom, (member526088951_alt_o @ p @ arrow_734252939e_Prof), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_0__096P_A_058_AProf_096)).
% 29.06/5.38 thf(fact_268_mem__def, axiom, ![X932:produc1501160679le_alt, X933:produc1501160679le_alt > $o]:(((member214075476le_alt @ X932 @ X933)<=>(X933 @ X932))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_268_mem__def)).
% 29.06/5.38 thf(fact_491_distinct__rev, axiom, ![X1475:list_A2115238852le_alt]:(((distin236324274le_alt @ (rev_Ar1106406943le_alt @ X1475))<=>(distin236324274le_alt @ X1475))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_491_distinct__rev)).
% 29.06/5.38 thf(fact_589_hd__in__set, axiom, ![X1737:list_A2115238852le_alt]:((((X1737)!=(nil_Ar1286194111le_alt))=>(member84363362le_alt @ (hd_Arr1965683346le_alt @ X1737) @ (set_Ar577454304le_alt @ X1737)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_589_hd__in__set)).
% 29.06/5.38 thf(fact_479_hd__rev, axiom, ![X1456:list_A2115238852le_alt]:((((X1456)!=(nil_Ar1286194111le_alt))=>((hd_Arr1965683346le_alt @ (rev_Ar1106406943le_alt @ X1456))=(last_A1217315288le_alt @ X1456)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_479_hd__rev)).
% 29.06/5.38 thf(fact_394_last__snoc, axiom, ![X1169:list_A2115238852le_alt, X1170:arrow_475358991le_alt]:(((last_A1217315288le_alt @ (append179082452le_alt @ X1169 @ (cons_A228743023le_alt @ X1170 @ nil_Ar1286194111le_alt)))=(X1170))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_394_last__snoc)).
% 29.06/5.38 thf(fact_488_Nil__is__rev__conv, axiom, ![X1471:list_A2115238852le_alt]:((((nil_Ar1286194111le_alt)=(rev_Ar1106406943le_alt @ X1471))<=>((X1471)=(nil_Ar1286194111le_alt)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_488_Nil__is__rev__conv)).
% 29.06/5.38 thf(fact_572_last__in__set, axiom, ![X1702:list_A2115238852le_alt]:((((X1702)!=(nil_Ar1286194111le_alt))=>(member84363362le_alt @ (last_A1217315288le_alt @ X1702) @ (set_Ar577454304le_alt @ X1702)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_572_last__in__set)).
% 29.06/5.38 thf(fact_4_dist, axiom, (distin236324274le_alt @ (cons_A228743023le_alt @ a @ (cons_A228743023le_alt @ b @ (cons_A228743023le_alt @ c @ nil_Ar1286194111le_alt)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_4_dist)).
% 29.06/5.38 thf(fact_605_List_Oinsert__def, axiom, ![X1777:arrow_475358991le_alt, X1778:list_A2115238852le_alt]:((((member84363362le_alt @ X1777 @ (set_Ar577454304le_alt @ X1778))=>((insert2120566741le_alt @ X1777 @ X1778)=(X1778)))&(~((member84363362le_alt @ X1777 @ (set_Ar577454304le_alt @ X1778)))=>((insert2120566741le_alt @ X1777 @ X1778)=(cons_A228743023le_alt @ X1777 @ X1778))))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_605_List_Oinsert__def)).
% 29.06/5.38 thf(fact_548_in__set__insert, axiom, ![X1638:arrow_475358991le_alt, X1639:list_A2115238852le_alt]:(((member84363362le_alt @ X1638 @ (set_Ar577454304le_alt @ X1639))=>((insert2120566741le_alt @ X1638 @ X1639)=(X1639)))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_548_in__set__insert)).
% 29.06/5.38 thf(fact_43_not__Cons__self, axiom, ![X66:list_A2115238852le_alt, X67:arrow_475358991le_alt]:(((X66)!=(cons_A228743023le_alt @ X67 @ X66))), file('/export/starexec/sandbox2/tmp/tmp.pkkW2jC0oR/E---3.1_1281338.p', fact_43_not__Cons__self)).
% 29.06/5.38 thf(c_0_30, plain, ![X3117:list_A2115238852le_alt, X3118:arrow_475358991le_alt]:(((((rev_Ar1106406943le_alt @ X3117)!=(cons_A228743023le_alt @ X3118 @ nil_Ar1286194111le_alt))|((X3117)=(cons_A228743023le_alt @ X3118 @ nil_Ar1286194111le_alt)))&(((X3117)!=(cons_A228743023le_alt @ X3118 @ nil_Ar1286194111le_alt))|((rev_Ar1106406943le_alt @ X3117)=(cons_A228743023le_alt @ X3118 @ nil_Ar1286194111le_alt))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_492_rev__singleton__conv])])])).
% 29.06/5.38 thf(c_0_31, plain, ![X2939:arrow_475358991le_alt, X2940:list_A2115238852le_alt]:(((rev_Ar1106406943le_alt @ (cons_A228743023le_alt @ X2939 @ X2940))=(append179082452le_alt @ (rev_Ar1106406943le_alt @ X2940) @ (cons_A228743023le_alt @ X2939 @ nil_Ar1286194111le_alt)))), inference(variable_rename,[status(thm)],[fact_495_rev_Osimps_I2_J])).
% 29.06/5.38 thf(c_0_32, plain, ![X3276:list_A2115238852le_alt, X3277:arrow_475358991le_alt]:(((esk86_0 @ X3277 @ X3276)=(append179082452le_alt @ X3276 @ (cons_A228743023le_alt @ X3277 @ nil_Ar1286194111le_alt)))), inference(variable_rename,[status(thm)],[])).
% 29.06/5.38 thf(c_0_33, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:((((rev_Ar1106406943le_alt @ X11)=(cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt))|((X11)!=(cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 29.06/5.38 thf(c_0_34, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((rev_Ar1106406943le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(append179082452le_alt @ (rev_Ar1106406943le_alt @ X11) @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 29.06/5.38 thf(c_0_35, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((esk86_0 @ X2 @ X11)=(append179082452le_alt @ X11 @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 29.06/5.38 thf(c_0_36, plain, ((top_to988227749indi_o)=(collec22405327e_indi @ (^[Z0:arrow_1429601828e_indi]:($true)))), inference(fof_simplification,[status(thm)],[fact_344_UNIV__def])).
% 29.06/5.38 thf(c_0_37, plain, ![X3257:arrow_1429601828e_indi]:(((epred28_0 @ X3257)<=>($true))), introduced(definition)).
% 29.06/5.38 thf(c_0_38, plain, ![X3194:arrow_1429601828e_indi > $o]:(((collec22405327e_indi @ X3194)=(X3194))), inference(variable_rename,[status(thm)],[fact_273_Collect__def])).
% 29.06/5.38 thf(c_0_39, plain, ![X1422:list_A2115238852le_alt]:((((X1422)!=(nil_Ar1286194111le_alt))=>((rotate335349260le_alt @ X1422)=(append179082452le_alt @ (tl_Arr465451158le_alt @ X1422) @ (cons_A228743023le_alt @ (hd_Arr1965683346le_alt @ X1422) @ nil_Ar1286194111le_alt))))), inference(fof_simplification,[status(thm)],[fact_464_rotate1__hd__tl])).
% 29.06/5.38 thf(c_0_40, plain, ![X2:arrow_475358991le_alt]:(((rev_Ar1106406943le_alt @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt))=(cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt))), inference(er,[status(thm)],[c_0_33])).
% 29.06/5.38 thf(c_0_41, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((rev_Ar1106406943le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(esk86_0 @ X2 @ (rev_Ar1106406943le_alt @ X11)))), inference(rw,[status(thm)],[c_0_34, c_0_35])).
% 29.06/5.38 thf(c_0_42, plain, ((rev_Ar1106406943le_alt @ nil_Ar1286194111le_alt)=(nil_Ar1286194111le_alt)), inference(split_conjunct,[status(thm)],[fact_489_rev_Osimps_I1_J])).
% 29.06/5.38 thf(c_0_43, plain, ![X193:arrow_1429601828e_indi, X194:arrow_1429601828e_indi > produc1501160679le_alt > $o, X195:arrow_1429601828e_indi > $o, X196:arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o]:(((member526088951_alt_o @ X194 @ (pi_Arr1929480907_alt_o @ X195 @ X196))=>(~(member377231867_alt_o @ (X194 @ X193) @ (X196 @ X193))=>~(member2052026769e_indi @ X193 @ X195)))), inference(fof_simplification,[status(thm)],[fact_78_PiE])).
% 29.06/5.38 thf(c_0_44, plain, ((arrow_734252939e_Prof)=(pi_Arr1929480907_alt_o @ top_to988227749indi_o @ (^[Z0:arrow_1429601828e_indi]:(arrow_823908191le_Lin)))), inference(fof_simplification,[status(thm)],[fact_289_Prof__def])).
% 29.06/5.38 thf(c_0_45, plain, ![X3239:arrow_1429601828e_indi]:(((epred23_0 @ X3239)=(arrow_823908191le_Lin))), introduced(definition)).
% 29.06/5.38 thf(c_0_46, plain, ((top_to988227749indi_o)=(collec22405327e_indi @ epred28_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_36]), c_0_37])).
% 29.06/5.38 thf(c_0_47, plain, ![X81:arrow_1429601828e_indi > $o]:(((collec22405327e_indi @ X81)=(X81))), inference(split_conjunct,[status(thm)],[c_0_38])).
% 29.06/5.38 thf(c_0_48, plain, ![X3072:arrow_1429601828e_indi]:((member2052026769e_indi @ X3072 @ top_to988227749indi_o)), inference(variable_rename,[status(thm)],[fact_316_UNIV__I])).
% 29.06/5.38 thf(c_0_49, plain, ![X3101:list_A2115238852le_alt]:((((X3101)=(nil_Ar1286194111le_alt))|((rotate335349260le_alt @ X3101)=(append179082452le_alt @ (tl_Arr465451158le_alt @ X3101) @ (cons_A228743023le_alt @ (hd_Arr1965683346le_alt @ X3101) @ nil_Ar1286194111le_alt))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])).
% 29.06/5.38 thf(c_0_50, plain, ![X2:arrow_475358991le_alt]:(((cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt)=(esk86_0 @ X2 @ nil_Ar1286194111le_alt))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41]), c_0_42])).
% 29.06/5.38 thf(c_0_51, plain, ![X53:arrow_475358991le_alt, X54:list_A2115238852le_alt]:(((nil_Ar1286194111le_alt)!=(cons_A228743023le_alt @ X53 @ X54))), inference(fof_simplification,[status(thm)],[fact_37_list_Osimps_I2_J])).
% 29.06/5.38 thf(c_0_52, plain, ![X4:arrow_475358991le_alt, X5:arrow_475358991le_alt, X6:produc1501160679le_alt > $o, X8:arrow_475358991le_alt, X9:arrow_475358991le_alt]:((((X8)!=(X9))=>((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)=>((member214075476le_alt @ (produc1347929815le_alt @ X4 @ X5) @ (arrow_2098199487_below @ X6 @ X8 @ X9))<=>((((X4)!=(X5))&(((X5)=(X8))=>(member214075476le_alt @ (produc1347929815le_alt @ X4 @ X9) @ X6)))&(((X5)!=(X8))=>((((X4)=(X8))=>(((X5)=(X9))|(member214075476le_alt @ (produc1347929815le_alt @ X9 @ X5) @ X6)))&(((X4)!=(X8))=>(member214075476le_alt @ (produc1347929815le_alt @ X4 @ X5) @ X6))))))))), inference(fof_simplification,[status(thm)],[fact_12_in__below])).
% 29.06/5.38 thf(c_0_53, plain, ![X3041:arrow_1429601828e_indi, X3042:arrow_1429601828e_indi > produc1501160679le_alt > $o, X3043:arrow_1429601828e_indi > $o, X3044:arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o]:((~(member526088951_alt_o @ X3042 @ (pi_Arr1929480907_alt_o @ X3043 @ X3044))|((member377231867_alt_o @ (X3042 @ X3041) @ (X3044 @ X3041))|~(member2052026769e_indi @ X3041 @ X3043)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])])).
% 29.06/5.38 thf(c_0_54, plain, ((arrow_734252939e_Prof)=(pi_Arr1929480907_alt_o @ top_to988227749indi_o @ epred23_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_44]), c_0_45])).
% 29.06/5.38 thf(c_0_55, plain, ((top_to988227749indi_o)=(epred28_0)), inference(rw,[status(thm)],[c_0_46, c_0_47])).
% 29.06/5.38 thf(c_0_56, plain, ![X3287:arrow_1429601828e_indi]:(((epred23_0 @ X3287)=(arrow_823908191le_Lin))), inference(variable_rename,[status(thm)],[])).
% 29.06/5.38 thf(c_0_57, plain, ![X1:arrow_1429601828e_indi]:((member2052026769e_indi @ X1 @ top_to988227749indi_o)), inference(split_conjunct,[status(thm)],[c_0_48])).
% 29.06/5.38 thf(c_0_58, negated_conjecture, ~(![X1:arrow_1429601828e_indi]:(((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ X1))<=>(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_below @ (p @ X1) @ c @ b))))), inference(assume_negation,[status(cth)],[conj_0])).
% 29.06/5.38 thf(c_0_59, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|((rotate335349260le_alt @ X11)=(append179082452le_alt @ (tl_Arr465451158le_alt @ X11) @ (cons_A228743023le_alt @ (hd_Arr1965683346le_alt @ X11) @ nil_Ar1286194111le_alt))))), inference(split_conjunct,[status(thm)],[c_0_49])).
% 29.06/5.38 thf(c_0_60, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((append179082452le_alt @ X11 @ (esk86_0 @ X2 @ nil_Ar1286194111le_alt))=(esk86_0 @ X2 @ X11))), inference(rw,[status(thm)],[c_0_35, c_0_50])).
% 29.06/5.38 thf(c_0_61, plain, ![X3110:arrow_475358991le_alt, X3111:list_A2115238852le_alt]:(((tl_Arr465451158le_alt @ (cons_A228743023le_alt @ X3110 @ X3111))=(X3111))), inference(variable_rename,[status(thm)],[fact_452_tl_Osimps_I2_J])).
% 29.06/5.38 thf(c_0_62, plain, ![X3133:arrow_475358991le_alt, X3134:list_A2115238852le_alt]:(((hd_Arr1965683346le_alt @ (cons_A228743023le_alt @ X3133 @ X3134))=(X3133))), inference(variable_rename,[status(thm)],[fact_467_hd_Osimps])).
% 29.06/5.38 thf(c_0_63, plain, ![X2742:arrow_475358991le_alt, X2743:list_A2115238852le_alt]:(((nil_Ar1286194111le_alt)!=(cons_A228743023le_alt @ X2742 @ X2743))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_51])])).
% 29.06/5.38 thf(c_0_64, plain, ![X1088:list_A2115238852le_alt, X1089:arrow_475358991le_alt, X1090:list_A2115238852le_alt]:((((append179082452le_alt @ X1088 @ (cons_A228743023le_alt @ X1089 @ nil_Ar1286194111le_alt))=(X1090))<=>((((X1090)!=(nil_Ar1286194111le_alt))&((butlas274947851le_alt @ X1090)=(X1088)))&((last_A1217315288le_alt @ X1090)=(X1089))))), inference(fof_simplification,[status(thm)],[fact_365_snoc__eq__iff__butlast])).
% 29.06/5.38 thf(c_0_65, plain, ![X2588:arrow_475358991le_alt, X2589:arrow_475358991le_alt, X2590:produc1501160679le_alt > $o, X2591:arrow_475358991le_alt, X2592:arrow_475358991le_alt]:(((((((X2588)!=(X2589))|~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(((X2589)!=(X2591))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592))))&((((X2588)!=(X2591))|(((X2589)=(X2592))|(member214075476le_alt @ (produc1347929815le_alt @ X2592 @ X2589) @ X2590))|((X2589)=(X2591))|~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(((X2588)=(X2591))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|((X2589)=(X2591))|~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))))&(((((X2589)!=(X2591))|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(((((X2588)!=(X2591))|((X2588)=(X2591))|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|((X2588)=(X2591))|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592))))&(((((X2588)!=(X2591))|((X2589)!=(X2592))|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|((X2589)!=(X2592))|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592))))&((((X2588)!=(X2591))|~(member214075476le_alt @ (produc1347929815le_alt @ X2592 @ X2589) @ X2590)|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|~(member214075476le_alt @ (produc1347929815le_alt @ X2592 @ X2589) @ X2590)|(((X2589)=(X2591))|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))))))&((((X2589)!=(X2591))|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(((((X2588)!=(X2591))|((X2588)=(X2591))|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|((X2588)=(X2591))|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592))))&(((((X2588)!=(X2591))|((X2589)!=(X2592))|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|((X2589)!=(X2592))|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592))))&((((X2588)!=(X2591))|~(member214075476le_alt @ (produc1347929815le_alt @ X2592 @ X2589) @ X2590)|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))&(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ X2590)|~(member214075476le_alt @ (produc1347929815le_alt @ X2592 @ X2589) @ X2590)|(~(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2592) @ X2590)|((X2588)=(X2589)))|(member214075476le_alt @ (produc1347929815le_alt @ X2588 @ X2589) @ (arrow_2098199487_below @ X2590 @ X2591 @ X2592))|~(member377231867_alt_o @ X2590 @ arrow_823908191le_Lin)|((X2591)=(X2592)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_52])])])])).
% 29.06/5.38 thf(c_0_66, plain, ![X38:arrow_1429601828e_indi > produc1501160679le_alt > $o, X1:arrow_1429601828e_indi, X196:arrow_1429601828e_indi > (produc1501160679le_alt > $o) > $o, X81:arrow_1429601828e_indi > $o]:(((member377231867_alt_o @ (X38 @ X1) @ (X196 @ X1))|~((member526088951_alt_o @ X38 @ (pi_Arr1929480907_alt_o @ X81 @ X196)))|~((member2052026769e_indi @ X1 @ X81)))), inference(split_conjunct,[status(thm)],[c_0_53])).
% 29.06/5.38 thf(c_0_67, plain, ((pi_Arr1929480907_alt_o @ epred28_0 @ epred23_0)=(arrow_734252939e_Prof)), inference(rw,[status(thm)],[c_0_54, c_0_55])).
% 29.06/5.38 thf(c_0_68, plain, ![X1:arrow_1429601828e_indi]:(((epred23_0 @ X1)=(arrow_823908191le_Lin))), inference(split_conjunct,[status(thm)],[c_0_56])).
% 29.06/5.38 thf(c_0_69, plain, ![X1:arrow_1429601828e_indi]:((member2052026769e_indi @ X1 @ epred28_0)), inference(rw,[status(thm)],[c_0_57, c_0_55])).
% 29.06/5.38 thf(c_0_70, negated_conjecture, ((~(member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0))|~(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_below @ (p @ esk1_0) @ c @ b)))&((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0))|(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_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_58])])])])).
% 29.06/5.38 thf(c_0_71, plain, ![X3291:arrow_1429601828e_indi]:(((epred20_0 @ X3291)=(arrow_2098199487_below @ (p @ X3291) @ c @ b))), inference(variable_rename,[status(thm)],[])).
% 29.06/5.38 thf(c_0_72, plain, ![X1654:arrow_475358991le_alt, X1655:list_A2115238852le_alt]:(((distin236324274le_alt @ (cons_A228743023le_alt @ X1654 @ X1655))<=>(~(member84363362le_alt @ X1654 @ (set_Ar577454304le_alt @ X1655))&(distin236324274le_alt @ X1655)))), inference(fof_simplification,[status(thm)],[fact_556_distinct_Osimps_I2_J])).
% 29.06/5.38 thf(c_0_73, plain, ![X2724:list_A2115238852le_alt]:(((~(distin236324274le_alt @ (rotate335349260le_alt @ X2724))|(distin236324274le_alt @ X2724))&(~(distin236324274le_alt @ X2724)|(distin236324274le_alt @ (rotate335349260le_alt @ X2724))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_406_distinct1__rotate])])])).
% 29.06/5.38 thf(c_0_74, plain, ![X11:list_A2115238852le_alt]:((((esk86_0 @ (hd_Arr1965683346le_alt @ X11) @ (tl_Arr465451158le_alt @ X11))=(rotate335349260le_alt @ X11))|((X11)=(nil_Ar1286194111le_alt)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_50]), c_0_60])).
% 29.06/5.38 thf(c_0_75, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((tl_Arr465451158le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(X11))), inference(split_conjunct,[status(thm)],[c_0_61])).
% 29.06/5.38 thf(c_0_76, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((hd_Arr1965683346le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(X2))), inference(split_conjunct,[status(thm)],[c_0_62])).
% 29.06/5.38 thf(c_0_77, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((nil_Ar1286194111le_alt)!=(cons_A228743023le_alt @ X2 @ X11))), inference(split_conjunct,[status(thm)],[c_0_63])).
% 29.06/5.38 thf(c_0_78, plain, ![X3285:arrow_475358991le_alt, X3286:list_A2115238852le_alt]:(((~(epred24_1 @ X3286 @ X3285)|((X3285)!=(last_A1217315288le_alt @ X3286)))&(((X3285)=(last_A1217315288le_alt @ X3286))|(epred24_1 @ X3286 @ X3285)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[])])])])).
% 29.06/5.38 thf(c_0_79, plain, ![X991:arrow_475358991le_alt, X992:list_A2115238852le_alt]:((((X992)!=(nil_Ar1286194111le_alt))=>((last_A1217315288le_alt @ (cons_A228743023le_alt @ X991 @ X992))=(last_A1217315288le_alt @ X992)))), inference(fof_simplification,[status(thm)],[fact_294_last__ConsR])).
% 29.06/5.38 thf(c_0_80, plain, ![X2881:list_A2115238852le_alt, X2882:arrow_475358991le_alt, X2883:list_A2115238852le_alt]:(((((((X2883)!=(nil_Ar1286194111le_alt))|((append179082452le_alt @ X2881 @ (cons_A228743023le_alt @ X2882 @ nil_Ar1286194111le_alt))!=(X2883)))&(((butlas274947851le_alt @ X2883)=(X2881))|((append179082452le_alt @ X2881 @ (cons_A228743023le_alt @ X2882 @ nil_Ar1286194111le_alt))!=(X2883))))&(((last_A1217315288le_alt @ X2883)=(X2882))|((append179082452le_alt @ X2881 @ (cons_A228743023le_alt @ X2882 @ nil_Ar1286194111le_alt))!=(X2883))))&(((X2883)=(nil_Ar1286194111le_alt))|((butlas274947851le_alt @ X2883)!=(X2881))|((last_A1217315288le_alt @ X2883)!=(X2882))|((append179082452le_alt @ X2881 @ (cons_A228743023le_alt @ X2882 @ nil_Ar1286194111le_alt))=(X2883))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_64])])])])).
% 29.06/5.38 thf(c_0_81, plain, ![X2:arrow_475358991le_alt, X5:arrow_475358991le_alt, X4:arrow_475358991le_alt, X7:arrow_475358991le_alt, X6:produc1501160679le_alt > $o]:(((member214075476le_alt @ (produc1347929815le_alt @ X5 @ X7) @ X6)|((X4)=(X7))|((X2)!=(X4))|~((member214075476le_alt @ (produc1347929815le_alt @ X5 @ X2) @ (arrow_2098199487_below @ X6 @ X4 @ X7)))|~((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)))), inference(split_conjunct,[status(thm)],[c_0_65])).
% 29.06/5.38 thf(c_0_82, plain, ![X1:arrow_1429601828e_indi, X38:arrow_1429601828e_indi > produc1501160679le_alt > $o]:(((member377231867_alt_o @ (X38 @ X1) @ arrow_823908191le_Lin)|~((member526088951_alt_o @ X38 @ arrow_734252939e_Prof)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_68]), c_0_69])])).
% 29.06/5.38 thf(c_0_83, plain, (member526088951_alt_o @ p @ arrow_734252939e_Prof), inference(split_conjunct,[status(thm)],[fact_0__096P_A_058_AProf_096])).
% 29.06/5.38 thf(c_0_84, plain, ![X2586:produc1501160679le_alt, X2587:produc1501160679le_alt > $o]:(((~(member214075476le_alt @ X2586 @ X2587)|(X2587 @ X2586))&(~(X2587 @ X2586)|(member214075476le_alt @ X2586 @ X2587)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_268_mem__def])])])).
% 29.06/5.38 thf(c_0_85, negated_conjecture, ((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0))|(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_below @ (p @ esk1_0) @ c @ b))), inference(split_conjunct,[status(thm)],[c_0_70])).
% 29.06/5.38 thf(c_0_86, plain, ![X1:arrow_1429601828e_indi]:(((epred20_0 @ X1)=(arrow_2098199487_below @ (p @ X1) @ c @ b))), inference(split_conjunct,[status(thm)],[c_0_71])).
% 29.06/5.38 thf(c_0_87, plain, ![X2740:arrow_475358991le_alt, X2741:list_A2115238852le_alt]:((((~(member84363362le_alt @ X2740 @ (set_Ar577454304le_alt @ X2741))|~(distin236324274le_alt @ (cons_A228743023le_alt @ X2740 @ X2741)))&((distin236324274le_alt @ X2741)|~(distin236324274le_alt @ (cons_A228743023le_alt @ X2740 @ X2741))))&((member84363362le_alt @ X2740 @ (set_Ar577454304le_alt @ X2741))|~(distin236324274le_alt @ X2741)|(distin236324274le_alt @ (cons_A228743023le_alt @ X2740 @ X2741))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_72])])])])).
% 29.06/5.38 thf(c_0_88, plain, ![X11:list_A2115238852le_alt]:(((distin236324274le_alt @ X11)|~((distin236324274le_alt @ (rotate335349260le_alt @ X11))))), inference(split_conjunct,[status(thm)],[c_0_73])).
% 29.06/5.38 thf(c_0_89, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((rotate335349260le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(esk86_0 @ X2 @ X11))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_75]), c_0_76]), c_0_77])).
% 29.06/5.38 thf(c_0_90, plain, ![X2735:list_A2115238852le_alt]:(((~(distin236324274le_alt @ (rev_Ar1106406943le_alt @ X2735))|(distin236324274le_alt @ X2735))&(~(distin236324274le_alt @ X2735)|(distin236324274le_alt @ (rev_Ar1106406943le_alt @ X2735))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_491_distinct__rev])])])).
% 29.06/5.38 thf(c_0_91, plain, ![X1737:list_A2115238852le_alt]:((((X1737)!=(nil_Ar1286194111le_alt))=>(member84363362le_alt @ (hd_Arr1965683346le_alt @ X1737) @ (set_Ar577454304le_alt @ X1737)))), inference(fof_simplification,[status(thm)],[fact_589_hd__in__set])).
% 29.06/5.38 thf(c_0_92, plain, ![X1456:list_A2115238852le_alt]:((((X1456)!=(nil_Ar1286194111le_alt))=>((hd_Arr1965683346le_alt @ (rev_Ar1106406943le_alt @ X1456))=(last_A1217315288le_alt @ X1456)))), inference(fof_simplification,[status(thm)],[fact_479_hd__rev])).
% 29.06/5.38 thf(c_0_93, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((~((epred24_1 @ X11 @ X2))|((X2)!=(last_A1217315288le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_78])).
% 29.06/5.38 thf(c_0_94, plain, ![X3093:arrow_475358991le_alt, X3094:list_A2115238852le_alt]:((((X3094)=(nil_Ar1286194111le_alt))|((last_A1217315288le_alt @ (cons_A228743023le_alt @ X3093 @ X3094))=(last_A1217315288le_alt @ X3094)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_79])])).
% 29.06/5.38 thf(c_0_95, plain, ![X2924:list_A2115238852le_alt, X2925:arrow_475358991le_alt]:(((last_A1217315288le_alt @ (append179082452le_alt @ X2924 @ (cons_A228743023le_alt @ X2925 @ nil_Ar1286194111le_alt)))=(X2925))), inference(variable_rename,[status(thm)],[fact_394_last__snoc])).
% 29.06/5.38 thf(c_0_96, plain, ![X2:arrow_475358991le_alt, X12:list_A2115238852le_alt, X11:list_A2115238852le_alt]:((((X11)!=(nil_Ar1286194111le_alt))|((append179082452le_alt @ X12 @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt))!=(X11)))), inference(split_conjunct,[status(thm)],[c_0_80])).
% 29.06/5.38 thf(c_0_97, plain, ![X2:arrow_475358991le_alt, X5:arrow_475358991le_alt, X4:arrow_475358991le_alt, X6:produc1501160679le_alt > $o]:((((X2)=(X4))|(member214075476le_alt @ (produc1347929815le_alt @ X5 @ X4) @ X6)|~((member214075476le_alt @ (produc1347929815le_alt @ X5 @ X2) @ (arrow_2098199487_below @ X6 @ X2 @ X4)))|~((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)))), inference(er,[status(thm)],[c_0_81])).
% 29.06/5.38 thf(c_0_98, plain, ![X1:arrow_1429601828e_indi]:((member377231867_alt_o @ (p @ X1) @ arrow_823908191le_Lin)), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 29.06/5.38 thf(c_0_99, plain, ![X71:produc1501160679le_alt, X6:produc1501160679le_alt > $o]:(((X6 @ X71)|~((member214075476le_alt @ X71 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_84])).
% 29.06/5.38 thf(c_0_100, negated_conjecture, ((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0))|(member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (epred20_0 @ esk1_0))), inference(rw,[status(thm)],[c_0_85, c_0_86])).
% 29.06/5.38 thf(c_0_101, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((~((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ X11)))|~((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ X11))))), inference(split_conjunct,[status(thm)],[c_0_87])).
% 29.06/5.38 thf(c_0_102, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ X11))|~((distin236324274le_alt @ (esk86_0 @ X2 @ X11))))), inference(spm,[status(thm)],[c_0_88, c_0_89])).
% 29.06/5.38 thf(c_0_103, plain, ![X11:list_A2115238852le_alt]:(((distin236324274le_alt @ (rev_Ar1106406943le_alt @ X11))|~((distin236324274le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_90])).
% 29.06/5.38 thf(c_0_104, plain, ![X2999:list_A2115238852le_alt]:((((X2999)=(nil_Ar1286194111le_alt))|(member84363362le_alt @ (hd_Arr1965683346le_alt @ X2999) @ (set_Ar577454304le_alt @ X2999)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_91])])).
% 29.06/5.38 thf(c_0_105, plain, ![X3098:list_A2115238852le_alt]:((((X3098)=(nil_Ar1286194111le_alt))|((hd_Arr1965683346le_alt @ (rev_Ar1106406943le_alt @ X3098))=(last_A1217315288le_alt @ X3098)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_92])])).
% 29.06/5.38 thf(c_0_106, plain, ![X3116:list_A2115238852le_alt]:(((((nil_Ar1286194111le_alt)!=(rev_Ar1106406943le_alt @ X3116))|((X3116)=(nil_Ar1286194111le_alt)))&(((X3116)!=(nil_Ar1286194111le_alt))|((nil_Ar1286194111le_alt)=(rev_Ar1106406943le_alt @ X3116))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_488_Nil__is__rev__conv])])])).
% 29.06/5.38 thf(c_0_107, plain, ![X11:list_A2115238852le_alt]:(~((epred24_1 @ X11 @ (last_A1217315288le_alt @ X11)))), inference(er,[status(thm)],[c_0_93])).
% 29.06/5.38 thf(c_0_108, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|((last_A1217315288le_alt @ (cons_A228743023le_alt @ X2 @ X11))=(last_A1217315288le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_94])).
% 29.06/5.38 thf(c_0_109, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((last_A1217315288le_alt @ (append179082452le_alt @ X11 @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt)))=(X2))), inference(split_conjunct,[status(thm)],[c_0_95])).
% 29.06/5.38 thf(c_0_110, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((append179082452le_alt @ X11 @ (cons_A228743023le_alt @ X2 @ nil_Ar1286194111le_alt))!=(nil_Ar1286194111le_alt))), inference(er,[status(thm)],[c_0_96])).
% 29.06/5.38 thf(c_0_111, plain, ![X2:arrow_475358991le_alt, X4:arrow_475358991le_alt, X5:arrow_475358991le_alt, X7:arrow_475358991le_alt, X6:produc1501160679le_alt > $o]:((((X5)=(X2))|(member214075476le_alt @ (produc1347929815le_alt @ X5 @ X2) @ (arrow_2098199487_below @ X6 @ X4 @ X7))|((X4)=(X7))|((X2)!=(X4))|~((member214075476le_alt @ (produc1347929815le_alt @ X5 @ X7) @ X6))|~((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)))), inference(split_conjunct,[status(thm)],[c_0_65])).
% 29.06/5.38 thf(c_0_112, plain, ![X2:arrow_475358991le_alt, X1:arrow_1429601828e_indi]:((((b)=(c))|(member214075476le_alt @ (produc1347929815le_alt @ X2 @ b) @ (p @ X1))|~((member214075476le_alt @ (produc1347929815le_alt @ X2 @ c) @ (epred20_0 @ X1))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_86]), c_0_98])])).
% 29.06/5.38 thf(c_0_113, negated_conjecture, ((member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (epred20_0 @ esk1_0))|(p @ esk1_0 @ (produc1347929815le_alt @ a @ b))), inference(spm,[status(thm)],[c_0_99, c_0_100])).
% 29.06/5.38 thf(c_0_114, plain, ![X6:produc1501160679le_alt > $o, X71:produc1501160679le_alt]:(((member214075476le_alt @ X71 @ X6)|~((X6 @ X71)))), inference(split_conjunct,[status(thm)],[c_0_84])).
% 29.06/5.38 thf(c_0_115, negated_conjecture, (~((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0)))|~((member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (arrow_2098199487_below @ (p @ esk1_0) @ c @ b)))), inference(split_conjunct,[status(thm)],[c_0_70])).
% 29.06/5.38 thf(c_0_116, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((~((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ X11)))|~((distin236324274le_alt @ (esk86_0 @ X2 @ X11))))), inference(spm,[status(thm)],[c_0_101, c_0_102])).
% 29.06/5.38 thf(c_0_117, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((distin236324274le_alt @ (esk86_0 @ X2 @ (rev_Ar1106406943le_alt @ X11)))|~((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ X11))))), inference(spm,[status(thm)],[c_0_103, c_0_41])).
% 29.06/5.38 thf(c_0_118, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|(member84363362le_alt @ (hd_Arr1965683346le_alt @ X11) @ (set_Ar577454304le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_104])).
% 29.06/5.38 thf(c_0_119, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|((hd_Arr1965683346le_alt @ (rev_Ar1106406943le_alt @ X11))=(last_A1217315288le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_105])).
% 29.06/5.38 thf(c_0_120, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|((nil_Ar1286194111le_alt)!=(rev_Ar1106406943le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_106])).
% 29.06/5.38 thf(c_0_121, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|~((epred24_1 @ (cons_A228743023le_alt @ X2 @ X11) @ (last_A1217315288le_alt @ X11))))), inference(spm,[status(thm)],[c_0_107, c_0_108])).
% 29.06/5.38 thf(c_0_122, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:(((last_A1217315288le_alt @ (esk86_0 @ X2 @ X11))=(X2))), inference(rw,[status(thm)],[c_0_109, c_0_35])).
% 29.06/5.38 thf(c_0_123, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((esk86_0 @ X2 @ X11)!=(nil_Ar1286194111le_alt))), inference(rw,[status(thm)],[c_0_110, c_0_35])).
% 29.06/5.38 thf(c_0_124, plain, ![X1702:list_A2115238852le_alt]:((((X1702)!=(nil_Ar1286194111le_alt))=>(member84363362le_alt @ (last_A1217315288le_alt @ X1702) @ (set_Ar577454304le_alt @ X1702)))), inference(fof_simplification,[status(thm)],[fact_572_last__in__set])).
% 29.06/5.38 thf(c_0_125, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((distin236324274le_alt @ X11)|~((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ X11))))), inference(split_conjunct,[status(thm)],[c_0_87])).
% 29.06/5.38 thf(c_0_126, plain, (distin236324274le_alt @ (cons_A228743023le_alt @ a @ (cons_A228743023le_alt @ b @ (cons_A228743023le_alt @ c @ nil_Ar1286194111le_alt)))), inference(split_conjunct,[status(thm)],[fact_4_dist])).
% 29.06/5.38 thf(c_0_127, plain, ![X1777:arrow_475358991le_alt, X1778:list_A2115238852le_alt]:((((member84363362le_alt @ X1777 @ (set_Ar577454304le_alt @ X1778))=>((insert2120566741le_alt @ X1777 @ X1778)=(X1778)))&(~(member84363362le_alt @ X1777 @ (set_Ar577454304le_alt @ X1778))=>((insert2120566741le_alt @ X1777 @ X1778)=(cons_A228743023le_alt @ X1777 @ X1778))))), inference(fof_simplification,[status(thm)],[fact_605_List_Oinsert__def])).
% 29.06/5.38 thf(c_0_128, plain, ![X2:arrow_475358991le_alt, X4:arrow_475358991le_alt, X5:arrow_475358991le_alt, X6:produc1501160679le_alt > $o]:((((X2)=(X4))|((X2)=(X5))|(member214075476le_alt @ (produc1347929815le_alt @ X5 @ X2) @ (arrow_2098199487_below @ X6 @ X2 @ X4))|~((member214075476le_alt @ (produc1347929815le_alt @ X5 @ X4) @ X6))|~((member377231867_alt_o @ X6 @ arrow_823908191le_Lin)))), inference(er,[status(thm)],[c_0_111])).
% 29.06/5.38 thf(c_0_129, negated_conjecture, (((b)=(c))|(member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_113]), c_0_114])).
% 29.06/5.38 thf(c_0_130, negated_conjecture, (~((member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (epred20_0 @ esk1_0)))|~((member214075476le_alt @ (produc1347929815le_alt @ a @ b) @ (p @ esk1_0)))), inference(rw,[status(thm)],[c_0_115, c_0_86])).
% 29.06/5.38 thf(c_0_131, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((~((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ (rev_Ar1106406943le_alt @ X11))))|~((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ X11))))), inference(spm,[status(thm)],[c_0_116, c_0_117])).
% 29.06/5.38 thf(c_0_132, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|(member84363362le_alt @ (last_A1217315288le_alt @ X11) @ (set_Ar577454304le_alt @ (rev_Ar1106406943le_alt @ X11))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_119]), c_0_120])).
% 29.06/5.38 thf(c_0_133, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt, X4:arrow_475358991le_alt]:(~((epred24_1 @ (cons_A228743023le_alt @ X2 @ (esk86_0 @ X4 @ X11)) @ X4))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_122]), c_0_123])).
% 29.06/5.38 thf(c_0_134, plain, ![X11:list_A2115238852le_alt, X2:arrow_475358991le_alt]:((((X2)=(last_A1217315288le_alt @ X11))|(epred24_1 @ X11 @ X2))), inference(split_conjunct,[status(thm)],[c_0_78])).
% 29.06/5.38 thf(c_0_135, plain, ![X2992:list_A2115238852le_alt]:((((X2992)=(nil_Ar1286194111le_alt))|(member84363362le_alt @ (last_A1217315288le_alt @ X2992) @ (set_Ar577454304le_alt @ X2992)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_124])])).
% 29.06/5.38 thf(c_0_136, plain, (distin236324274le_alt @ (cons_A228743023le_alt @ b @ (esk86_0 @ c @ nil_Ar1286194111le_alt))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125, c_0_126]), c_0_50])).
% 29.06/5.38 thf(c_0_137, plain, ![X3000:arrow_475358991le_alt, X3001:list_A2115238852le_alt]:(((~(member84363362le_alt @ X3000 @ (set_Ar577454304le_alt @ X3001))|((insert2120566741le_alt @ X3000 @ X3001)=(X3001)))&((member84363362le_alt @ X3000 @ (set_Ar577454304le_alt @ X3001))|((insert2120566741le_alt @ X3000 @ X3001)=(cons_A228743023le_alt @ X3000 @ X3001))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_127])])])).
% 29.06/5.38 thf(c_0_138, negated_conjecture, ![X2:arrow_475358991le_alt]:((((b)=(c))|((X2)=(b))|((X2)=(a))|(member214075476le_alt @ (produc1347929815le_alt @ a @ X2) @ (arrow_2098199487_below @ (p @ esk1_0) @ X2 @ b)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_98])])).
% 29.06/5.38 thf(c_0_139, negated_conjecture, (((b)=(c))|~((member214075476le_alt @ (produc1347929815le_alt @ a @ c) @ (epred20_0 @ esk1_0)))), inference(spm,[status(thm)],[c_0_130, c_0_129])).
% 29.06/5.38 thf(c_0_140, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|~((distin236324274le_alt @ (cons_A228743023le_alt @ (last_A1217315288le_alt @ X11) @ X11))))), inference(spm,[status(thm)],[c_0_131, c_0_132])).
% 29.06/5.38 thf(c_0_141, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt, X4:arrow_475358991le_alt]:(((last_A1217315288le_alt @ (cons_A228743023le_alt @ X2 @ (esk86_0 @ X4 @ X11)))=(X4))), inference(spm,[status(thm)],[c_0_133, c_0_134])).
% 29.06/5.38 thf(c_0_142, plain, ![X2990:arrow_475358991le_alt, X2991:list_A2115238852le_alt]:((~(member84363362le_alt @ X2990 @ (set_Ar577454304le_alt @ X2991))|((insert2120566741le_alt @ X2990 @ X2991)=(X2991)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_548_in__set__insert])])])).
% 29.06/5.38 thf(c_0_143, plain, ![X11:list_A2115238852le_alt]:((((X11)=(nil_Ar1286194111le_alt))|(member84363362le_alt @ (last_A1217315288le_alt @ X11) @ (set_Ar577454304le_alt @ X11)))), inference(split_conjunct,[status(thm)],[c_0_135])).
% 29.06/5.38 thf(c_0_144, plain, ![X66:list_A2115238852le_alt, X67:arrow_475358991le_alt]:(((X66)!=(cons_A228743023le_alt @ X67 @ X66))), inference(fof_simplification,[status(thm)],[fact_43_not__Cons__self])).
% 29.06/5.38 thf(c_0_145, plain, ~((member84363362le_alt @ b @ (set_Ar577454304le_alt @ (esk86_0 @ c @ nil_Ar1286194111le_alt)))), inference(spm,[status(thm)],[c_0_101, c_0_136])).
% 29.06/5.38 thf(c_0_146, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ X11))|((insert2120566741le_alt @ X2 @ X11)=(cons_A228743023le_alt @ X2 @ X11)))), inference(split_conjunct,[status(thm)],[c_0_137])).
% 29.06/5.38 thf(c_0_147, plain, (distin236324274le_alt @ (cons_A228743023le_alt @ a @ (cons_A228743023le_alt @ b @ (esk86_0 @ c @ nil_Ar1286194111le_alt)))), inference(spm,[status(thm)],[c_0_126, c_0_50])).
% 29.06/5.38 thf(c_0_148, plain, (((a)=(c))|((b)=(c))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_138, c_0_86]), c_0_139])).
% 29.06/5.38 thf(c_0_149, plain, ![X2:arrow_475358991le_alt, X4:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(~((distin236324274le_alt @ (cons_A228743023le_alt @ X2 @ (cons_A228743023le_alt @ X4 @ (esk86_0 @ X2 @ X11)))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_140, c_0_141]), c_0_77])).
% 29.06/5.38 thf(c_0_150, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((((insert2120566741le_alt @ X2 @ X11)=(X11))|~((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ X11))))), inference(split_conjunct,[status(thm)],[c_0_142])).
% 29.06/5.38 thf(c_0_151, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:((member84363362le_alt @ X2 @ (set_Ar577454304le_alt @ (esk86_0 @ X2 @ X11)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_143, c_0_122]), c_0_123])).
% 29.06/5.38 thf(c_0_152, plain, ![X2752:list_A2115238852le_alt, X2753:arrow_475358991le_alt]:(((X2752)!=(cons_A228743023le_alt @ X2753 @ X2752))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_144])])).
% 29.06/5.38 thf(c_0_153, plain, ((insert2120566741le_alt @ b @ (esk86_0 @ c @ nil_Ar1286194111le_alt))=(cons_A228743023le_alt @ b @ (esk86_0 @ c @ nil_Ar1286194111le_alt))), inference(spm,[status(thm)],[c_0_145, c_0_146])).
% 29.06/5.38 thf(c_0_154, plain, ((b)=(c)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_147, c_0_148]), c_0_149])).
% 29.06/5.38 thf(c_0_155, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((insert2120566741le_alt @ X2 @ (esk86_0 @ X2 @ X11))=(esk86_0 @ X2 @ X11))), inference(spm,[status(thm)],[c_0_150, c_0_151])).
% 29.06/5.38 thf(c_0_156, plain, ![X2:arrow_475358991le_alt, X11:list_A2115238852le_alt]:(((X11)!=(cons_A228743023le_alt @ X2 @ X11))), inference(split_conjunct,[status(thm)],[c_0_152])).
% 29.06/5.38 thf(c_0_157, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_154]), c_0_155]), c_0_154]), c_0_156]), ['proof']).
% 29.06/5.38 % SZS output end CNFRefutation
% 29.06/5.38 % Parsed axioms : 1031
% 29.06/5.38 % Removed by relevancy pruning/SinE : 798
% 29.06/5.38 % Initial clauses : 447
% 29.06/5.38 % Removed in clause preprocessing : 15
% 29.06/5.38 % Initial clauses in saturation : 432
% 29.06/5.38 % Processed clauses : 12130
% 29.06/5.38 % ...of these trivial : 102
% 29.06/5.38 % ...subsumed : 7812
% 29.06/5.38 % ...remaining for further processing : 4216
% 29.06/5.38 % Other redundant clauses eliminated : 5203
% 29.06/5.38 % Clauses deleted for lack of memory : 0
% 29.06/5.38 % Backward-subsumed : 130
% 29.06/5.38 % Backward-rewritten : 1415
% 29.06/5.38 % Generated clauses : 73500
% 29.06/5.38 % ...of the previous two non-redundant : 64824
% 29.06/5.38 % ...aggressively subsumed : 0
% 29.06/5.38 % Contextual simplify-reflections : 41
% 29.06/5.38 % Paramodulations : 65077
% 29.06/5.38 % Factorizations : 11
% 29.06/5.38 % NegExts : 345
% 29.06/5.38 % Equation resolutions : 5224
% 29.06/5.38 % Disequality decompositions : 0
% 29.06/5.38 % Total rewrite steps : 20070
% 29.06/5.38 % ...of those cached : 17716
% 29.06/5.38 % Propositional unsat checks : 0
% 29.06/5.38 % Propositional check models : 0
% 29.06/5.38 % Propositional check unsatisfiable : 0
% 29.06/5.38 % Propositional clauses : 0
% 29.06/5.38 % Propositional clauses after purity: 0
% 29.06/5.38 % Propositional unsat core size : 0
% 29.06/5.38 % Propositional preprocessing time : 0.000
% 29.06/5.38 % Propositional encoding time : 0.000
% 29.06/5.38 % Propositional solver time : 0.000
% 29.06/5.38 % Success case prop preproc time : 0.000
% 29.06/5.38 % Success case prop encoding time : 0.000
% 29.06/5.38 % Success case prop solver time : 0.000
% 29.06/5.38 % Current number of processed clauses : 2096
% 29.06/5.38 % Positive orientable unit clauses : 280
% 29.06/5.38 % Positive unorientable unit clauses: 0
% 29.06/5.38 % Negative unit clauses : 253
% 29.06/5.38 % Non-unit-clauses : 1563
% 29.06/5.38 % Current number of unprocessed clauses: 52085
% 29.06/5.38 % ...number of literals in the above : 161791
% 29.06/5.38 % Current number of archived formulas : 0
% 29.06/5.38 % Current number of archived clauses : 2061
% 29.06/5.38 % Clause-clause subsumption calls (NU) : 1697252
% 29.06/5.38 % Rec. Clause-clause subsumption calls : 1006312
% 29.06/5.38 % Non-unit clause-clause subsumptions : 4976
% 29.06/5.38 % Unit Clause-clause subsumption calls : 87747
% 29.06/5.38 % Rewrite failures with RHS unbound : 0
% 29.06/5.38 % BW rewrite match attempts : 235
% 29.06/5.38 % BW rewrite match successes : 78
% 29.06/5.38 % Condensation attempts : 0
% 29.06/5.38 % Condensation successes : 0
% 29.06/5.38 % Termbank termtop insertions : 2244413
% 29.06/5.38 % Search garbage collected termcells : 15487
% 29.06/5.38
% 29.06/5.38 % -------------------------------------------------
% 29.06/5.38 % User time : 4.689 s
% 29.06/5.38 % System time : 0.121 s
% 29.06/5.38 % Total time : 4.810 s
% 29.06/5.38 % Maximum resident set size: 7932 pages
% 29.06/5.38
% 29.06/5.38 % -------------------------------------------------
% 29.06/5.38 % User time : 23.289 s
% 29.06/5.38 % System time : 0.615 s
% 29.06/5.38 % Total time : 23.905 s
% 29.06/5.38 % Maximum resident set size: 7168 pages
% 29.06/5.38 % E exiting
%------------------------------------------------------------------------------