%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP045^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:04:11 AM UTC 2026
% Result : Theorem 1.21s 0.55s
% Output : CNFRefutation 1.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP045^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 % Computer : n009.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Tue Sep 29 19:41:30 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.24 Running higher-order theorem proving
% 0.19/0.32 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.TPinnUAQJA/E---3.1_264263.p
% 1.21/0.55 % Version: 3.5.1-ho
% 1.21/0.55 % Preprocessing class: HSLMSMSMSSLNHSA.
% 1.21/0.55 % Scheduled 7 strats onto 8 cores with 300 seconds (2400 total)
% 1.21/0.55 % Starting new_bool_8 with 600s (2) cores
% 1.21/0.55 % Starting new_ho_3 with 300s (1) cores
% 1.21/0.55 % Starting additional_ho_3 with 300s (1) cores
% 1.21/0.55 % Starting full_lambda_10 with 300s (1) cores
% 1.21/0.55 % Starting ehoh_best with 300s (1) cores
% 1.21/0.55 % Starting sh2lt with 300s (1) cores
% 1.21/0.55 % Starting full_lambda_4 with 300s (1) cores
% 1.21/0.55 % new_bool_8 with pid 264307 completed with status 0
% 1.21/0.55 % Result found by new_bool_8
% 1.21/0.55 % Preprocessing class: HSLMSMSMSSLNHSA.
% 1.21/0.55 % Scheduled 7 strats onto 8 cores with 300 seconds (2400 total)
% 1.21/0.55 % Starting new_bool_8 with 600s (2) cores
% 1.21/0.55 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 1.21/0.55 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 1.21/0.55 % Search class: HGHSM-FFMF31-DHSFFSBN
% 1.21/0.55 % partial match(3): HGHSM-FSLM31-DHSFFSBN
% 1.21/0.55 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.21/0.55 % Starting SubtermCWHack with 55s (1) cores
% 1.21/0.55 % Starting new_bool_8 with 61s (1) cores
% 1.21/0.55 % SubtermCWHack with pid 264314 completed with status 0
% 1.21/0.55 % Result found by SubtermCWHack
% 1.21/0.55 % Preprocessing class: HSLMSMSMSSLNHSA.
% 1.21/0.55 % Scheduled 7 strats onto 8 cores with 300 seconds (2400 total)
% 1.21/0.55 % Starting new_bool_8 with 600s (2) cores
% 1.21/0.55 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 1.21/0.55 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 1.21/0.55 % Search class: HGHSM-FFMF31-DHSFFSBN
% 1.21/0.55 % partial match(3): HGHSM-FSLM31-DHSFFSBN
% 1.21/0.55 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.21/0.55 % Starting SubtermCWHack with 55s (1) cores
% 1.21/0.55 % Preprocessing time : 0.004 s
% 1.21/0.55
% 1.21/0.55 % Proof found!
% 1.21/0.55 % SZS status Theorem
% 1.21/0.55 % SZS output start CNFRefutation
% 1.21/0.55 thf(decl_sort1, type, l: $tType).
% 1.21/0.55 thf(decl_sort2, type, option_val_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort3, type, produc1156025366_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort4, type, expr_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort5, type, val_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort6, type, cntxt_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort7, type, r: $tType).
% 1.21/0.55 thf(decl_sort8, type, option1457017436_r_l_v: $tType).
% 1.21/0.55 thf(decl_sort9, type, produc1164766533_r_l_v: $tType).
% 1.21/0.55 thf(decl_23, type, combine_l_val_r_l_v: (l > option_val_r_l_v) > (l > option_val_r_l_v) > l > option_val_r_l_v).
% 1.21/0.55 thf(decl_34, type, vE_r_l_v: val_r_l_v > expr_r_l_v).
% 1.21/0.55 thf(decl_35, type, plug_r_l_v: cntxt_r_l_v > expr_r_l_v > expr_r_l_v).
% 1.21/0.55 thf(decl_38, type, rid_r_l_v: r > val_r_l_v).
% 1.21/0.55 thf(decl_58, type, fun_up709272714_r_l_v: (r > option1457017436_r_l_v) > r > option1457017436_r_l_v > r > option1457017436_r_l_v).
% 1.21/0.55 thf(decl_77, type, none_val_r_l_v: option_val_r_l_v).
% 1.21/0.55 thf(decl_80, type, some_P1807977723_r_l_v: produc1156025366_r_l_v > option1457017436_r_l_v).
% 1.21/0.55 thf(decl_94, type, produc1834103605_r_l_v: (l > option_val_r_l_v) > expr_r_l_v > produc1164766533_r_l_v).
% 1.21/0.55 thf(decl_95, type, produc297528454_r_l_v: (l > option_val_r_l_v) > produc1164766533_r_l_v > produc1156025366_r_l_v).
% 1.21/0.55 thf(decl_119, type, e: cntxt_r_l_v).
% 1.21/0.55 thf(decl_120, type, sigma: l > option_val_r_l_v).
% 1.21/0.55 thf(decl_121, type, tau: l > option_val_r_l_v).
% 1.21/0.55 thf(decl_122, type, e2: expr_r_l_v).
% 1.21/0.55 thf(decl_123, type, r2: r).
% 1.21/0.55 thf(decl_124, type, r3: r).
% 1.21/0.55 thf(decl_125, type, r4: r).
% 1.21/0.55 thf(decl_126, type, s_1: r > option1457017436_r_l_v).
% 1.21/0.55 thf(decl_127, type, s_2: r > option1457017436_r_l_v).
% 1.21/0.55 thf(decl_130, type, x: produc1156025366_r_l_v).
% 1.21/0.55 thf(decl_162, type, esk32_0: l > option_val_r_l_v).
% 1.21/0.55 thf(conj_0, conjecture, ((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x)) @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[X1:l]:(none_val_r_l_v)) @ e2))))=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[X1:l]:(none_val_r_l_v)) @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', conj_0)).
% 1.21/0.55 thf(fact_44_fun__upd__same, axiom, ![X11:r > option1457017436_r_l_v, X9:r, X89:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ X11 @ X9 @ X89 @ X9)=(X89))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_44_fun__upd__same)).
% 1.21/0.55 thf(fact_3_assms_I1_J, axiom, ((s_2)=(fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_3_assms_I1_J)).
% 1.21/0.55 thf(fact_23_fun__upd__upd, axiom, ![X11:r > option1457017436_r_l_v, X9:r, X42:option1457017436_r_l_v, X43:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X11 @ X9 @ X42) @ X9 @ X43)=(fun_up709272714_r_l_v @ X11 @ X9 @ X43))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_23_fun__upd__upd)).
% 1.21/0.55 thf(fact_25_fun__upd__triv, axiom, ![X11:r > option1457017436_r_l_v, X9:r]:(((fun_up709272714_r_l_v @ X11 @ X9 @ (X11 @ X9))=(X11))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_25_fun__upd__triv)).
% 1.21/0.55 thf(fact_40_fun__upd__twist, axiom, ![X73:r, X74:r, X75:r > option1457017436_r_l_v, X76:option1457017436_r_l_v, X77:option1457017436_r_l_v]:((((X73)!=(X74))=>((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X75 @ X73 @ X76) @ X74 @ X77)=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X75 @ X74 @ X77) @ X73 @ X76)))), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_40_fun__upd__twist)).
% 1.21/0.55 thf(fact_2_assms_I6_J, axiom, ((r2)!=(r3)), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_2_assms_I6_J)).
% 1.21/0.55 thf(fact_1_assms_I7_J, axiom, ((r2)!=(r4)), file('/export/starexec/sandbox2/tmp/tmp.TPinnUAQJA/E---3.1_264263.p', fact_1_assms_I7_J)).
% 1.21/0.55 thf(c_0_8, negated_conjecture, ~(((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x)) @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[X1:l]:(none_val_r_l_v)) @ e2))))=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[X1:l]:(none_val_r_l_v)) @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x)))), inference(assume_negation,[status(cth)],[conj_0])).
% 1.21/0.55 thf(c_0_9, plain, ![X682:r > option1457017436_r_l_v, X683:r, X684:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ X682 @ X683 @ X684 @ X683)=(X684))), inference(variable_rename,[status(thm)],[fact_44_fun__upd__same])).
% 1.21/0.56 thf(c_0_10, plain, ((s_2)=(fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x))), inference(split_conjunct,[status(thm)],[fact_3_assms_I1_J])).
% 1.21/0.56 thf(c_0_11, negated_conjecture, ((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x)) @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[Z0:l]:(none_val_r_l_v)) @ e2))))!=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[Z0:l]:(none_val_r_l_v)) @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_8])])).
% 1.21/0.56 thf(c_0_12, plain, ![X664:r > option1457017436_r_l_v, X665:r, X666:option1457017436_r_l_v, X667:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X664 @ X665 @ X666) @ X665 @ X667)=(fun_up709272714_r_l_v @ X664 @ X665 @ X667))), inference(variable_rename,[status(thm)],[fact_23_fun__upd__upd])).
% 1.21/0.56 thf(c_0_13, plain, ![X668:r > option1457017436_r_l_v, X669:r]:(((fun_up709272714_r_l_v @ X668 @ X669 @ (X668 @ X669))=(X668))), inference(variable_rename,[status(thm)],[fact_25_fun__upd__triv])).
% 1.21/0.56 thf(c_0_14, plain, ![X3:r, X2:r > option1457017436_r_l_v, X20:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ X2 @ X3 @ X20 @ X3)=(X20))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 1.21/0.56 thf(c_0_15, plain, ![X3:r]:(((fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x) @ X3)=(s_2 @ X3))), inference(arg_cong,[status(thm)],[c_0_10])).
% 1.21/0.56 thf(c_0_16, plain, ![X73:r, X74:r, X75:r > option1457017436_r_l_v, X76:option1457017436_r_l_v, X77:option1457017436_r_l_v]:((((X73)!=(X74))=>((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X75 @ X73 @ X76) @ X74 @ X77)=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X75 @ X74 @ X77) @ X73 @ X76)))), inference(fof_simplification,[status(thm)],[fact_40_fun__upd__twist])).
% 1.21/0.56 thf(c_0_17, negated_conjecture, ((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x)) @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[Z0:l]:(none_val_r_l_v)) @ e2))))!=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ (^[Z0:l]:(none_val_r_l_v)) @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x))), inference(fof_nnf,[status(thm)],[c_0_11])).
% 1.21/0.56 thf(c_0_18, plain, ![X820:l]:(((esk32_0 @ X820)=(none_val_r_l_v))), introduced(definition)).
% 1.21/0.56 thf(c_0_19, plain, ![X3:r, X20:option1457017436_r_l_v, X2:r > option1457017436_r_l_v, X24:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X2 @ X3 @ X20) @ X3 @ X24)=(fun_up709272714_r_l_v @ X2 @ X3 @ X24))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.21/0.56 thf(c_0_20, plain, ![X3:r, X2:r > option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ X2 @ X3 @ (X2 @ X3))=(X2))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.21/0.56 thf(c_0_21, plain, ((s_2 @ r2)=(some_P1807977723_r_l_v @ x)), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 1.21/0.56 thf(c_0_22, plain, ![X673:r, X674:r, X675:r > option1457017436_r_l_v, X676:option1457017436_r_l_v, X677:option1457017436_r_l_v]:((((X673)=(X674))|((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X675 @ X673 @ X676) @ X674 @ X677)=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X675 @ X674 @ X677) @ X673 @ X676)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])).
% 1.21/0.56 thf(c_0_23, plain, ((r2)!=(r3)), inference(fof_simplification,[status(thm)],[fact_2_assms_I6_J])).
% 1.21/0.56 thf(c_0_24, plain, ((r2)!=(r4)), inference(fof_simplification,[status(thm)],[fact_1_assms_I7_J])).
% 1.21/0.56 thf(c_0_25, negated_conjecture, ((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r2 @ (some_P1807977723_r_l_v @ x)) @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ esk32_0 @ e2))))!=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ esk32_0 @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_17]), c_0_18]), c_0_18])).
% 1.21/0.56 thf(c_0_26, plain, ![X20:option1457017436_r_l_v]:(((fun_up709272714_r_l_v @ s_1 @ r2 @ X20)=(fun_up709272714_r_l_v @ s_2 @ r2 @ X20))), inference(spm,[status(thm)],[c_0_19, c_0_10])).
% 1.21/0.56 thf(c_0_27, plain, ((fun_up709272714_r_l_v @ s_2 @ r2 @ (some_P1807977723_r_l_v @ x))=(s_2)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 1.21/0.56 thf(c_0_28, plain, ![X8:r, X2:r > option1457017436_r_l_v, X3:r, X24:option1457017436_r_l_v, X20:option1457017436_r_l_v]:((((X3)=(X8))|((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X2 @ X3 @ X20) @ X8 @ X24)=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X2 @ X8 @ X24) @ X3 @ X20)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 1.21/0.56 thf(c_0_29, plain, ((r2)!=(r3)), inference(fof_nnf,[status(thm)],[c_0_23])).
% 1.21/0.56 thf(c_0_30, plain, ((r2)!=(r4)), inference(fof_nnf,[status(thm)],[c_0_24])).
% 1.21/0.56 thf(c_0_31, negated_conjecture, ((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_1 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ esk32_0 @ e2)))) @ r2 @ (some_P1807977723_r_l_v @ x))!=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ s_2 @ r3 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ sigma @ (produc1834103605_r_l_v @ tau @ (plug_r_l_v @ e @ (vE_r_l_v @ (rid_r_l_v @ r4))))))) @ r4 @ (some_P1807977723_r_l_v @ (produc297528454_r_l_v @ (combine_l_val_r_l_v @ sigma @ tau) @ (produc1834103605_r_l_v @ esk32_0 @ e2))))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26]), c_0_27])).
% 1.21/0.56 thf(c_0_32, plain, ![X2:r > option1457017436_r_l_v, X3:r, X8:r, X42:option1457017436_r_l_v, X24:option1457017436_r_l_v, X20:option1457017436_r_l_v, X9:r]:((((fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X2 @ X3 @ X20) @ X8 @ X24) @ X9 @ X42)=(fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ (fun_up709272714_r_l_v @ X2 @ X8 @ X24) @ X9 @ X42) @ X3 @ X20))|((X3)=(X8))|((X3)=(X9)))), inference(spm,[status(thm)],[c_0_28, c_0_28])).
% 1.21/0.56 thf(c_0_33, plain, ((r2)!=(r3)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.21/0.56 thf(c_0_34, plain, ((r2)!=(r4)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 1.21/0.56 thf(c_0_35, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_26]), c_0_27])]), c_0_33]), c_0_34]), ['proof']).
% 1.21/0.56 % SZS output end CNFRefutation
% 1.21/0.56 % Parsed axioms : 493
% 1.21/0.56 % Removed by relevancy pruning/SinE : 443
% 1.21/0.56 % Initial clauses : 121
% 1.21/0.56 % Removed in clause preprocessing : 47
% 1.21/0.56 % Initial clauses in saturation : 74
% 1.21/0.56 % Processed clauses : 1562
% 1.21/0.56 % ...of these trivial : 16
% 1.21/0.56 % ...subsumed : 1149
% 1.21/0.56 % ...remaining for further processing : 397
% 1.21/0.56 % Other redundant clauses eliminated : 493
% 1.21/0.56 % Clauses deleted for lack of memory : 0
% 1.21/0.56 % Backward-subsumed : 16
% 1.21/0.56 % Backward-rewritten : 15
% 1.21/0.56 % Generated clauses : 6193
% 1.21/0.56 % ...of the previous two non-redundant : 4787
% 1.21/0.56 % ...aggressively subsumed : 0
% 1.21/0.56 % Contextual simplify-reflections : 0
% 1.21/0.56 % Paramodulations : 5647
% 1.21/0.56 % Factorizations : 1
% 1.21/0.56 % NegExts : 0
% 1.21/0.56 % Equation resolutions : 511
% 1.21/0.56 % Disequality decompositions : 0
% 1.21/0.56 % Total rewrite steps : 1822
% 1.21/0.56 % ...of those cached : 1646
% 1.21/0.56 % Propositional unsat checks : 0
% 1.21/0.56 % Propositional check models : 0
% 1.21/0.56 % Propositional check unsatisfiable : 0
% 1.21/0.56 % Propositional clauses : 0
% 1.21/0.56 % Propositional clauses after purity: 0
% 1.21/0.56 % Propositional unsat core size : 0
% 1.21/0.56 % Propositional preprocessing time : 0.000
% 1.21/0.56 % Propositional encoding time : 0.000
% 1.21/0.56 % Propositional solver time : 0.000
% 1.21/0.56 % Success case prop preproc time : 0.000
% 1.21/0.56 % Success case prop encoding time : 0.000
% 1.21/0.56 % Success case prop solver time : 0.000
% 1.21/0.56 % Current number of processed clauses : 354
% 1.21/0.56 % Positive orientable unit clauses : 39
% 1.21/0.56 % Positive unorientable unit clauses: 0
% 1.21/0.56 % Negative unit clauses : 21
% 1.21/0.56 % Non-unit-clauses : 294
% 1.21/0.56 % Current number of unprocessed clauses: 3166
% 1.21/0.56 % ...number of literals in the above : 11787
% 1.21/0.56 % Current number of archived formulas : 0
% 1.21/0.56 % Current number of archived clauses : 37
% 1.21/0.56 % Clause-clause subsumption calls (NU) : 15607
% 1.21/0.56 % Rec. Clause-clause subsumption calls : 10704
% 1.21/0.56 % Non-unit clause-clause subsumptions : 863
% 1.21/0.56 % Unit Clause-clause subsumption calls : 503
% 1.21/0.56 % Rewrite failures with RHS unbound : 0
% 1.21/0.56 % BW rewrite match attempts : 90
% 1.21/0.56 % BW rewrite match successes : 7
% 1.21/0.56 % Condensation attempts : 0
% 1.21/0.56 % Condensation successes : 0
% 1.21/0.56 % Termbank termtop insertions : 76612
% 1.21/0.56 % Search garbage collected termcells : 5784
% 1.21/0.56
% 1.21/0.56 % -------------------------------------------------
% 1.21/0.56 % User time : 0.144 s
% 1.21/0.56 % System time : 0.009 s
% 1.21/0.56 % Total time : 0.153 s
% 1.21/0.56 % Maximum resident set size: 4980 pages
% 1.21/0.56
% 1.21/0.56 % -------------------------------------------------
% 1.21/0.56 % User time : 0.284 s
% 1.21/0.56 % System time : 0.025 s
% 1.21/0.56 % Total time : 0.309 s
% 1.21/0.56 % Maximum resident set size: 5376 pages
% 1.21/0.56 % E exiting
%------------------------------------------------------------------------------