%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% 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 : 600s
% DateTime : Thu Jul 21 09:49:50 EDT 2022
% Result : Satisfiable 0.21s 0.47s
% Output : FiniteModel 0.21s
% Verified :
% SZS Type : FiniteModel
% Domain size : 1
% Comments :
%------------------------------------------------------------------------------
% domain size is 1
fof(domain,fi_domain,
! [X] : X = "1" ).
fof(k0,fi_predicates,
! [X1] :
( k0(X1)
<=> $true ) ).
fof(k1,fi_predicates,
! [X1] :
( k1(X1)
<=> $true ) ).
fof(k2,fi_predicates,
! [X1,X2] :
( k2(X1,X2)
<=> $true ) ).
fof(k3,fi_predicates,
! [X1,X2,X3] :
( k3(X1,X2,X3)
<=> $true ) ).
fof(k4,fi_predicates,
! [X1] :
( k4(X1)
<=> $true ) ).
fof(k5,fi_predicates,
! [X1] :
( k5(X1)
<=> $true ) ).
fof(l0,fi_predicates,
! [X1] :
( l0(X1)
<=> $true ) ).
fof(l1,fi_predicates,
! [X1,X2] :
( l1(X1,X2)
<=> $true ) ).
fof(l2,fi_predicates,
! [X1,X2] :
( l2(X1,X2)
<=> $true ) ).
fof(l3,fi_predicates,
! [X1,X2] :
( l3(X1,X2)
<=> $true ) ).
fof(l4,fi_predicates,
! [X1] :
( l4(X1)
<=> $true ) ).
fof(l5,fi_predicates,
! [X1] :
( l5(X1)
<=> $true ) ).
fof(m0,fi_predicates,
! [X1,X2,X3] :
( m0(X1,X2,X3)
<=> $true ) ).
fof(m1,fi_predicates,
! [X1,X2,X3] :
( m1(X1,X2,X3)
<=> $true ) ).
fof(m2,fi_predicates,
! [X1] :
( m2(X1)
<=> $true ) ).
fof(m3,fi_predicates,
! [X1,X2,X3] :
( m3(X1,X2,X3)
<=> $true ) ).
fof(m4,fi_predicates,
! [X1,X2] :
( m4(X1,X2)
<=> $true ) ).
fof(m5,fi_predicates,
! [X1,X2] :
( m5(X1,X2)
<=> $true ) ).
fof(n0,fi_predicates,
! [X1,X2] :
( n0(X1,X2)
<=> $true ) ).
fof(n1,fi_predicates,
! [X1,X2,X3] :
( n1(X1,X2,X3)
<=> $true ) ).
fof(n2,fi_predicates,
! [X1] :
( n2(X1)
<=> $true ) ).
fof(n3,fi_predicates,
! [X1] :
( n3(X1)
<=> $true ) ).
fof(n4,fi_predicates,
! [X1,X2] :
( n4(X1,X2)
<=> $true ) ).
fof(n5,fi_predicates,
! [X1,X2] :
( n5(X1,X2)
<=> $true ) ).
fof(p0,fi_predicates,
! [X1,X2] :
( p0(X1,X2)
<=> $true ) ).
fof(p1,fi_predicates,
! [X1,X2,X3] :
( p1(X1,X2,X3)
<=> $true ) ).
fof(p2,fi_predicates,
! [X1,X2,X3] :
( p2(X1,X2,X3)
<=> $true ) ).
fof(p3,fi_predicates,
! [X1,X2,X3] :
( p3(X1,X2,X3)
<=> $true ) ).
fof(p4,fi_predicates,
! [X1,X2,X3] :
( p4(X1,X2,X3)
<=> $true ) ).
fof(p5,fi_predicates,
! [X1,X2,X3] :
( p5(X1,X2,X3)
<=> $true ) ).
fof(q0,fi_predicates,
! [X1,X2] :
( q0(X1,X2)
<=> $true ) ).
fof(q1,fi_predicates,
! [X1,X2,X3] :
( q1(X1,X2,X3)
<=> $true ) ).
fof(q2,fi_predicates,
! [X1,X2,X3] :
( q2(X1,X2,X3)
<=> $true ) ).
fof(q3,fi_predicates,
! [X1,X2] :
( q3(X1,X2)
<=> $true ) ).
fof(q4,fi_predicates,
! [X1,X2] :
( q4(X1,X2)
<=> $true ) ).
fof(q5,fi_predicates,
! [X1,X2] :
( q5(X1,X2)
<=> $true ) ).
fof(r0,fi_predicates,
! [X1] :
( r0(X1)
<=> $true ) ).
fof(r1,fi_predicates,
! [X1] :
( r1(X1)
<=> $true ) ).
fof(r2,fi_predicates,
! [X1] :
( r2(X1)
<=> $true ) ).
fof(r3,fi_predicates,
! [X1,X2,X3] :
( r3(X1,X2,X3)
<=> $true ) ).
fof(r4,fi_predicates,
! [X1] :
( r4(X1)
<=> $true ) ).
fof(r5,fi_predicates,
! [X1,X2] :
( r5(X1,X2)
<=> $true ) ).
fof(s0,fi_predicates,
! [X1] :
( s0(X1)
<=> $true ) ).
fof(s1,fi_predicates,
! [X1] :
( s1(X1)
<=> $true ) ).
fof(s2,fi_predicates,
! [X1] :
( s2(X1)
<=> $true ) ).
fof(s3,fi_predicates,
! [X1,X2] :
( s3(X1,X2)
<=> $true ) ).
fof(s4,fi_predicates,
! [X1] :
( s4(X1)
<=> $true ) ).
fof(s5,fi_predicates,
! [X1] :
( s5(X1)
<=> $true ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.13 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jul 12 06:59:39 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 Paradox, version 4.0, 2010-06-29.
% 0.13/0.35 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK
% 0.13/0.35 Reading 'Axioms/SYN001-0.ax' ... ('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax') OK
% 0.21/0.43 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.47 +++ BEGIN MODEL
% 0.21/0.47 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.21/0.47 +++ END MODEL
% 0.21/0.47 +++ RESULT: Satisfiable
% 0.21/0.47 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------