%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWX234_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 : Thu Sep 24 03:14:21 PM UTC 2026
% Result : Theorem 15.88s 2.75s
% Output : CNFRefutation 15.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX234_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 10:36:47 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.40 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.88/2.75 % Version: 3.5.1
% 15.88/2.75 % Preprocessing class: FSLSSMSMSSSNFFN.
% 15.88/2.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.88/2.75 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 15.88/2.75 % Starting new_bool_3 with 300s (1) cores
% 15.88/2.75 % Starting new_bool_1 with 300s (1) cores
% 15.88/2.75 % Starting sh5l with 300s (1) cores
% 15.88/2.75 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 3242435 completed with status 0
% 15.88/2.75 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 15.88/2.75 % Preprocessing class: FSLSSMSMSSSNFFN.
% 15.88/2.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.88/2.75 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 15.88/2.75 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 15.88/2.75 % No SInE strategy applied
% 15.88/2.75 % Search class: FGHSM-FFMS31-MFFFFFBN
% 15.88/2.75 % partial match(1): FGHSM-FFMS31-MFFFFFNN
% 15.88/2.75 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 15.88/2.75 % Starting SubtermCWHack with 136s (1) cores
% 15.88/2.75 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 15.88/2.75 % Starting G-E--_107_C37_SOS_F1_PI_AE_Q4_CS_SP_PS_S0Y with 380s (1) cores
% 15.88/2.75 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S059I with 136s (1) cores
% 15.88/2.75 % Starting G-E--_208_B07----D_F1_SE_CS_SP_PS_S5PRR_RG_S04AA with 136s (1) cores
% 15.88/2.75 % G-E--_107_C37_SOS_F1_PI_AE_Q4_CS_SP_PS_S0Y with pid 3242443 completed with status 0
% 15.88/2.75 % Result found by G-E--_107_C37_SOS_F1_PI_AE_Q4_CS_SP_PS_S0Y
% 15.88/2.75 % Preprocessing class: FSLSSMSMSSSNFFN.
% 15.88/2.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.88/2.75 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 15.88/2.75 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 15.88/2.75 % No SInE strategy applied
% 15.88/2.75 % Search class: FGHSM-FFMS31-MFFFFFBN
% 15.88/2.75 % partial match(1): FGHSM-FFMS31-MFFFFFNN
% 15.88/2.75 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 15.88/2.75 % Starting SubtermCWHack with 136s (1) cores
% 15.88/2.75 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 15.88/2.75 % Starting G-E--_107_C37_SOS_F1_PI_AE_Q4_CS_SP_PS_S0Y with 380s (1) cores
% 15.88/2.75 % Preprocessing time : 0.002 s
% 15.88/2.75 % Presaturation interreduction done
% 15.88/2.75
% 15.88/2.75 % Proof found!
% 15.88/2.75 % SZS status Theorem
% 15.88/2.75 % SZS output start CNFRefutation
% 15.88/2.75 tff(decl_23, type, cons3: ($o * $i) > $i).
% 15.88/2.75 tff(decl_24, type, pair2: ($i * $i) > $i).
% 15.88/2.75 tff(decl_27, type, cons: ($i * $i) > $i).
% 15.88/2.75 tff(decl_31, type, cons2: ($i * $i) > $i).
% 15.88/2.75 tff(decl_34, type, nil2: $i).
% 15.88/2.75 tff(decl_38, type, a: $i).
% 15.88/2.75 tff(decl_39, type, b: $i).
% 15.88/2.75 tff(decl_41, type, atom: $i > $i).
% 15.88/2.75 tff(decl_42, type, proj1Atom: $i > $i).
% 15.88/2.75 tff(decl_43, type, x: ($i * $i) > $i).
% 15.88/2.75 tff(decl_44, type, proj1: $i > $i).
% 15.88/2.75 tff(decl_45, type, proj2: $i > $i).
% 15.88/2.75 tff(decl_46, type, y: ($i * $i) > $i).
% 15.88/2.75 tff(decl_47, type, proj12: $i > $i).
% 15.88/2.75 tff(decl_48, type, proj22: $i > $i).
% 15.88/2.75 tff(decl_49, type, star: $i > $i).
% 15.88/2.75 tff(decl_50, type, proj1Star: $i > $i).
% 15.88/2.75 tff(decl_51, type, nil4: $i).
% 15.88/2.75 tff(decl_52, type, eps: $i).
% 15.88/2.75 tff(decl_55, type, splits: ($i * $i) > $i).
% 15.88/2.75 tff(decl_56, type, splits2: $i > $i).
% 15.88/2.75 tff(decl_57, type, or2: $i > $o).
% 15.88/2.75 tff(decl_58, type, eps2: $i > $o).
% 15.88/2.75 tff(decl_59, type, step: ($i * $i) > $i).
% 15.88/2.75 tff(decl_60, type, rec: ($i * $i) > $o).
% 15.88/2.75 tff(decl_61, type, reck2: ($i * $i) > $o).
% 15.88/2.75 tff(decl_62, type, reck: ($i * $i * $i) > $i).
% 15.88/2.75 tff(decl_63, type, epred1_0: $o).
% 15.88/2.75 tff(decl_64, type, epred2_0: $o).
% 15.88/2.75 fof(axiom_076, axiom, ![X13, X14, X19, X25, X15]:(reck(X13,X14,cons(pair2(X25,X15),X19))=cons3((reck2(X13,X25)&rec(X14,X15)),reck(X13,X14,X19))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_076)).
% 15.88/2.75 fof(axiom_048, axiom, ![X8, X11]:(splits2(cons2(X8,X11))=cons(pair2(nil2,cons2(X8,X11)),splits(X8,splits2(X11)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_048)).
% 15.88/2.75 fof(axiom_050, axiom, ![X12:$o, X11]:((or2(cons3(X12,X11))<=>(X12|or2(X11)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_050)).
% 15.88/2.75 fof(axiom_064, axiom, ![X1, X19, X11]:((rec(X1,cons2(X19,X11))<=>rec(step(X1,X19),X11))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_064)).
% 15.88/2.75 fof(axiom_063, axiom, ![X1]:((rec(X1,nil2)<=>eps2(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_063)).
% 15.88/2.75 fof(goal_077, conjecture, ?[X13]:(reck2(X13,cons2(a,cons2(b,cons2(b,nil2))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal_077)).
% 15.88/2.75 fof(axiom_072, axiom, ![X8, X15, X16]:((reck2(y(X15,X16),X8)<=>or2(reck(X15,X16,splits2(X8))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_072)).
% 15.88/2.75 fof(axiom_031, axiom, ![X1, X2, X6]:(atom(X1)!=x(X2,X6)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_031)).
% 15.88/2.75 fof(axiom_051, axiom, ![X1]:((X1!=eps=>(X1!=x(proj1(X1),proj2(X1))=>(X1!=y(proj12(X1),proj22(X1))=>(X1!=star(proj1Star(X1))=>~(eps2(X1))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_051)).
% 15.88/2.75 fof(axiom_024, axiom, ![X1, X2]:(nil4!=x(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_024)).
% 15.88/2.75 fof(axiom_056, axiom, ![X1, X8]:((X1!=atom(proj1Atom(X1))=>(X1!=x(proj1(X1),proj2(X1))=>(X1!=y(proj12(X1),proj22(X1))=>(X1!=star(proj1Star(X1))=>step(X1,X8)=nil4))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_056)).
% 15.88/2.75 fof(axiom_061, axiom, ![X8, X15, X16]:((~(eps2(X15))=>step(y(X15,X16),X8)=x(y(step(X15,X8),X16),nil4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_061)).
% 15.88/2.75 fof(axiom_057, axiom, ![X8, X17]:((X17=X8=>step(atom(X17),X8)=eps)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_057)).
% 15.88/2.75 fof(axiom_032, axiom, ![X1, X2, X6]:(atom(X1)!=y(X2,X6)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_032)).
% 15.88/2.75 fof(axiom_033, axiom, ![X1, X2]:(atom(X1)!=star(X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_033)).
% 15.88/2.75 fof(axiom_027, axiom, ![X1]:(eps!=atom(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_027)).
% 15.88/2.75 fof(axiom_025, axiom, ![X1, X2]:(nil4!=y(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_025)).
% 15.88/2.75 fof(axiom_026, axiom, ![X1]:(nil4!=star(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_026)).
% 15.88/2.75 fof(axiom_023, axiom, ![X1]:(nil4!=atom(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_023)).
% 15.88/2.75 fof(axiom_066, axiom, reck2(eps,nil2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_066)).
% 15.88/2.75 fof(axiom_059, axiom, ![X8, X13, X14]:(step(x(X13,X14),X8)=x(step(X13,X8),step(X14,X8))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_059)).
% 15.88/2.75 fof(axiom_053, axiom, ![X13, X14]:((eps2(x(X13,X14))<=>(eps2(X13)|eps2(X14)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_053)).
% 15.88/2.75 fof(axiom_060, axiom, ![X8, X15, X16]:((eps2(X15)=>step(y(X15,X16),X8)=x(y(step(X15,X8),X16),step(X16,X8)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_060)).
% 15.88/2.75 fof(axiom_062, axiom, ![X8, X18]:(step(star(X18),X8)=y(step(X18,X8),star(X18))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_062)).
% 15.88/2.75 fof(axiom_054, axiom, ![X15, X16]:((eps2(y(X15,X16))<=>(eps2(X15)&eps2(X16)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_054)).
% 15.88/2.75 fof(axiom_055, axiom, ![X8]:(eps2(star(X8))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_055)).
% 15.88/2.75 fof(axiom_052, axiom, eps2(eps), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_052)).
% 15.88/2.75 fof(c_0_27, axiom, ![X13, X14, X19, X25, X15]:(((~((reck2(X13,X25)&rec(X14,X15)))|reck(X13,X14,cons(pair2(X25,X15),X19))=cons3($true,reck(X13,X14,X19)))&((reck2(X13,X25)&rec(X14,X15))|reck(X13,X14,cons(pair2(X25,X15),X19))=cons3($false,reck(X13,X14,X19))))), inference(fool_unroll,[status(thm)],[axiom_076])).
% 15.88/2.75 fof(c_0_28, plain, ![X156, X157, X158, X159, X160]:(((~reck2(X156,X159)|~rec(X157,X160)|reck(X156,X157,cons(pair2(X159,X160),X158))=cons3($true,reck(X156,X157,X158)))&((reck2(X156,X159)|reck(X156,X157,cons(pair2(X159,X160),X158))=cons3($false,reck(X156,X157,X158)))&(rec(X157,X160)|reck(X156,X157,cons(pair2(X159,X160),X158))=cons3($false,reck(X156,X157,X158)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])])).
% 15.88/2.75 fof(c_0_29, plain, ![X103, X104]:(splits2(cons2(X103,X104))=cons(pair2(nil2,cons2(X103,X104)),splits(X103,splits2(X104)))), inference(variable_rename,[status(thm)],[axiom_048])).
% 15.88/2.75 fof(c_0_30, plain, ![X105:$o, X106]:(((~or2(cons3(X105,X106))|(X105|or2(X106)))&((~X105|or2(cons3(X105,X106)))&(~or2(X106)|or2(cons3(X105,X106)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_050])])])])).
% 15.88/2.75 cnf(c_0_31, plain, (reck(X1,X6,cons(pair2(X2,X7),X8))=cons3($true,reck(X1,X6,X8))|~reck2(X1,X2)|~rec(X6,X7)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 15.88/2.75 cnf(c_0_32, plain, (splits2(cons2(X1,X2))=cons(pair2(nil2,cons2(X1,X2)),splits(X1,splits2(X2)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 15.88/2.75 fof(c_0_33, plain, ![X131, X132, X133]:(((~rec(X131,cons2(X132,X133))|rec(step(X131,X132),X133))&(~rec(step(X131,X132),X133)|rec(X131,cons2(X132,X133))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_064])])])).
% 15.88/2.75 fof(c_0_34, plain, ![X130]:(((~rec(X130,nil2)|eps2(X130))&(~eps2(X130)|rec(X130,nil2)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_063])])])).
% 15.88/2.75 fof(c_0_35, negated_conjecture, ~(?[X13]:(reck2(X13,cons2(a,cons2(b,cons2(b,nil2)))))), inference(assume_negation,[status(cth)],[goal_077])).
% 15.88/2.75 fof(c_0_36, plain, ![X147, X148, X149]:(((~reck2(y(X148,X149),X147)|or2(reck(X148,X149,splits2(X147))))&(~or2(reck(X148,X149,splits2(X147)))|reck2(y(X148,X149),X147)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_072])])])).
% 15.88/2.75 cnf(c_0_37, plain, (or2(cons3($true,X1))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_30])])])).
% 15.88/2.75 cnf(c_0_38, plain, (cons3($true,reck(X1,X2,splits(X6,splits2(X7))))=reck(X1,X2,splits2(cons2(X6,X7)))|~reck2(X1,nil2)|~rec(X2,cons2(X6,X7))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 15.88/2.75 fof(c_0_39, plain, ![X1, X2, X6]:(atom(X1)!=x(X2,X6)), inference(fof_simplification,[status(thm)],[axiom_031])).
% 15.88/2.75 fof(c_0_40, plain, ![X1]:((X1!=eps=>(X1!=x(proj1(X1),proj2(X1))=>(X1!=y(proj12(X1),proj22(X1))=>(X1!=star(proj1Star(X1))=>~eps2(X1)))))), inference(fof_simplification,[status(thm)],[axiom_051])).
% 15.88/2.75 fof(c_0_41, plain, ![X1, X2]:(nil4!=x(X1,X2)), inference(fof_simplification,[status(thm)],[axiom_024])).
% 15.88/2.75 fof(c_0_42, plain, ![X1, X8]:((X1!=atom(proj1Atom(X1))=>(X1!=x(proj1(X1),proj2(X1))=>(X1!=y(proj12(X1),proj22(X1))=>(X1!=star(proj1Star(X1))=>step(X1,X8)=nil4))))), inference(fof_simplification,[status(thm)],[axiom_056])).
% 15.88/2.75 cnf(c_0_43, plain, (rec(X1,cons2(X2,X6))|~rec(step(X1,X2),X6)), inference(split_conjunct,[status(thm)],[c_0_33])).
% 15.88/2.75 cnf(c_0_44, plain, (rec(X1,nil2)|~eps2(X1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 15.88/2.75 fof(c_0_45, negated_conjecture, ![X161]:(~reck2(X161,cons2(a,cons2(b,cons2(b,nil2))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])])).
% 15.88/2.75 cnf(c_0_46, plain, (reck2(y(X1,X2),X6)|~or2(reck(X1,X2,splits2(X6)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 15.88/2.75 cnf(c_0_47, plain, (or2(reck(X1,X2,splits2(cons2(X6,X7))))|~reck2(X1,nil2)|~rec(X2,cons2(X6,X7))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 15.88/2.75 fof(c_0_48, plain, (~epred1_0<=>![X1]:(~reck2(X1,nil2))), introduced(definition)).
% 15.88/2.75 fof(c_0_49, plain, ![X8, X15, X16]:((~eps2(X15)=>step(y(X15,X16),X8)=x(y(step(X15,X8),X16),nil4))), inference(fof_simplification,[status(thm)],[axiom_061])).
% 15.88/2.75 fof(c_0_50, plain, ![X115, X116]:((X116!=X115|step(atom(X116),X115)=eps)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_057])])])).
% 15.88/2.75 fof(c_0_51, plain, ![X70, X71, X72]:(atom(X70)!=x(X71,X72)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_39])])).
% 15.88/2.75 fof(c_0_52, plain, ![X107]:((X107=eps|(X107=x(proj1(X107),proj2(X107))|(X107=y(proj12(X107),proj22(X107))|(X107=star(proj1Star(X107))|~eps2(X107)))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])])).
% 15.88/2.75 fof(c_0_53, plain, ![X1, X2, X6]:(atom(X1)!=y(X2,X6)), inference(fof_simplification,[status(thm)],[axiom_032])).
% 15.88/2.75 fof(c_0_54, plain, ![X1, X2]:(atom(X1)!=star(X2)), inference(fof_simplification,[status(thm)],[axiom_033])).
% 15.88/2.75 fof(c_0_55, plain, ![X1]:(eps!=atom(X1)), inference(fof_simplification,[status(thm)],[axiom_027])).
% 15.88/2.75 fof(c_0_56, plain, ![X59, X60]:(nil4!=x(X59,X60)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_41])])).
% 15.88/2.75 fof(c_0_57, plain, ![X113, X114]:((X113=atom(proj1Atom(X113))|(X113=x(proj1(X113),proj2(X113))|(X113=y(proj12(X113),proj22(X113))|(X113=star(proj1Star(X113))|step(X113,X114)=nil4))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_42])])).
% 15.88/2.75 fof(c_0_58, plain, ![X1, X2]:(nil4!=y(X1,X2)), inference(fof_simplification,[status(thm)],[axiom_025])).
% 15.88/2.75 fof(c_0_59, plain, ![X1]:(nil4!=star(X1)), inference(fof_simplification,[status(thm)],[axiom_026])).
% 15.88/2.75 fof(c_0_60, plain, ![X1]:(nil4!=atom(X1)), inference(fof_simplification,[status(thm)],[axiom_023])).
% 15.88/2.75 cnf(c_0_61, plain, (rec(X1,cons2(X2,nil2))|~eps2(step(X1,X2))), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 15.88/2.75 fof(c_0_62, plain, (~epred2_0<=>![X2]:(~rec(X2,cons2(a,cons2(b,cons2(b,nil2)))))), introduced(definition)).
% 15.88/2.75 cnf(c_0_63, negated_conjecture, (~reck2(X1,cons2(a,cons2(b,cons2(b,nil2))))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 15.88/2.75 cnf(c_0_64, plain, (reck2(y(X1,X2),cons2(X6,X7))|~reck2(X1,nil2)|~rec(X2,cons2(X6,X7))), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 15.88/2.75 cnf(c_0_65, negated_conjecture, (epred1_0|~reck2(X1,nil2)), inference(split_equiv,[status(thm)],[c_0_48])).
% 15.88/2.75 cnf(c_0_66, plain, (reck2(eps,nil2)), inference(split_conjunct,[status(thm)],[axiom_066])).
% 15.88/2.75 fof(c_0_67, plain, ![X125, X126, X127]:((eps2(X126)|step(y(X126,X127),X125)=x(y(step(X126,X125),X127),nil4))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])).
% 15.88/2.75 cnf(c_0_68, plain, (step(atom(X1),X2)=eps|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_50])).
% 15.88/2.75 cnf(c_0_69, plain, (atom(X1)!=x(X2,X6)), inference(split_conjunct,[status(thm)],[c_0_51])).
% 15.88/2.75 cnf(c_0_70, plain, (X1=eps|X1=x(proj1(X1),proj2(X1))|X1=y(proj12(X1),proj22(X1))|X1=star(proj1Star(X1))|~eps2(X1)), inference(split_conjunct,[status(thm)],[c_0_52])).
% 15.88/2.75 fof(c_0_71, plain, ![X73, X74, X75]:(atom(X73)!=y(X74,X75)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_53])])).
% 15.88/2.75 fof(c_0_72, plain, ![X76, X77]:(atom(X76)!=star(X77)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_54])])).
% 15.88/2.75 fof(c_0_73, plain, ![X64]:(eps!=atom(X64)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_55])])).
% 15.88/2.75 cnf(c_0_74, plain, (nil4!=x(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_56])).
% 15.88/2.75 cnf(c_0_75, plain, (X1=atom(proj1Atom(X1))|X1=x(proj1(X1),proj2(X1))|X1=y(proj12(X1),proj22(X1))|X1=star(proj1Star(X1))|step(X1,X2)=nil4), inference(split_conjunct,[status(thm)],[c_0_57])).
% 15.88/2.75 fof(c_0_76, plain, ![X61, X62]:(nil4!=y(X61,X62)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_58])])).
% 15.88/2.75 fof(c_0_77, plain, ![X63]:(nil4!=star(X63)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_59])])).
% 15.88/2.75 fof(c_0_78, plain, ![X58]:(nil4!=atom(X58)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_60])])).
% 15.88/2.75 cnf(c_0_79, plain, (rec(X1,cons2(X2,cons2(X6,nil2)))|~eps2(step(step(X1,X2),X6))), inference(spm,[status(thm)],[c_0_43, c_0_61])).
% 15.88/2.75 cnf(c_0_80, negated_conjecture, (~epred2_0|~epred1_0), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_48]), c_0_62])).
% 15.88/2.75 cnf(c_0_81, negated_conjecture, (epred1_0), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 15.88/2.75 cnf(c_0_82, plain, (eps2(X1)|step(y(X1,X2),X6)=x(y(step(X1,X6),X2),nil4)), inference(split_conjunct,[status(thm)],[c_0_67])).
% 15.88/2.75 cnf(c_0_83, plain, (step(atom(X1),X1)=eps), inference(er,[status(thm)],[c_0_68])).
% 15.88/2.75 cnf(c_0_84, plain, (y(proj12(X1),proj22(X1))=X1|star(proj1Star(X1))=X1|X1=eps|atom(X2)!=X1|~eps2(X1)), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 15.88/2.75 cnf(c_0_85, plain, (atom(X1)!=y(X2,X6)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 15.88/2.75 cnf(c_0_86, plain, (atom(X1)!=star(X2)), inference(split_conjunct,[status(thm)],[c_0_72])).
% 15.88/2.75 cnf(c_0_87, plain, (eps!=atom(X1)), inference(split_conjunct,[status(thm)],[c_0_73])).
% 15.88/2.75 fof(c_0_88, plain, ![X119, X120, X121]:(step(x(X120,X121),X119)=x(step(X120,X119),step(X121,X119))), inference(variable_rename,[status(thm)],[axiom_059])).
% 15.88/2.75 cnf(c_0_89, plain, (y(proj12(X1),proj22(X1))=X1|step(X1,X2)=nil4|star(proj1Star(X1))=X1|atom(proj1Atom(X1))=X1|X1!=nil4), inference(spm,[status(thm)],[c_0_74, c_0_75])).
% 15.88/2.75 cnf(c_0_90, plain, (nil4!=y(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_76])).
% 15.88/2.75 cnf(c_0_91, plain, (nil4!=star(X1)), inference(split_conjunct,[status(thm)],[c_0_77])).
% 15.88/2.75 cnf(c_0_92, plain, (nil4!=atom(X1)), inference(split_conjunct,[status(thm)],[c_0_78])).
% 15.88/2.75 cnf(c_0_93, negated_conjecture, (epred2_0|~rec(X1,cons2(a,cons2(b,cons2(b,nil2))))), inference(split_equiv,[status(thm)],[c_0_62])).
% 15.88/2.75 cnf(c_0_94, plain, (rec(X1,cons2(X2,cons2(X6,cons2(X7,nil2))))|~eps2(step(step(step(X1,X2),X6),X7))), inference(spm,[status(thm)],[c_0_43, c_0_79])).
% 15.88/2.75 cnf(c_0_95, negated_conjecture, (~epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_80, c_0_81])])).
% 15.88/2.75 cnf(c_0_96, plain, (step(y(atom(X1),X2),X1)=x(y(eps,X2),nil4)|eps2(atom(X1))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 15.88/2.75 cnf(c_0_97, plain, (~eps2(atom(X1))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_84]), c_0_85]), c_0_86]), c_0_87])).
% 15.88/2.75 cnf(c_0_98, plain, (step(x(X1,X2),X6)=x(step(X1,X6),step(X2,X6))), inference(split_conjunct,[status(thm)],[c_0_88])).
% 15.88/2.75 cnf(c_0_99, plain, (step(nil4,X1)=nil4), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_89]), c_0_90]), c_0_91]), c_0_92])).
% 15.88/2.75 fof(c_0_100, plain, ![X108, X109]:(((~eps2(x(X108,X109))|(eps2(X108)|eps2(X109)))&((~eps2(X108)|eps2(x(X108,X109)))&(~eps2(X109)|eps2(x(X108,X109)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_053])])])])).
% 15.88/2.75 cnf(c_0_101, negated_conjecture, (~eps2(step(step(step(X1,a),b),b))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_94]), c_0_95])).
% 15.88/2.75 cnf(c_0_102, plain, (step(y(atom(X1),X2),X1)=x(y(eps,X2),nil4)), inference(sr,[status(thm)],[c_0_96, c_0_97])).
% 15.88/2.75 cnf(c_0_103, plain, (step(x(X1,nil4),X2)=x(step(X1,X2),nil4)), inference(spm,[status(thm)],[c_0_98, c_0_99])).
% 15.88/2.75 cnf(c_0_104, plain, (eps2(x(X2,X1))|~eps2(X1)), inference(split_conjunct,[status(thm)],[c_0_100])).
% 15.88/2.75 fof(c_0_105, plain, ![X122, X123, X124]:((~eps2(X123)|step(y(X123,X124),X122)=x(y(step(X123,X122),X124),step(X124,X122)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_060])])])).
% 15.88/2.75 cnf(c_0_106, negated_conjecture, (~eps2(x(step(step(y(eps,X1),b),b),nil4))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_102]), c_0_103]), c_0_103])).
% 15.88/2.75 cnf(c_0_107, plain, (eps2(x(X1,X2))|~eps2(X1)), inference(split_conjunct,[status(thm)],[c_0_100])).
% 15.88/2.75 cnf(c_0_108, plain, (eps2(step(x(X1,X2),X6))|~eps2(step(X2,X6))), inference(spm,[status(thm)],[c_0_104, c_0_98])).
% 15.88/2.75 cnf(c_0_109, plain, (step(y(X1,X2),X6)=x(y(step(X1,X6),X2),step(X2,X6))|~eps2(X1)), inference(split_conjunct,[status(thm)],[c_0_105])).
% 15.88/2.75 fof(c_0_110, plain, ![X128, X129]:(step(star(X129),X128)=y(step(X129,X128),star(X129))), inference(variable_rename,[status(thm)],[axiom_062])).
% 15.88/2.75 fof(c_0_111, plain, ![X110, X111]:((((eps2(X110)|~eps2(y(X110,X111)))&(eps2(X111)|~eps2(y(X110,X111))))&(~eps2(X110)|~eps2(X111)|eps2(y(X110,X111))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_054])])])])).
% 15.88/2.75 fof(c_0_112, plain, ![X112]:(eps2(star(X112))), inference(variable_rename,[status(thm)],[axiom_055])).
% 15.88/2.75 cnf(c_0_113, negated_conjecture, (~eps2(step(step(y(eps,X1),b),b))), inference(spm,[status(thm)],[c_0_106, c_0_107])).
% 15.88/2.75 cnf(c_0_114, plain, (eps2(step(step(y(X1,X2),X6),X7))|~eps2(step(step(X2,X6),X7))|~eps2(X1)), inference(spm,[status(thm)],[c_0_108, c_0_109])).
% 15.88/2.75 cnf(c_0_115, plain, (eps2(eps)), inference(split_conjunct,[status(thm)],[axiom_052])).
% 15.88/2.75 cnf(c_0_116, plain, (step(star(X1),X2)=y(step(X1,X2),star(X1))), inference(split_conjunct,[status(thm)],[c_0_110])).
% 15.88/2.75 cnf(c_0_117, plain, (eps2(y(X1,X2))|~eps2(X1)|~eps2(X2)), inference(split_conjunct,[status(thm)],[c_0_111])).
% 15.88/2.75 cnf(c_0_118, plain, (eps2(star(X1))), inference(split_conjunct,[status(thm)],[c_0_112])).
% 15.88/2.75 cnf(c_0_119, negated_conjecture, (~eps2(step(step(X1,b),b))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_114]), c_0_115])])).
% 15.88/2.75 cnf(c_0_120, plain, (step(star(atom(X1)),X1)=y(eps,star(atom(X1)))), inference(spm,[status(thm)],[c_0_116, c_0_83])).
% 15.88/2.75 cnf(c_0_121, plain, (eps2(step(star(X1),X2))|~eps2(step(X1,X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_116]), c_0_118])])).
% 15.88/2.75 cnf(c_0_122, negated_conjecture, (~eps2(step(y(eps,star(atom(b))),b))), inference(spm,[status(thm)],[c_0_119, c_0_120])).
% 15.88/2.75 cnf(c_0_123, plain, (eps2(step(y(X1,X2),X6))|~eps2(step(X2,X6))|~eps2(X1)), inference(spm,[status(thm)],[c_0_104, c_0_109])).
% 15.88/2.75 cnf(c_0_124, plain, (eps2(y(eps,star(atom(X1))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_120]), c_0_83]), c_0_115])])).
% 15.88/2.75 cnf(c_0_125, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_123]), c_0_120]), c_0_124]), c_0_115])]), ['proof']).
% 15.88/2.75 % SZS output end CNFRefutation
% 15.88/2.75 % Parsed axioms : 77
% 15.88/2.75 % Removed by relevancy pruning/SinE : 0
% 15.88/2.75 % Initial clauses : 94
% 15.88/2.75 % Removed in clause preprocessing : 1
% 15.88/2.75 % Initial clauses in saturation : 93
% 15.88/2.75 % Processed clauses : 3536
% 15.88/2.75 % ...of these trivial : 302
% 15.88/2.75 % ...subsumed : 1907
% 15.88/2.75 % ...remaining for further processing : 1327
% 15.88/2.75 % Other redundant clauses eliminated : 1595
% 15.88/2.75 % Clauses deleted for lack of memory : 0
% 15.88/2.75 % Backward-subsumed : 95
% 15.88/2.75 % Backward-rewritten : 212
% 15.88/2.75 % Generated clauses : 159024
% 15.88/2.75 % ...of the previous two non-redundant : 152295
% 15.88/2.75 % ...aggressively subsumed : 0
% 15.88/2.75 % Contextual simplify-reflections : 56
% 15.88/2.75 % Paramodulations : 157262
% 15.88/2.75 % Factorizations : 0
% 15.88/2.75 % NegExts : 0
% 15.88/2.75 % Equation resolutions : 1757
% 15.88/2.75 % Disequality decompositions : 0
% 15.88/2.75 % Total rewrite steps : 20204
% 15.88/2.75 % ...of those cached : 16924
% 15.88/2.75 % Propositional unsat checks : 0
% 15.88/2.75 % Propositional check models : 0
% 15.88/2.75 % Propositional check unsatisfiable : 0
% 15.88/2.75 % Propositional clauses : 0
% 15.88/2.75 % Propositional clauses after purity: 0
% 15.88/2.75 % Propositional unsat core size : 0
% 15.88/2.75 % Propositional preprocessing time : 0.000
% 15.88/2.75 % Propositional encoding time : 0.000
% 15.88/2.75 % Propositional solver time : 0.000
% 15.88/2.75 % Success case prop preproc time : 0.000
% 15.88/2.75 % Success case prop encoding time : 0.000
% 15.88/2.75 % Success case prop solver time : 0.000
% 15.88/2.75 % Current number of processed clauses : 922
% 15.88/2.75 % Positive orientable unit clauses : 368
% 15.88/2.75 % Positive unorientable unit clauses: 0
% 15.88/2.75 % Negative unit clauses : 145
% 15.88/2.75 % Non-unit-clauses : 409
% 15.88/2.75 % Current number of unprocessed clauses: 138873
% 15.88/2.75 % ...number of literals in the above : 373128
% 15.88/2.75 % Current number of archived formulas : 0
% 15.88/2.75 % Current number of archived clauses : 402
% 15.88/2.75 % Clause-clause subsumption calls (NU) : 17042
% 15.88/2.75 % Rec. Clause-clause subsumption calls : 11074
% 15.88/2.75 % Non-unit clause-clause subsumptions : 485
% 15.88/2.75 % Unit Clause-clause subsumption calls : 13838
% 15.88/2.75 % Rewrite failures with RHS unbound : 0
% 15.88/2.75 % BW rewrite match attempts : 6995
% 15.88/2.75 % BW rewrite match successes : 180
% 15.88/2.75 % Condensation attempts : 0
% 15.88/2.75 % Condensation successes : 0
% 15.88/2.75 % Termbank termtop insertions : 2184789
% 15.88/2.75 % Search garbage collected termcells : 647
% 15.88/2.75
% 15.88/2.75 % -------------------------------------------------
% 15.88/2.75 % User time : 2.162 s
% 15.88/2.75 % System time : 0.092 s
% 15.88/2.75 % Total time : 2.254 s
% 15.88/2.75 % Maximum resident set size: 3460 pages
% 15.88/2.75
% 15.88/2.75 % -------------------------------------------------
% 15.88/2.75 % User time : 10.827 s
% 15.88/2.75 % System time : 0.522 s
% 15.88/2.75 % Total time : 11.349 s
% 15.88/2.75 % Maximum resident set size: 4864 pages
% 15.88/2.75 % E exiting
%------------------------------------------------------------------------------