%------------------------------------------------------------------------------
% File : Leo-III-SAT---1.7.19
% Problem : LCL491+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d SAT
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 1 12:41:23 PM UTC 2025
% Result : Theorem 247.07s 44.66s
% Output : Refutation 247.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 8
% Syntax : Number of formulae : 36 ( 17 unt; 0 typ; 0 def)
% Number of atoms : 59 ( 13 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 221 ( 16 ~; 11 |; 2 &; 182 @)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 48 ( 0 ^; 48 !; 0 ?; 48 :)
% Comments :
%------------------------------------------------------------------------------
thf(or_2_type,type,
or_2: $o ).
thf(op_implies_and_type,type,
op_implies_and: $o ).
thf(op_or_type,type,
op_or: $o ).
thf(and_type,type,
and: $i > $i > $i ).
thf(implies_type,type,
implies: $i > $i > $i ).
thf(or_type,type,
or: $i > $i > $i ).
thf(not_type,type,
not: $i > $i ).
thf(r2_type,type,
r2: $o ).
thf(is_a_theorem_type,type,
is_a_theorem: $i > $o ).
thf(sk54_type,type,
sk54: $i ).
thf(sk55_type,type,
sk55: $i ).
thf(46,axiom,
( or_2
<=> ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_2) ).
thf(156,plain,
( ( or_2
=> ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) ) )
& ( ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) )
=> or_2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(157,plain,
( ~ ( is_a_theorem @ ( implies @ sk55 @ ( or @ sk54 @ sk55 ) ) )
| or_2 ),
inference(cnf,[status(esa)],[156]) ).
thf(14,axiom,
( op_or
=> ! [A: $i,B: $i] :
( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_or) ).
thf(61,plain,
( op_or
=> ! [A: $i,B: $i] :
( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ~ op_or
| ( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ) ),
inference(cnf,[status(esa)],[61]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) )
| ~ op_or ),
inference(lifteq,[status(thm)],[62]) ).
thf(7,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_or) ).
thf(52,plain,
op_or,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(332,plain,
! [B: $i,A: $i] :
( ( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[63,52]) ).
thf(333,plain,
! [B: $i,A: $i] :
( ( or @ A @ B )
= ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(1,conjecture,
or_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_2) ).
thf(2,negated_conjecture,
~ or_2,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(47,plain,
~ or_2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(597,plain,
( ~ ( is_a_theorem @ ( implies @ sk55 @ ( not @ ( and @ ( not @ sk54 ) @ ( not @ sk55 ) ) ) ) )
| $false ),
inference(rewrite,[status(thm)],[157,333,47]) ).
thf(598,plain,
~ ( is_a_theorem @ ( implies @ sk55 @ ( not @ ( and @ ( not @ sk54 ) @ ( not @ sk55 ) ) ) ) ),
inference(simp,[status(thm)],[597]) ).
thf(19,axiom,
( op_implies_and
=> ! [A: $i,B: $i] :
( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_implies_and) ).
thf(70,plain,
( op_implies_and
=> ! [A: $i,B: $i] :
( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ~ op_implies_and
| ( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) )
| ~ op_implies_and ),
inference(lifteq,[status(thm)],[71]) ).
thf(4,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_implies_and) ).
thf(49,plain,
op_implies_and,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(2009,plain,
! [B: $i,A: $i] :
( ( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[72,49]) ).
thf(2010,plain,
! [B: $i,A: $i] :
( ( implies @ A @ B )
= ( not @ ( and @ A @ ( not @ B ) ) ) ),
inference(simp,[status(thm)],[2009]) ).
thf(2013,plain,
~ ( is_a_theorem @ ( not @ ( and @ sk55 @ ( not @ ( not @ ( and @ ( not @ sk54 ) @ ( not @ sk55 ) ) ) ) ) ) ),
inference(rewrite,[status(thm)],[598,2010]) ).
thf(24,axiom,
( r2
<=> ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2) ).
thf(85,plain,
( ( r2
=> ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) ) )
& ( ! [A: $i,B: $i] : ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) )
=> r2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(87,plain,
! [B: $i,A: $i] :
( ~ r2
| ( is_a_theorem @ ( implies @ B @ ( or @ A @ B ) ) ) ),
inference(cnf,[status(esa)],[85]) ).
thf(17,axiom,
r2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',principia_r2) ).
thf(68,plain,
r2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(8016,plain,
! [B: $i,A: $i] :
( ~ $true
| ( is_a_theorem @ ( not @ ( and @ B @ ( not @ ( or @ A @ B ) ) ) ) ) ),
inference(rewrite,[status(thm)],[87,68,2010]) ).
thf(8017,plain,
! [B: $i,A: $i] : ( is_a_theorem @ ( not @ ( and @ B @ ( not @ ( or @ A @ B ) ) ) ) ),
inference(simp,[status(thm)],[8016]) ).
thf(8026,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( is_a_theorem @ ( not @ ( and @ D @ ( not @ ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ) ) ) )
| ( ( or @ A @ B )
!= ( or @ C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[333,8017]) ).
thf(8027,plain,
! [B: $i,A: $i] : ( is_a_theorem @ ( not @ ( and @ B @ ( not @ ( not @ ( and @ ( not @ A ) @ ( not @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[8026:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(8318,plain,
~ $true,
inference(rewrite,[status(thm)],[2013,8027]) ).
thf(8319,plain,
$false,
inference(simp,[status(thm)],[8318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : LCL491+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% 0.06/0.12 % Command : run_Leo-III %s %d SAT
% 0.11/0.33 % Computer : n021.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Sep 30 12:44:24 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.94/0.87 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.34/1.00 % [INFO] Parsing done (123ms).
% 1.34/1.00 % [INFO] Running in sequential loop mode.
% 1.68/1.21 % [INFO] nitpick registered as external prover.
% 1.68/1.21 % [INFO] Scanning for conjecture ...
% 1.87/1.26 % [INFO] Found a conjecture (or negated_conjecture) and 44 axioms. Running axiom selection ...
% 1.97/1.31 % [INFO] Axiom selection finished. Selected 44 axioms (removed 0 axioms).
% 2.21/1.36 % [INFO] Problem is first-order (TPTP FOF).
% 2.31/1.37 % [INFO] Type checking passed.
% 2.31/1.37 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 247.07/44.63 % [INFO] Killing All external provers ...
% 247.07/44.66 % Time passed: 44110ms (effective reasoning time: 43635ms)
% 247.07/44.66 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 247.07/44.66 % Axioms used in derivation (7): principia_r2, hilbert_op_implies_and, hilbert_op_or, op_implies_and, op_or, r2, or_2
% 247.07/44.66 % No. of inferences in proof: 36
% 247.07/44.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 44110 ms resp. 43635 ms w/o parsing
% 247.07/44.68 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 247.07/44.68 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------