%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL875-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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 : Fri Sep 25 02:08:36 PM UTC 2026
% Result : Unsatisfiable 14.94s 2.82s
% Output : CNFRefutation 14.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 51
% Syntax : Number of formulae : 167 ( 136 unt; 45 def)
% Number of atoms : 563 ( 45 equ)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 74 ( 40 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 48 ( 46 usr; 46 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 23 con; 0-2 aty)
% Number of variables : 59 ( 0 sgn 59 !; 0 ?; 48 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b) ).
fof(f3,axiom,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c) ).
fof(f4,axiom,
! [X0] : is_a_theorem(implies(X0,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i) ).
fof(f5,axiom,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',w) ).
fof(f6,negated_conjecture,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_rezus) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_58,plain,
! [X0: $i] : is_a_theorem(implies(X0,X0)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),
inference(cnf_transformation,[],[f5]) ).
tcf(c_60,negated_conjecture,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
inference(cnf_transformation,[],[f6]) ).
tcf(c_81,definition,
iPr_def_10 = implies(y,y),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_82,definition,
iPr_def_11 = implies(z,z),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_83,definition,
iPr_def_12 = implies(u,u),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_84,definition,
iPr_def_13 = implies(v,v),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_85,definition,
iPr_def_14 = implies(x,w),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_86,definition,
iPr_def_15 = implies(iPr_def_13,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_87,definition,
iPr_def_16 = implies(iPr_def_12,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_88,definition,
iPr_def_17 = implies(iPr_def_11,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_89,definition,
iPr_def_18 = implies(iPr_def_10,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_90,definition,
iPr_def_19 = implies(iPr_def_18,w),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_91,definition,
iPr_def_20 = implies(x,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_92,definition,
iPr_def_21 = implies(v6,v7),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_93,definition,
iPr_def_22 = implies(v7,v8),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_94,definition,
iPr_def_23 = implies(v6,v8),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_95,definition,
iPr_def_24 = implies(iPr_def_22,iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_96,definition,
iPr_def_25 = implies(iPr_def_21,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_97,definition,
iPr_def_26 = implies(v9,v10),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_98,definition,
iPr_def_27 = implies(v9,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_99,definition,
iPr_def_28 = implies(iPr_def_27,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_100,definition,
iPr_def_29 = implies(v11,v12),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_101,definition,
iPr_def_30 = implies(v12,v13),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_102,definition,
iPr_def_31 = implies(v11,v13),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_103,definition,
iPr_def_32 = implies(iPr_def_30,iPr_def_31),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_104,definition,
iPr_def_33 = implies(iPr_def_29,iPr_def_32),
introduced(definition,[new_symbols(definition,[iPr_def_33])],[]) ).
tcf(c_105,definition,
iPr_def_34 = implies(iPr_def_33,v14),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_106,definition,
iPr_def_35 = implies(iPr_def_28,iPr_def_34),
introduced(definition,[new_symbols(definition,[iPr_def_35])],[]) ).
tcf(c_107,definition,
iPr_def_36 = implies(iPr_def_35,v14),
introduced(definition,[new_symbols(definition,[iPr_def_36])],[]) ).
tcf(c_108,definition,
iPr_def_37 = implies(iPr_def_36,v15),
introduced(definition,[new_symbols(definition,[iPr_def_37])],[]) ).
tcf(c_109,definition,
iPr_def_38 = implies(iPr_def_25,iPr_def_37),
introduced(definition,[new_symbols(definition,[iPr_def_38])],[]) ).
tcf(c_110,definition,
iPr_def_39 = implies(iPr_def_38,v15),
introduced(definition,[new_symbols(definition,[iPr_def_39])],[]) ).
tcf(c_111,definition,
iPr_def_40 = implies(v17,v17),
introduced(definition,[new_symbols(definition,[iPr_def_40])],[]) ).
tcf(c_112,definition,
iPr_def_41 = implies(v18,v18),
introduced(definition,[new_symbols(definition,[iPr_def_41])],[]) ).
tcf(c_113,definition,
iPr_def_42 = implies(v19,v19),
introduced(definition,[new_symbols(definition,[iPr_def_42])],[]) ).
tcf(c_114,definition,
iPr_def_43 = implies(v20,v20),
introduced(definition,[new_symbols(definition,[iPr_def_43])],[]) ).
tcf(c_115,definition,
iPr_def_44 = implies(v16,v21),
introduced(definition,[new_symbols(definition,[iPr_def_44])],[]) ).
tcf(c_116,definition,
iPr_def_45 = implies(iPr_def_43,iPr_def_44),
introduced(definition,[new_symbols(definition,[iPr_def_45])],[]) ).
tcf(c_117,definition,
iPr_def_46 = implies(iPr_def_42,iPr_def_45),
introduced(definition,[new_symbols(definition,[iPr_def_46])],[]) ).
tcf(c_118,definition,
iPr_def_47 = implies(iPr_def_41,iPr_def_46),
introduced(definition,[new_symbols(definition,[iPr_def_47])],[]) ).
tcf(c_119,definition,
iPr_def_48 = implies(iPr_def_40,iPr_def_47),
introduced(definition,[new_symbols(definition,[iPr_def_48])],[]) ).
tcf(c_120,definition,
iPr_def_49 = implies(iPr_def_48,v21),
introduced(definition,[new_symbols(definition,[iPr_def_49])],[]) ).
tcf(c_121,definition,
iPr_def_50 = implies(v16,iPr_def_49),
introduced(definition,[new_symbols(definition,[iPr_def_50])],[]) ).
tcf(c_122,definition,
iPr_def_51 = implies(iPr_def_50,v22),
introduced(definition,[new_symbols(definition,[iPr_def_51])],[]) ).
tcf(c_123,definition,
iPr_def_52 = implies(iPr_def_39,iPr_def_51),
introduced(definition,[new_symbols(definition,[iPr_def_52])],[]) ).
tcf(c_124,definition,
iPr_def_53 = implies(iPr_def_20,iPr_def_52),
introduced(definition,[new_symbols(definition,[iPr_def_53])],[]) ).
tcf(c_125,definition,
iPr_def_54 = implies(iPr_def_53,v22),
introduced(definition,[new_symbols(definition,[iPr_def_54])],[]) ).
tcf(c_126,negated_conjecture,
~ is_a_theorem(iPr_def_54),
inference(demodulation,[status(thm)],[c_60,c_115,c_114,c_116,c_113,c_117,c_112,c_118,c_111,c_119,c_120,c_121,c_122,c_102,c_101,c_103,c_100,c_104,c_105,c_97,c_98,c_99,c_106,c_107,c_108,c_94,c_93,c_95,c_92,c_96,c_109,c_110,c_123,c_85,c_84,c_86,c_83,c_87,c_82,c_88,c_81,c_89,c_90,c_91,c_124,c_125]) ).
tcf(c_389,plain,
is_a_theorem(iPr_def_10),
inference(superposition,[status(thm)],[c_81,c_58]) ).
tcf(c_390,plain,
is_a_theorem(iPr_def_11),
inference(superposition,[status(thm)],[c_82,c_58]) ).
tcf(c_391,plain,
is_a_theorem(iPr_def_12),
inference(superposition,[status(thm)],[c_83,c_58]) ).
tcf(c_392,plain,
is_a_theorem(iPr_def_13),
inference(superposition,[status(thm)],[c_84,c_58]) ).
tcf(c_393,plain,
is_a_theorem(iPr_def_40),
inference(superposition,[status(thm)],[c_111,c_58]) ).
tcf(c_394,plain,
is_a_theorem(iPr_def_41),
inference(superposition,[status(thm)],[c_112,c_58]) ).
tcf(c_395,plain,
is_a_theorem(iPr_def_42),
inference(superposition,[status(thm)],[c_113,c_58]) ).
tcf(c_396,plain,
is_a_theorem(iPr_def_43),
inference(superposition,[status(thm)],[c_114,c_58]) ).
tcf(c_625,plain,
is_a_theorem(implies(implies(v9,iPr_def_26),iPr_def_26)),
inference(superposition,[status(thm)],[c_97,c_59]) ).
tcf(c_663,plain,
is_a_theorem(iPr_def_28),
inference(light_normalisation,[status(thm)],[c_625,c_98,c_99]) ).
tcf(c_734,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_22,implies(implies(X0,v7),implies(X0,v8)))),
inference(superposition,[status(thm)],[c_93,c_56]) ).
tcf(c_738,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_30,implies(implies(X0,v12),implies(X0,v13)))),
inference(superposition,[status(thm)],[c_101,c_56]) ).
tcf(c_1382,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_14),implies(x,implies(X0,w)))),
inference(superposition,[status(thm)],[c_85,c_57]) ).
tcf(c_1394,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_44),implies(v16,implies(X0,v21)))),
inference(superposition,[status(thm)],[c_115,c_57]) ).
tcf(c_1395,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_15),implies(iPr_def_13,implies(X0,iPr_def_14)))),
inference(superposition,[status(thm)],[c_86,c_57]) ).
tcf(c_1396,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_16),implies(iPr_def_12,implies(X0,iPr_def_15)))),
inference(superposition,[status(thm)],[c_87,c_57]) ).
tcf(c_1397,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_17),implies(iPr_def_11,implies(X0,iPr_def_16)))),
inference(superposition,[status(thm)],[c_88,c_57]) ).
tcf(c_1407,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_34),implies(iPr_def_33,implies(X0,v14)))),
inference(superposition,[status(thm)],[c_105,c_57]) ).
tcf(c_1410,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_37),implies(iPr_def_36,implies(X0,v15)))),
inference(superposition,[status(thm)],[c_108,c_57]) ).
tcf(c_1413,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_45),implies(iPr_def_43,implies(X0,iPr_def_44)))),
inference(superposition,[status(thm)],[c_116,c_57]) ).
tcf(c_1414,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_46),implies(iPr_def_42,implies(X0,iPr_def_45)))),
inference(superposition,[status(thm)],[c_117,c_57]) ).
tcf(c_1415,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_47),implies(iPr_def_41,implies(X0,iPr_def_46)))),
inference(superposition,[status(thm)],[c_118,c_57]) ).
tcf(c_1419,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_51),implies(iPr_def_50,implies(X0,v22)))),
inference(superposition,[status(thm)],[c_122,c_57]) ).
tcf(c_1420,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_52),implies(iPr_def_39,implies(X0,iPr_def_51)))),
inference(superposition,[status(thm)],[c_123,c_57]) ).
tcf(c_1446,plain,
! [X0: $i] : is_a_theorem(implies(implies(iPr_def_22,implies(X0,iPr_def_23)),implies(X0,iPr_def_24))),
inference(superposition,[status(thm)],[c_95,c_57]) ).
tcf(c_1450,plain,
! [X0: $i] : is_a_theorem(implies(implies(iPr_def_30,implies(X0,iPr_def_31)),implies(X0,iPr_def_32))),
inference(superposition,[status(thm)],[c_103,c_57]) ).
tcf(c_1468,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(implies(X1,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(superposition,[status(thm)],[c_57,c_55]) ).
tcf(c_2428,plain,
is_a_theorem(implies(iPr_def_22,implies(implies(v6,v7),iPr_def_23))),
inference(superposition,[status(thm)],[c_94,c_734]) ).
tcf(c_2430,plain,
is_a_theorem(implies(iPr_def_22,implies(iPr_def_21,iPr_def_23))),
inference(light_normalisation,[status(thm)],[c_2428,c_92]) ).
tcf(c_2561,plain,
is_a_theorem(implies(iPr_def_30,implies(implies(v11,v12),iPr_def_31))),
inference(superposition,[status(thm)],[c_102,c_738]) ).
tcf(c_2563,plain,
is_a_theorem(implies(iPr_def_30,implies(iPr_def_29,iPr_def_31))),
inference(light_normalisation,[status(thm)],[c_2561,c_100]) ).
tcf(c_4483,plain,
is_a_theorem(implies(implies(iPr_def_18,iPr_def_14),implies(x,iPr_def_19))),
inference(superposition,[status(thm)],[c_90,c_1382]) ).
tcf(c_4485,plain,
is_a_theorem(implies(implies(iPr_def_18,iPr_def_14),iPr_def_20)),
inference(light_normalisation,[status(thm)],[c_4483,c_91]) ).
tcf(c_4489,plain,
( is_a_theorem(iPr_def_20)
| ~ is_a_theorem(implies(iPr_def_18,iPr_def_14)) ),
inference(superposition,[status(thm)],[c_4485,c_55]) ).
tcf(c_4643,plain,
is_a_theorem(implies(implies(iPr_def_48,iPr_def_44),implies(v16,iPr_def_49))),
inference(superposition,[status(thm)],[c_120,c_1394]) ).
tcf(c_4645,plain,
is_a_theorem(implies(implies(iPr_def_48,iPr_def_44),iPr_def_50)),
inference(light_normalisation,[status(thm)],[c_4643,c_121]) ).
tcf(c_4649,plain,
( is_a_theorem(iPr_def_50)
| ~ is_a_theorem(implies(iPr_def_48,iPr_def_44)) ),
inference(superposition,[status(thm)],[c_4645,c_55]) ).
tcf(c_4739,plain,
is_a_theorem(implies(iPr_def_18,implies(iPr_def_11,implies(iPr_def_10,iPr_def_16)))),
inference(superposition,[status(thm)],[c_89,c_1397]) ).
tcf(c_4896,plain,
is_a_theorem(implies(implies(iPr_def_35,iPr_def_34),implies(iPr_def_33,iPr_def_36))),
inference(superposition,[status(thm)],[c_107,c_1407]) ).
tcf(c_4918,plain,
( is_a_theorem(implies(iPr_def_33,iPr_def_36))
| ~ is_a_theorem(implies(iPr_def_35,iPr_def_34)) ),
inference(superposition,[status(thm)],[c_4896,c_55]) ).
tcf(c_4967,plain,
is_a_theorem(implies(implies(iPr_def_38,iPr_def_37),implies(iPr_def_36,iPr_def_39))),
inference(superposition,[status(thm)],[c_110,c_1410]) ).
tcf(c_4982,plain,
( is_a_theorem(implies(iPr_def_36,iPr_def_39))
| ~ is_a_theorem(implies(iPr_def_38,iPr_def_37)) ),
inference(superposition,[status(thm)],[c_4967,c_55]) ).
tcf(c_5108,plain,
is_a_theorem(implies(iPr_def_48,implies(iPr_def_41,implies(iPr_def_40,iPr_def_46)))),
inference(superposition,[status(thm)],[c_119,c_1415]) ).
tcf(c_5204,plain,
is_a_theorem(implies(implies(iPr_def_53,iPr_def_51),implies(iPr_def_50,iPr_def_54))),
inference(superposition,[status(thm)],[c_125,c_1419]) ).
tcf(c_5226,plain,
( is_a_theorem(implies(iPr_def_50,iPr_def_54))
| ~ is_a_theorem(implies(iPr_def_53,iPr_def_51)) ),
inference(superposition,[status(thm)],[c_5204,c_55]) ).
tcf(c_5241,plain,
is_a_theorem(implies(iPr_def_53,implies(iPr_def_39,implies(iPr_def_20,iPr_def_51)))),
inference(superposition,[status(thm)],[c_124,c_1420]) ).
tcf(c_5598,plain,
is_a_theorem(implies(implies(iPr_def_22,implies(iPr_def_21,iPr_def_23)),iPr_def_25)),
inference(superposition,[status(thm)],[c_96,c_1446]) ).
tcf(c_5612,plain,
( is_a_theorem(iPr_def_25)
| ~ is_a_theorem(implies(iPr_def_22,implies(iPr_def_21,iPr_def_23))) ),
inference(superposition,[status(thm)],[c_5598,c_55]) ).
tcf(c_5613,plain,
is_a_theorem(iPr_def_25),
inference(forward_subsumption_resolution,[status(thm)],[c_5612,c_2430]) ).
tcf(c_5656,plain,
is_a_theorem(implies(implies(iPr_def_30,implies(iPr_def_29,iPr_def_31)),iPr_def_33)),
inference(superposition,[status(thm)],[c_104,c_1450]) ).
tcf(c_5661,plain,
( is_a_theorem(iPr_def_33)
| ~ is_a_theorem(implies(iPr_def_30,implies(iPr_def_29,iPr_def_31))) ),
inference(superposition,[status(thm)],[c_5656,c_55]) ).
tcf(c_5662,plain,
is_a_theorem(iPr_def_33),
inference(forward_subsumption_resolution,[status(thm)],[c_5661,c_2563]) ).
tcf(c_6117,plain,
! [X0: $i,X1: $i] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(superposition,[status(thm)],[c_58,c_1468]) ).
tcf(c_6272,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_13,implies(implies(X0,iPr_def_15),implies(X0,iPr_def_14)))),
inference(superposition,[status(thm)],[c_1395,c_1468]) ).
tcf(c_6273,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_12,implies(implies(X0,iPr_def_16),implies(X0,iPr_def_15)))),
inference(superposition,[status(thm)],[c_1396,c_1468]) ).
tcf(c_6290,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_43,implies(implies(X0,iPr_def_45),implies(X0,iPr_def_44)))),
inference(superposition,[status(thm)],[c_1413,c_1468]) ).
tcf(c_6291,plain,
! [X0: $i] : is_a_theorem(implies(iPr_def_42,implies(implies(X0,iPr_def_46),implies(X0,iPr_def_45)))),
inference(superposition,[status(thm)],[c_1414,c_1468]) ).
tcf(c_6469,plain,
is_a_theorem(implies(iPr_def_11,implies(iPr_def_18,implies(iPr_def_10,iPr_def_16)))),
inference(superposition,[status(thm)],[c_4739,c_1468]) ).
tcf(c_6488,plain,
is_a_theorem(implies(iPr_def_41,implies(iPr_def_48,implies(iPr_def_40,iPr_def_46)))),
inference(superposition,[status(thm)],[c_5108,c_1468]) ).
tcf(c_6494,plain,
is_a_theorem(implies(iPr_def_39,implies(iPr_def_53,implies(iPr_def_20,iPr_def_51)))),
inference(superposition,[status(thm)],[c_5241,c_1468]) ).
tcf(c_7519,plain,
is_a_theorem(implies(iPr_def_28,implies(iPr_def_35,iPr_def_34))),
inference(superposition,[status(thm)],[c_106,c_6117]) ).
tcf(c_7522,plain,
is_a_theorem(implies(iPr_def_25,implies(iPr_def_38,iPr_def_37))),
inference(superposition,[status(thm)],[c_109,c_6117]) ).
tcf(c_7830,plain,
( is_a_theorem(implies(iPr_def_35,iPr_def_34))
| ~ is_a_theorem(iPr_def_28) ),
inference(superposition,[status(thm)],[c_7519,c_55]) ).
tcf(c_7833,plain,
is_a_theorem(implies(iPr_def_35,iPr_def_34)),
inference(forward_subsumption_resolution,[status(thm)],[c_7830,c_663]) ).
tcf(c_7834,plain,
is_a_theorem(implies(iPr_def_33,iPr_def_36)),
inference(backward_subsumption_resolution,[status(thm)],[c_4918,c_7833]) ).
tcf(c_7836,plain,
( is_a_theorem(iPr_def_36)
| ~ is_a_theorem(iPr_def_33) ),
inference(superposition,[status(thm)],[c_7834,c_55]) ).
tcf(c_7837,plain,
is_a_theorem(iPr_def_36),
inference(forward_subsumption_resolution,[status(thm)],[c_7836,c_5662]) ).
tcf(c_7867,plain,
( is_a_theorem(implies(iPr_def_38,iPr_def_37))
| ~ is_a_theorem(iPr_def_25) ),
inference(superposition,[status(thm)],[c_7522,c_55]) ).
tcf(c_7870,plain,
is_a_theorem(implies(iPr_def_38,iPr_def_37)),
inference(forward_subsumption_resolution,[status(thm)],[c_7867,c_5613]) ).
tcf(c_7871,plain,
is_a_theorem(implies(iPr_def_36,iPr_def_39)),
inference(backward_subsumption_resolution,[status(thm)],[c_4982,c_7870]) ).
tcf(c_7891,plain,
( is_a_theorem(iPr_def_39)
| ~ is_a_theorem(iPr_def_36) ),
inference(superposition,[status(thm)],[c_7871,c_55]) ).
tcf(c_7892,plain,
is_a_theorem(iPr_def_39),
inference(forward_subsumption_resolution,[status(thm)],[c_7891,c_7837]) ).
tcf(c_9364,plain,
( is_a_theorem(implies(iPr_def_18,implies(iPr_def_10,iPr_def_16)))
| ~ is_a_theorem(iPr_def_11) ),
inference(superposition,[status(thm)],[c_6469,c_55]) ).
tcf(c_9366,plain,
is_a_theorem(implies(iPr_def_18,implies(iPr_def_10,iPr_def_16))),
inference(forward_subsumption_resolution,[status(thm)],[c_9364,c_390]) ).
tcf(c_9374,plain,
is_a_theorem(implies(iPr_def_10,implies(iPr_def_18,iPr_def_16))),
inference(superposition,[status(thm)],[c_9366,c_1468]) ).
tcf(c_9378,plain,
( is_a_theorem(implies(iPr_def_18,iPr_def_16))
| ~ is_a_theorem(iPr_def_10) ),
inference(superposition,[status(thm)],[c_9374,c_55]) ).
tcf(c_9380,plain,
is_a_theorem(implies(iPr_def_18,iPr_def_16)),
inference(forward_subsumption_resolution,[status(thm)],[c_9378,c_389]) ).
tcf(c_9590,plain,
( is_a_theorem(implies(iPr_def_48,implies(iPr_def_40,iPr_def_46)))
| ~ is_a_theorem(iPr_def_41) ),
inference(superposition,[status(thm)],[c_6488,c_55]) ).
tcf(c_9592,plain,
is_a_theorem(implies(iPr_def_48,implies(iPr_def_40,iPr_def_46))),
inference(forward_subsumption_resolution,[status(thm)],[c_9590,c_394]) ).
tcf(c_9594,plain,
is_a_theorem(implies(iPr_def_40,implies(iPr_def_48,iPr_def_46))),
inference(superposition,[status(thm)],[c_9592,c_1468]) ).
tcf(c_9595,plain,
( is_a_theorem(implies(iPr_def_48,iPr_def_46))
| ~ is_a_theorem(iPr_def_40) ),
inference(superposition,[status(thm)],[c_9594,c_55]) ).
tcf(c_9597,plain,
is_a_theorem(implies(iPr_def_48,iPr_def_46)),
inference(forward_subsumption_resolution,[status(thm)],[c_9595,c_393]) ).
tcf(c_9674,plain,
( is_a_theorem(implies(iPr_def_53,implies(iPr_def_20,iPr_def_51)))
| ~ is_a_theorem(iPr_def_39) ),
inference(superposition,[status(thm)],[c_6494,c_55]) ).
tcf(c_9676,plain,
is_a_theorem(implies(iPr_def_53,implies(iPr_def_20,iPr_def_51))),
inference(forward_subsumption_resolution,[status(thm)],[c_9674,c_7892]) ).
tcf(c_9678,plain,
is_a_theorem(implies(iPr_def_20,implies(iPr_def_53,iPr_def_51))),
inference(superposition,[status(thm)],[c_9676,c_1468]) ).
tcf(c_9681,plain,
( is_a_theorem(implies(iPr_def_53,iPr_def_51))
| ~ is_a_theorem(iPr_def_20) ),
inference(superposition,[status(thm)],[c_9678,c_55]) ).
tcf(c_9698,plain,
( is_a_theorem(implies(iPr_def_50,iPr_def_54))
| ~ is_a_theorem(iPr_def_20) ),
inference(superposition,[status(thm)],[c_9681,c_5226]) ).
tcf(c_9708,plain,
( is_a_theorem(iPr_def_54)
| ~ is_a_theorem(iPr_def_50)
| ~ is_a_theorem(iPr_def_20) ),
inference(superposition,[status(thm)],[c_9698,c_55]) ).
tcf(c_9710,plain,
( ~ is_a_theorem(iPr_def_50)
| ~ is_a_theorem(iPr_def_20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9708,c_126]) ).
tcf(c_18310,plain,
! [X0: $i] :
( is_a_theorem(implies(implies(X0,iPr_def_15),implies(X0,iPr_def_14)))
| ~ is_a_theorem(iPr_def_13) ),
inference(superposition,[status(thm)],[c_6272,c_55]) ).
tcf(c_18312,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_15),implies(X0,iPr_def_14))),
inference(forward_subsumption_resolution,[status(thm)],[c_18310,c_392]) ).
tcf(c_18370,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,iPr_def_14))
| ~ is_a_theorem(implies(X0,iPr_def_15)) ),
inference(superposition,[status(thm)],[c_18312,c_55]) ).
tcf(c_18690,plain,
! [X0: $i] :
( is_a_theorem(implies(implies(X0,iPr_def_16),implies(X0,iPr_def_15)))
| ~ is_a_theorem(iPr_def_12) ),
inference(superposition,[status(thm)],[c_6273,c_55]) ).
tcf(c_18692,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_16),implies(X0,iPr_def_15))),
inference(forward_subsumption_resolution,[status(thm)],[c_18690,c_391]) ).
tcf(c_18696,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,iPr_def_15))
| ~ is_a_theorem(implies(X0,iPr_def_16)) ),
inference(superposition,[status(thm)],[c_18692,c_55]) ).
tcf(c_18840,plain,
is_a_theorem(implies(iPr_def_18,iPr_def_15)),
inference(superposition,[status(thm)],[c_9380,c_18696]) ).
tcf(c_18952,plain,
is_a_theorem(implies(iPr_def_18,iPr_def_14)),
inference(superposition,[status(thm)],[c_18840,c_18370]) ).
tcf(c_18956,plain,
is_a_theorem(iPr_def_20),
inference(backward_subsumption_resolution,[status(thm)],[c_4489,c_18952]) ).
tcf(c_18961,plain,
~ is_a_theorem(iPr_def_50),
inference(backward_subsumption_resolution,[status(thm)],[c_9710,c_18956]) ).
tcf(c_18976,plain,
~ is_a_theorem(implies(iPr_def_48,iPr_def_44)),
inference(backward_subsumption_resolution,[status(thm)],[c_4649,c_18961]) ).
tcf(c_24627,plain,
! [X0: $i] :
( is_a_theorem(implies(implies(X0,iPr_def_45),implies(X0,iPr_def_44)))
| ~ is_a_theorem(iPr_def_43) ),
inference(superposition,[status(thm)],[c_6290,c_55]) ).
tcf(c_24629,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_45),implies(X0,iPr_def_44))),
inference(forward_subsumption_resolution,[status(thm)],[c_24627,c_396]) ).
tcf(c_24635,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,iPr_def_44))
| ~ is_a_theorem(implies(X0,iPr_def_45)) ),
inference(superposition,[status(thm)],[c_24629,c_55]) ).
tcf(c_25020,plain,
! [X0: $i] :
( is_a_theorem(implies(implies(X0,iPr_def_46),implies(X0,iPr_def_45)))
| ~ is_a_theorem(iPr_def_42) ),
inference(superposition,[status(thm)],[c_6291,c_55]) ).
tcf(c_25022,plain,
! [X0: $i] : is_a_theorem(implies(implies(X0,iPr_def_46),implies(X0,iPr_def_45))),
inference(forward_subsumption_resolution,[status(thm)],[c_25020,c_395]) ).
tcf(c_25026,plain,
! [X0: $i] :
( is_a_theorem(implies(X0,iPr_def_45))
| ~ is_a_theorem(implies(X0,iPr_def_46)) ),
inference(superposition,[status(thm)],[c_25022,c_55]) ).
tcf(c_25160,plain,
is_a_theorem(implies(iPr_def_48,iPr_def_45)),
inference(superposition,[status(thm)],[c_9597,c_25026]) ).
tcf(c_25270,plain,
is_a_theorem(implies(iPr_def_48,iPr_def_44)),
inference(superposition,[status(thm)],[c_25160,c_24635]) ).
tcf(c_25271,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_25270,c_18976]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL875-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n008.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 00:38:54 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.42
% 0.13/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.42
% 0.13/0.42 % Detected problem language: tptp
% 0.13/0.43 % Proving...
% 14.94/2.82 % SZS status Started for theBenchmark.p
% 14.94/2.82 % SZS status Unsatisfiable for theBenchmark.p
% 14.94/2.82
% 14.94/2.82 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.94/2.82
% 14.94/2.82 % ------ iProver source info
% 14.94/2.82
% 14.94/2.82 % git: date: 2026-07-19 20:42:38 +0200
% 14.94/2.82 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.94/2.82 % git: non_committed_changes: false
% 14.94/2.82
% 14.94/2.82 % ------ Parsing...% successful
% 14.94/2.82
% 14.94/2.82
% 14.94/2.82 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.94/2.82
% 14.94/2.82 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 14.94/2.82
% 14.94/2.82 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 14.94/2.82
% 14.94/2.82 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 14.94/2.82 % ------ Proving...
% 14.94/2.82 % ------ Problem Properties
% 14.94/2.82
% 14.94/2.82 %
% 14.94/2.82 % clauses 51
% 14.94/2.82 % conjectures 1
% 14.94/2.82 % EPR 1
% 14.94/2.82 % Horn 51
% 14.94/2.82 % unary 50
% 14.94/2.82 % binary 0
% 14.94/2.82 % lits 53
% 14.94/2.82 % lits eq 45
% 14.94/2.82 % fd_pure 0
% 14.94/2.82 % fd_pseudo 0
% 14.94/2.82 % fd_cond 0
% 14.94/2.82 % fd_pseudo_cond 0
% 14.94/2.82 % AC symbols 0
% 14.94/2.82
% 14.94/2.82 % ------ Schedule dynamic 5 is on
% 14.94/2.82
% 14.94/2.82 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 14.94/2.82
% 14.94/2.82
% 14.94/2.82 % ------
% 14.94/2.82 % Current options:
% 14.94/2.82 % ------
% 14.94/2.82
% 14.94/2.82
% 14.94/2.82 %
% 14.94/2.82
% 14.94/2.82 % ------ Proving...
% 14.94/2.82 %
% 14.94/2.82
% 14.94/2.82 % SZS status Unsatisfiable for theBenchmark.p
% 14.94/2.82
% 14.94/2.82 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.94/2.83
% 14.94/2.83
%------------------------------------------------------------------------------