%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL649+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n018.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 : Mon Sep 7 03:00:24 PM UTC 2026
% Result : CounterSatisfiable 0.11s 0.44s
% Output : Model 0.11s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(p504_type,type,
p504: $i > $o ).
tff(p602_type,type,
p602: $i > $o ).
tff(p205_type,type,
p205: $i > $o ).
tff(p301_type,type,
p301: $i > $o ).
tff(p303_type,type,
p303: $i > $o ).
tff(p405_type,type,
p405: $i > $o ).
tff(p604_type,type,
p604: $i > $o ).
tff(p605_type,type,
p605: $i > $o ).
tff(p203_type,type,
p203: $i > $o ).
tff(r1_type,type,
r1: ( $i * $i ) > $o ).
tff(p403_type,type,
p403: $i > $o ).
tff(p505_type,type,
p505: $i > $o ).
tff(p202_type,type,
p202: $i > $o ).
tff(p503_type,type,
p503: $i > $o ).
tff(p404_type,type,
p404: $i > $o ).
tff(p501_type,type,
p501: $i > $o ).
tff(p402_type,type,
p402: $i > $o ).
tff(p302_type,type,
p302: $i > $o ).
tff(p401_type,type,
p401: $i > $o ).
tff(p104_type,type,
p104: $i > $o ).
tff(p502_type,type,
p502: $i > $o ).
tff(p601_type,type,
p601: $i > $o ).
tff(p201_type,type,
p201: $i > $o ).
tff(p101_type,type,
p101: $i > $o ).
tff(p603_type,type,
p603: $i > $o ).
tff(p305_type,type,
p305: $i > $o ).
tff(p105_type,type,
p105: $i > $o ).
tff(p103_type,type,
p103: $i > $o ).
tff(p204_type,type,
p204: $i > $o ).
tff(p102_type,type,
p102: $i > $o ).
tff(p304_type,type,
p304: $i > $o ).
tff(formula1,axiom,
! [X0: $i] :
( p504(X0)
<=> $true ) ).
tff(formula2,axiom,
! [X0: $i] :
( p602(X0)
<=> $false ) ).
tff(formula3,axiom,
! [X0: $i] :
( p205(X0)
<=> $false ) ).
tff(formula4,axiom,
! [X0: $i] :
( p301(X0)
<=> $false ) ).
tff(formula5,axiom,
! [X0: $i] :
( p303(X0)
<=> $true ) ).
tff(formula6,axiom,
! [X0: $i] :
( p405(X0)
<=> $false ) ).
tff(formula7,axiom,
! [X0: $i] :
( p604(X0)
<=> $false ) ).
tff(formula8,axiom,
! [X0: $i] :
( p605(X0)
<=> $true ) ).
tff(formula9,axiom,
! [X0: $i] :
( p203(X0)
<=> $false ) ).
tff(formula10,axiom,
! [X0: $i,X1: $i] :
( r1(X0,X1)
<=> $true ) ).
tff(formula11,axiom,
! [X0: $i] :
( p403(X0)
<=> $false ) ).
tff(formula12,axiom,
! [X0: $i] :
( p505(X0)
<=> $false ) ).
tff(formula13,axiom,
! [X0: $i] :
( p202(X0)
<=> $true ) ).
tff(formula14,axiom,
! [X0: $i] :
( p503(X0)
<=> $false ) ).
tff(formula15,axiom,
! [X0: $i] :
( p404(X0)
<=> $true ) ).
tff(formula16,axiom,
! [X0: $i] :
( p501(X0)
<=> $false ) ).
tff(formula17,axiom,
! [X0: $i] :
( p402(X0)
<=> $false ) ).
tff(formula18,axiom,
! [X0: $i] :
( p302(X0)
<=> $false ) ).
tff(formula19,axiom,
! [X0: $i] :
( p401(X0)
<=> $false ) ).
tff(formula20,axiom,
! [X0: $i] :
( p104(X0)
<=> $false ) ).
tff(formula21,axiom,
! [X0: $i] :
( p502(X0)
<=> $false ) ).
tff(formula22,axiom,
! [X0: $i] :
( p601(X0)
<=> $false ) ).
tff(formula23,axiom,
! [X0: $i] :
( p201(X0)
<=> $false ) ).
tff(formula24,axiom,
! [X0: $i] :
( p101(X0)
<=> $true ) ).
tff(formula25,axiom,
! [X0: $i] :
( p603(X0)
<=> $false ) ).
tff(formula26,axiom,
! [X0: $i] :
( p305(X0)
<=> $false ) ).
tff(formula27,axiom,
! [X0: $i] :
( p105(X0)
<=> $false ) ).
tff(formula28,axiom,
! [X0: $i] :
( p103(X0)
<=> $false ) ).
tff(formula29,axiom,
! [X0: $i] :
( p204(X0)
<=> $false ) ).
tff(formula30,axiom,
! [X0: $i] :
( p102(X0)
<=> $false ) ).
tff(formula31,axiom,
! [X0: $i] :
( p304(X0)
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.11/0.36 % Computer : n018.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 : Sat Sep 5 15:02:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.44 % SZS status CounterSatisfiable
% 0.11/0.44 % SZS output start Model
% See solution above
% 0.11/0.45 % E exiting
%------------------------------------------------------------------------------