%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL020-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p 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 : Fri Sep 25 02:05:26 PM UTC 2026
% Result : Unsatisfiable 116.76s 22.54s
% Output : CNFRefutation 116.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 3
% Syntax : Number of formulae : 136 ( 38 unt; 0 def)
% Number of atoms : 293 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 316 ( 159 ~; 157 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 371 ( 0 sgn 371 !; 0 ?; 366 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xhk) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(a,equivalent(equivalent(b,equivalent(c,a)),equivalent(c,b)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_xgk) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_54,negated_conjecture,
~ is_a_theorem(equivalent(a,equivalent(equivalent(b,equivalent(c,a)),equivalent(c,b)))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_81,c_52]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_82,c_52]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X3,X2),X1)))) ),
inference(superposition,[status(thm)],[c_53,c_83]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_121,c_52]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1)) ),
inference(superposition,[status(thm)],[c_121,c_84]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_122,c_134]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_146]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_189,c_52]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_189,c_152]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X3,X0))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1)) ),
inference(superposition,[status(thm)],[c_190,c_152]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_189,c_199]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_190,c_199]) ).
tcf(c_223,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X0,X3),X2),X1)),X3))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_204]) ).
tcf(c_224,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X0,X2),X1),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_189,c_204]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X0,X3),X2))))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_205]) ).
tcf(c_349,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_224,c_200]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_349,c_199]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(renaming,[status(thm)],[c_411]) ).
tcf(c_413,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_412]) ).
tcf(c_417,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_224,c_412]) ).
tcf(c_452,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1)) ),
inference(superposition,[status(thm)],[c_284,c_413]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_417,c_412]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_480]) ).
tcf(c_511,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_492,c_413]) ).
tcf(c_554,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X0,X2),X2),X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_223,c_452]) ).
tcf(c_620,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_623,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_349,c_199]) ).
tcf(c_624,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(renaming,[status(thm)],[c_623]) ).
tcf(c_626,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_620,c_624]) ).
tcf(c_667,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_554,c_624]) ).
tcf(c_708,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_667]) ).
tcf(c_852,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_708,c_626]) ).
tcf(c_854,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(superposition,[status(thm)],[c_53,c_852]) ).
tcf(c_2863,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_2866,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_2863,c_52]) ).
tcf(c_2912,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_2863,c_152]) ).
tcf(c_2917,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_2863,c_2912]) ).
tcf(c_3028,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_511]) ).
tcf(c_3035,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_554,c_2912]) ).
tcf(c_3051,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_3035]) ).
tcf(c_3094,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_3051,c_2917]) ).
tcf(c_3096,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(superposition,[status(thm)],[c_53,c_3094]) ).
tcf(c_3113,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X1)) ),
inference(superposition,[status(thm)],[c_3096,c_511]) ).
tcf(c_3135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_2866,c_3028]) ).
tcf(c_4162,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X0)),X1)) ),
inference(superposition,[status(thm)],[c_53,c_3135]) ).
tcf(c_4181,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_2866,c_4162]) ).
tcf(c_4290,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_2863,c_4181]) ).
tcf(c_4719,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_4290]) ).
tcf(c_4750,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_4719,c_52]) ).
tcf(c_4781,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1))) ),
inference(superposition,[status(thm)],[c_4719,c_3113]) ).
tcf(c_4820,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(superposition,[status(thm)],[c_3096,c_4750]) ).
tcf(c_4861,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X2))) ),
inference(superposition,[status(thm)],[c_4820,c_4181]) ).
tcf(c_4923,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X0,X1),X1),X0),X2),X2)),
inference(superposition,[status(thm)],[c_4820,c_4781]) ).
tcf(c_4936,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X1),X0),X2)) ),
inference(superposition,[status(thm)],[c_4923,c_52]) ).
tcf(c_4957,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(equivalent(X0,X0)) ),
inference(superposition,[status(thm)],[c_4923,c_511]) ).
tcf(c_5009,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(equivalent(equivalent(X2,X3),X3),X2),X1),X0))),
inference(superposition,[status(thm)],[c_53,c_4936]) ).
tcf(c_5091,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),X1)),
inference(superposition,[status(thm)],[c_5009,c_4861]) ).
tcf(c_5227,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(equivalent(X0,X0)) ),
inference(superposition,[status(thm)],[c_5091,c_2917]) ).
tcf(c_12639,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_12642,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_12639,c_52]) ).
tcf(c_12716,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_511]) ).
tcf(c_12735,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_12642,c_12716]) ).
tcf(c_12738,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_224,c_12716]) ).
tcf(c_12748,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X1))) ),
inference(superposition,[status(thm)],[c_12639,c_12738]) ).
tcf(c_13671,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X0)),X1)) ),
inference(superposition,[status(thm)],[c_53,c_12735]) ).
tcf(c_13715,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_12642,c_13671]) ).
tcf(c_13756,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_12639,c_13715]) ).
tcf(c_13951,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_13756]) ).
tcf(c_13981,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13951,c_52]) ).
tcf(c_14005,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_13951,c_12748]) ).
tcf(c_14023,plain,
! [X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1)),
inference(global_subsumption_just,[status(thm)],[c_13981,c_854,c_4957]) ).
tcf(c_14024,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(renaming,[status(thm)],[c_14023]) ).
tcf(c_14137,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X2))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X1)) ),
inference(superposition,[status(thm)],[c_14024,c_14005]) ).
tcf(c_249383,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_249386,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_349,c_199]) ).
tcf(c_249387,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(renaming,[status(thm)],[c_249386]) ).
tcf(c_249389,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_249383,c_249387]) ).
tcf(c_249390,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_249383,c_52]) ).
tcf(c_249677,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_511]) ).
tcf(c_249685,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_554,c_249387]) ).
tcf(c_249690,plain,
! [X0: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X2))
| ~ is_a_theorem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_249685,c_708,c_14137]) ).
tcf(c_249691,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(renaming,[status(thm)],[c_249690]) ).
tcf(c_249711,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_249390,c_249677]) ).
tcf(c_249760,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X0)),X1)) ),
inference(superposition,[status(thm)],[c_53,c_249711]) ).
tcf(c_249773,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_249390,c_249760]) ).
tcf(c_249805,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_249691,c_249389]) ).
tcf(c_249807,plain,
! [X1: $i] : is_a_theorem(equivalent(X1,X1)),
inference(global_subsumption_just,[status(thm)],[c_249805,c_854,c_5227]) ).
tcf(c_249808,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(renaming,[status(thm)],[c_249807]) ).
tcf(c_249817,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X1)) ),
inference(superposition,[status(thm)],[c_249808,c_511]) ).
tcf(c_249986,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X0)) ),
inference(superposition,[status(thm)],[c_53,c_249773]) ).
tcf(c_249987,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_249383,c_249773]) ).
tcf(c_250002,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_249390,c_249986]) ).
tcf(c_250098,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_249987]) ).
tcf(c_250120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X0,X3),X2)),X1))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_53,c_250002]) ).
tcf(c_250162,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_250098,c_52]) ).
tcf(c_250177,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1))) ),
inference(superposition,[status(thm)],[c_250098,c_249817]) ).
tcf(c_250187,plain,
! [X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1)),
inference(global_subsumption_just,[status(thm)],[c_250162,c_854,c_4957]) ).
tcf(c_250188,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(renaming,[status(thm)],[c_250187]) ).
tcf(c_250189,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_250188,c_250002]) ).
tcf(c_250228,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X0,X1),X1),X0),X2),X2)),
inference(superposition,[status(thm)],[c_250188,c_250177]) ).
tcf(c_250235,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X1),X0),X2)) ),
inference(superposition,[status(thm)],[c_250228,c_52]) ).
tcf(c_250263,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X0,X1),X1))),
inference(superposition,[status(thm)],[c_249808,c_250189]) ).
tcf(c_250278,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_250263,c_249773]) ).
tcf(c_250296,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0)),X2)),
inference(superposition,[status(thm)],[c_53,c_250278]) ).
tcf(c_250337,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X0),X1)),
inference(superposition,[status(thm)],[c_250296,c_249986]) ).
tcf(c_250412,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X0,X2),X1),X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_250120,c_249986]) ).
tcf(c_250470,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X0)) ),
inference(superposition,[status(thm)],[c_250412,c_250235]) ).
tcf(c_250471,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X0),X1))),
inference(superposition,[status(thm)],[c_250337,c_250278]) ).
tcf(c_251165,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X1))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_250120,c_250470]) ).
tcf(c_251406,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X0,X1),X2)),equivalent(X2,X1))),
inference(superposition,[status(thm)],[c_53,c_251165]) ).
tcf(c_251441,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X1,X0))),
inference(superposition,[status(thm)],[c_250471,c_251165]) ).
tcf(c_251501,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X0),X2))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_251441,c_250002]) ).
tcf(c_251716,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(X0,X1),X2)),X1),X2)),
inference(superposition,[status(thm)],[c_251406,c_251165]) ).
tcf(c_252614,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(equivalent(X1,X0),X2))),X2)),
inference(superposition,[status(thm)],[c_251716,c_251501]) ).
tcf(c_253077,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X2,equivalent(equivalent(X2,X1),X0))))),
inference(superposition,[status(thm)],[c_252614,c_250278]) ).
tcf(c_253113,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(equivalent(X1,X2),X0))),X2)),
inference(superposition,[status(thm)],[c_253077,c_251165]) ).
tcf(c_253158,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X0,X1),equivalent(X1,X2))),X2)),
inference(superposition,[status(thm)],[c_253113,c_249986]) ).
tcf(c_254712,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(X2,X0)),X1)),
inference(superposition,[status(thm)],[c_253158,c_249986]) ).
tcf(c_256414,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X1,X2),X0)),X2)),
inference(superposition,[status(thm)],[c_254712,c_251501]) ).
tcf(c_256514,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))),
inference(superposition,[status(thm)],[c_256414,c_250278]) ).
tcf(c_257039,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X0),X2)),equivalent(X2,X1))),
inference(superposition,[status(thm)],[c_256514,c_251165]) ).
tcf(c_257135,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,equivalent(equivalent(X1,X2),X0)))),
inference(superposition,[status(thm)],[c_257039,c_250278]) ).
tcf(c_257702,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(X2,X1),equivalent(X0,X2))))),
inference(superposition,[status(thm)],[c_257135,c_250189]) ).
tcf(c_259273,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X0),equivalent(X2,X1))),X2)),
inference(superposition,[status(thm)],[c_257702,c_250278]) ).
tcf(c_260370,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X1,X0)),X2)),
inference(superposition,[status(thm)],[c_259273,c_249986]) ).
tcf(c_262017,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1)))),
inference(superposition,[status(thm)],[c_260370,c_250278]) ).
tcf(c_263356,plain,
$false,
inference(superposition,[status(thm)],[c_262017,c_54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL020-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 21:38:14 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.43 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 116.76/22.54 % SZS status Started for theBenchmark.p
% 116.76/22.54 % SZS status Unsatisfiable for theBenchmark.p
% 116.76/22.54
% 116.76/22.54 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 116.76/22.54
% 116.76/22.54 % ------ iProver source info
% 116.76/22.54
% 116.76/22.54 % git: date: 2026-07-19 20:42:38 +0200
% 116.76/22.54 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 116.76/22.54 % git: non_committed_changes: false
% 116.76/22.54
% 116.76/22.54 % ------ Parsing...% successful
% 116.76/22.54
% 116.76/22.54
% 116.76/22.54 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 116.76/22.54
% 116.76/22.54 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 116.76/22.54
% 116.76/22.54 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 116.76/22.54 % ------ Proving...
% 116.76/22.54 % ------ Problem Properties
% 116.76/22.54
% 116.76/22.54 %
% 116.76/22.54 % clauses 3
% 116.76/22.54 % conjectures 1
% 116.76/22.54 % EPR 0
% 116.76/22.54 % Horn 3
% 116.76/22.54 % unary 2
% 116.76/22.54 % binary 0
% 116.76/22.54 % lits 5
% 116.76/22.54 % lits eq 0
% 116.76/22.54 % fd_pure 0
% 116.76/22.54 % fd_pseudo 0
% 116.76/22.54 % fd_cond 0
% 116.76/22.54 % fd_pseudo_cond 0
% 116.76/22.54 % AC symbols 0
% 116.76/22.54
% 116.76/22.54 % ------ Input Options Time Limit: Unbounded
% 116.76/22.54
% 116.76/22.54
% 116.76/22.54 % ------
% 116.76/22.54 % Current options:
% 116.76/22.54 % ------
% 116.76/22.54
% 116.76/22.54
% 116.76/22.54 %
% 116.76/22.54
% 116.76/22.54 % ------ Proving...
% 116.76/22.54 %
% 116.76/22.54
% 116.76/22.54 % SZS status Unsatisfiable for theBenchmark.p
% 116.76/22.54
% 116.76/22.54 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 116.76/22.55
% 116.76/22.55
%------------------------------------------------------------------------------