%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYN513-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n019.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:48:21 EDT 2022
% Result : Satisfiable 0.20s 0.53s
% Output : FiniteModel 0.20s
% Verified :
% SZS Type : FiniteModel
% Domain size : 3
% Comments :
%------------------------------------------------------------------------------
% domain size is 3
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2"
| X = "3" ) ).
fof(a775,fi_functors,
a775 = "1" ).
fof(a776,fi_functors,
a776 = "1" ).
fof(a777,fi_functors,
a777 = "1" ).
fof(a778,fi_functors,
a778 = "1" ).
fof(a779,fi_functors,
a779 = "1" ).
fof(a780,fi_functors,
a780 = "1" ).
fof(a781,fi_functors,
a781 = "1" ).
fof(a782,fi_functors,
a782 = "1" ).
fof(a783,fi_functors,
a783 = "1" ).
fof(a784,fi_functors,
a784 = "1" ).
fof(a785,fi_functors,
a785 = "1" ).
fof(a786,fi_functors,
a786 = "3" ).
fof(a787,fi_functors,
a787 = "1" ).
fof(a788,fi_functors,
a788 = "3" ).
fof(a789,fi_functors,
a789 = "2" ).
fof(a790,fi_functors,
a790 = "3" ).
fof(a791,fi_functors,
a791 = "3" ).
fof(a792,fi_functors,
a792 = "1" ).
fof(a793,fi_functors,
a793 = "1" ).
fof(a794,fi_functors,
a794 = "1" ).
fof(a795,fi_functors,
a795 = "1" ).
fof(a796,fi_functors,
a796 = "3" ).
fof(a797,fi_functors,
a797 = "2" ).
fof(a798,fi_functors,
a798 = "1" ).
fof(a800,fi_functors,
a800 = "1" ).
fof(a801,fi_functors,
a801 = "1" ).
fof(a802,fi_functors,
a802 = "1" ).
fof(a803,fi_functors,
a803 = "1" ).
fof(a804,fi_functors,
a804 = "3" ).
fof(a805,fi_functors,
a805 = "1" ).
fof(a806,fi_functors,
a806 = "2" ).
fof(a807,fi_functors,
a807 = "3" ).
fof(a808,fi_functors,
a808 = "2" ).
fof(a809,fi_functors,
a809 = "3" ).
fof(a811,fi_functors,
a811 = "1" ).
fof(a812,fi_functors,
a812 = "1" ).
fof(a813,fi_functors,
a813 = "1" ).
fof(a815,fi_functors,
a815 = "1" ).
fof(a816,fi_functors,
a816 = "1" ).
fof(a817,fi_functors,
a817 = "1" ).
fof(a818,fi_functors,
a818 = "1" ).
fof(a819,fi_functors,
a819 = "1" ).
fof(a820,fi_functors,
a820 = "1" ).
fof(a821,fi_functors,
a821 = "1" ).
fof(a822,fi_functors,
a822 = "1" ).
fof(a823,fi_functors,
a823 = "1" ).
fof(a824,fi_functors,
a824 = "1" ).
fof(a825,fi_functors,
a825 = "1" ).
fof(a826,fi_functors,
a826 = "2" ).
fof(a827,fi_functors,
a827 = "1" ).
fof(a828,fi_functors,
a828 = "1" ).
fof(a829,fi_functors,
a829 = "1" ).
fof(a830,fi_functors,
a830 = "1" ).
fof(a831,fi_functors,
a831 = "3" ).
fof(a832,fi_functors,
a832 = "1" ).
fof(a833,fi_functors,
a833 = "1" ).
fof(a834,fi_functors,
a834 = "1" ).
fof(a835,fi_functors,
a835 = "1" ).
fof(a836,fi_functors,
a836 = "1" ).
fof(a837,fi_functors,
a837 = "1" ).
fof(a838,fi_functors,
a838 = "1" ).
fof(a839,fi_functors,
a839 = "2" ).
fof(a840,fi_functors,
a840 = "1" ).
fof(a841,fi_functors,
a841 = "3" ).
fof(a842,fi_functors,
a842 = "1" ).
fof(a843,fi_functors,
a843 = "3" ).
fof(a844,fi_functors,
a844 = "1" ).
fof(a845,fi_functors,
a845 = "1" ).
fof(a846,fi_functors,
a846 = "1" ).
fof(a847,fi_functors,
a847 = "2" ).
fof(a848,fi_functors,
a848 = "1" ).
fof(a849,fi_functors,
a849 = "1" ).
fof(a850,fi_functors,
a850 = "1" ).
fof(a851,fi_functors,
a851 = "3" ).
fof(a852,fi_functors,
a852 = "1" ).
fof(a853,fi_functors,
a853 = "3" ).
fof(a854,fi_functors,
a854 = "2" ).
fof(a855,fi_functors,
a855 = "1" ).
fof(a856,fi_functors,
a856 = "1" ).
fof(a857,fi_functors,
a857 = "1" ).
fof(a858,fi_functors,
a858 = "3" ).
fof(a859,fi_functors,
a859 = "2" ).
fof(a860,fi_functors,
a860 = "1" ).
fof(a861,fi_functors,
a861 = "1" ).
fof(a862,fi_functors,
a862 = "1" ).
fof(a863,fi_functors,
a863 = "1" ).
fof(a864,fi_functors,
a864 = "1" ).
fof(a865,fi_functors,
a865 = "1" ).
fof(a866,fi_functors,
a866 = "1" ).
fof(a867,fi_functors,
a867 = "3" ).
fof(a868,fi_functors,
a868 = "3" ).
fof(a869,fi_functors,
a869 = "2" ).
fof(a870,fi_functors,
a870 = "1" ).
fof(a871,fi_functors,
a871 = "2" ).
fof(a872,fi_functors,
a872 = "3" ).
fof(a873,fi_functors,
a873 = "1" ).
fof(a874,fi_functors,
a874 = "1" ).
fof(a875,fi_functors,
a875 = "1" ).
fof(a876,fi_functors,
a876 = "1" ).
fof(a877,fi_functors,
a877 = "1" ).
fof(a878,fi_functors,
a878 = "1" ).
fof(a879,fi_functors,
a879 = "1" ).
fof(a880,fi_functors,
a880 = "1" ).
fof(a881,fi_functors,
a881 = "3" ).
fof(a882,fi_functors,
a882 = "1" ).
fof(a883,fi_functors,
a883 = "1" ).
fof(a884,fi_functors,
a884 = "3" ).
fof(a886,fi_functors,
a886 = "2" ).
fof(a887,fi_functors,
a887 = "1" ).
fof(a888,fi_functors,
a888 = "1" ).
fof(a889,fi_functors,
a889 = "1" ).
fof(a890,fi_functors,
a890 = "1" ).
fof(a891,fi_functors,
a891 = "1" ).
fof(a892,fi_functors,
a892 = "1" ).
fof(a893,fi_functors,
a893 = "3" ).
fof(a894,fi_functors,
a894 = "2" ).
fof(a895,fi_functors,
a895 = "1" ).
fof(a896,fi_functors,
a896 = "1" ).
fof(c1_0,fi_predicates,
( c1_0
<=> $false ) ).
fof(c1_1,fi_predicates,
( ( c1_1("1")
<=> $false )
& ( c1_1("2")
<=> $true )
& ( c1_1("3")
<=> $false ) ) ).
fof(c1_2,fi_predicates,
( ( c1_2("1","1")
<=> $true )
& ( c1_2("1","2")
<=> $false )
& ( c1_2("1","3")
<=> $true )
& ( c1_2("2","1")
<=> $false )
& ( c1_2("2","2")
<=> $false )
& ( c1_2("2","3")
<=> $true )
& ( c1_2("3","1")
<=> $false )
& ( c1_2("3","2")
<=> $false )
& ( c1_2("3","3")
<=> $false ) ) ).
fof(c2_0,fi_predicates,
( c2_0
<=> $false ) ).
fof(c2_1,fi_predicates,
( ( c2_1("1")
<=> $true )
& ( c2_1("2")
<=> $false )
& ( c2_1("3")
<=> $true ) ) ).
fof(c2_2,fi_predicates,
( ( c2_2("1","1")
<=> $false )
& ( c2_2("1","2")
<=> $false )
& ( c2_2("1","3")
<=> $true )
& ( c2_2("2","1")
<=> $true )
& ( c2_2("2","2")
<=> $true )
& ( c2_2("2","3")
<=> $false )
& ( c2_2("3","1")
<=> $false )
& ( c2_2("3","2")
<=> $true )
& ( c2_2("3","3")
<=> $false ) ) ).
fof(c3_0,fi_predicates,
( c3_0
<=> $true ) ).
fof(c3_1,fi_predicates,
( ( c3_1("1")
<=> $false )
& ( c3_1("2")
<=> $false )
& ( c3_1("3")
<=> $true ) ) ).
fof(c3_2,fi_predicates,
( ( c3_2("1","1")
<=> $false )
& ( c3_2("1","2")
<=> $false )
& ( c3_2("1","3")
<=> $true )
& ( c3_2("2","1")
<=> $true )
& ( c3_2("2","2")
<=> $true )
& ( c3_2("2","3")
<=> $true )
& ( c3_2("3","1")
<=> $true )
& ( c3_2("3","2")
<=> $true )
& ( c3_2("3","3")
<=> $false ) ) ).
fof(c4_0,fi_predicates,
( c4_0
<=> $false ) ).
fof(c4_1,fi_predicates,
( ( c4_1("1")
<=> $true )
& ( c4_1("2")
<=> $true )
& ( c4_1("3")
<=> $true ) ) ).
fof(c4_2,fi_predicates,
( ( c4_2("1","1")
<=> $false )
& ( c4_2("1","2")
<=> $true )
& ( c4_2("1","3")
<=> $false )
& ( c4_2("2","1")
<=> $true )
& ( c4_2("2","2")
<=> $true )
& ( c4_2("2","3")
<=> $false )
& ( c4_2("3","1")
<=> $true )
& ( c4_2("3","2")
<=> $false )
& ( c4_2("3","3")
<=> $true ) ) ).
fof(c5_0,fi_predicates,
( c5_0
<=> $true ) ).
fof(c5_1,fi_predicates,
( ( c5_1("1")
<=> $false )
& ( c5_1("2")
<=> $false )
& ( c5_1("3")
<=> $true ) ) ).
fof(c5_2,fi_predicates,
( ( c5_2("1","1")
<=> $true )
& ( c5_2("1","2")
<=> $true )
& ( c5_2("1","3")
<=> $false )
& ( c5_2("2","1")
<=> $false )
& ( c5_2("2","2")
<=> $true )
& ( c5_2("2","3")
<=> $false )
& ( c5_2("3","1")
<=> $false )
& ( c5_2("3","2")
<=> $true )
& ( c5_2("3","3")
<=> $true ) ) ).
fof(ndr1_0,fi_predicates,
( ndr1_0
<=> $true ) ).
fof(ndr1_1,fi_predicates,
( ( ndr1_1("1")
<=> $true )
& ( ndr1_1("2")
<=> $true )
& ( ndr1_1("3")
<=> $true ) ) ).
fof(ssSkC0,fi_predicates,
( ssSkC0
<=> $true ) ).
fof(ssSkC1,fi_predicates,
( ssSkC1
<=> $true ) ).
fof(ssSkC10,fi_predicates,
( ssSkC10
<=> $false ) ).
fof(ssSkC11,fi_predicates,
( ssSkC11
<=> $true ) ).
fof(ssSkC12,fi_predicates,
( ssSkC12
<=> $true ) ).
fof(ssSkC13,fi_predicates,
( ssSkC13
<=> $true ) ).
fof(ssSkC14,fi_predicates,
( ssSkC14
<=> $true ) ).
fof(ssSkC15,fi_predicates,
( ssSkC15
<=> $false ) ).
fof(ssSkC16,fi_predicates,
( ssSkC16
<=> $false ) ).
fof(ssSkC17,fi_predicates,
( ssSkC17
<=> $false ) ).
fof(ssSkC18,fi_predicates,
( ssSkC18
<=> $true ) ).
fof(ssSkC19,fi_predicates,
( ssSkC19
<=> $true ) ).
fof(ssSkC2,fi_predicates,
( ssSkC2
<=> $true ) ).
fof(ssSkC20,fi_predicates,
( ssSkC20
<=> $false ) ).
fof(ssSkC21,fi_predicates,
( ssSkC21
<=> $true ) ).
fof(ssSkC22,fi_predicates,
( ssSkC22
<=> $true ) ).
fof(ssSkC3,fi_predicates,
( ssSkC3
<=> $true ) ).
fof(ssSkC4,fi_predicates,
( ssSkC4
<=> $false ) ).
fof(ssSkC5,fi_predicates,
( ssSkC5
<=> $true ) ).
fof(ssSkC6,fi_predicates,
( ssSkC6
<=> $true ) ).
fof(ssSkC7,fi_predicates,
( ssSkC7
<=> $false ) ).
fof(ssSkC8,fi_predicates,
( ssSkC8
<=> $false ) ).
fof(ssSkC9,fi_predicates,
( ssSkC9
<=> $false ) ).
fof(ssSkP0,fi_predicates,
( ( ssSkP0("1")
<=> $false )
& ( ssSkP0("2")
<=> $true )
& ( ssSkP0("3")
<=> $true ) ) ).
fof(ssSkP1,fi_predicates,
( ( ssSkP1("1")
<=> $true )
& ( ssSkP1("2")
<=> $false )
& ( ssSkP1("3")
<=> $true ) ) ).
fof(ssSkP2,fi_predicates,
( ( ssSkP2("1")
<=> $true )
& ( ssSkP2("2")
<=> $true )
& ( ssSkP2("3")
<=> $false ) ) ).
fof(ssSkP3,fi_predicates,
( ( ssSkP3("1")
<=> $true )
& ( ssSkP3("2")
<=> $true )
& ( ssSkP3("3")
<=> $true ) ) ).
fof(ssSkP4,fi_predicates,
( ( ssSkP4("1")
<=> $true )
& ( ssSkP4("2")
<=> $true )
& ( ssSkP4("3")
<=> $false ) ) ).
fof(ssSkP5,fi_predicates,
( ( ssSkP5("1")
<=> $true )
& ( ssSkP5("2")
<=> $false )
& ( ssSkP5("3")
<=> $false ) ) ).
fof(ssSkP6,fi_predicates,
( ( ssSkP6("1")
<=> $true )
& ( ssSkP6("2")
<=> $true )
& ( ssSkP6("3")
<=> $true ) ) ).
fof(ssSkP7,fi_predicates,
( ( ssSkP7("1")
<=> $false )
& ( ssSkP7("2")
<=> $true )
& ( ssSkP7("3")
<=> $true ) ) ).
fof(ssSkP8,fi_predicates,
( ( ssSkP8("1")
<=> $true )
& ( ssSkP8("2")
<=> $true )
& ( ssSkP8("3")
<=> $true ) ) ).
fof(ssSkP9,fi_predicates,
( ( ssSkP9("1")
<=> $true )
& ( ssSkP9("2")
<=> $true )
& ( ssSkP9("3")
<=> $true ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN513-1 : TPTP v8.1.0. Released v2.1.0.
% 0.13/0.13 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.34 % Computer : n019.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 05:37:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 Paradox, version 4.0, 2010-06-29.
% 0.13/0.34 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK
% 0.20/0.43 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.53 +++ BEGIN MODEL
% 0.20/0.53 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.20/0.53 +++ END MODEL
% 0.20/0.53 +++ RESULT: Satisfiable
% 0.20/0.53 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------