%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n004.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 19:06:13 EDT 2022
% Result : CounterSatisfiable 0.18s 0.51s
% Output : FiniteModel 0.18s
% Verified :
% SZS Type : FiniteModel
% Domain size : 7
% Comments :
%------------------------------------------------------------------------------
% domain size is 7
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2"
| X = "3"
| X = "4"
| X = "5"
| X = "6"
| X = "7" ) ).
fof(b48_buttercup10098,fi_predicates,
( ( b48_buttercup10098("1")
<=> $true )
& ( b48_buttercup10098("2")
<=> $true )
& ( b48_buttercup10098("3")
<=> $true )
& ( b48_buttercup10098("4")
<=> $true )
& ( b48_buttercup10098("5")
<=> $true )
& ( b48_buttercup10098("6")
<=> $true )
& ( b48_buttercup10098("7")
<=> $true ) ) ).
fof(b48_buttercup10102,fi_predicates,
( ( b48_buttercup10102("1")
<=> $false )
& ( b48_buttercup10102("2")
<=> $false )
& ( b48_buttercup10102("3")
<=> $false )
& ( b48_buttercup10102("4")
<=> $false )
& ( b48_buttercup10102("5")
<=> $false )
& ( b48_buttercup10102("6")
<=> $true )
& ( b48_buttercup10102("7")
<=> $false ) ) ).
fof(b48_buttercup10104,fi_predicates,
( ( b48_buttercup10104("1")
<=> $false )
& ( b48_buttercup10104("2")
<=> $true )
& ( b48_buttercup10104("3")
<=> $false )
& ( b48_buttercup10104("4")
<=> $false )
& ( b48_buttercup10104("5")
<=> $false )
& ( b48_buttercup10104("6")
<=> $false )
& ( b48_buttercup10104("7")
<=> $false ) ) ).
fof(b48_buttercup10107,fi_predicates,
( ( b48_buttercup10107("1")
<=> $false )
& ( b48_buttercup10107("2")
<=> $false )
& ( b48_buttercup10107("3")
<=> $false )
& ( b48_buttercup10107("4")
<=> $true )
& ( b48_buttercup10107("5")
<=> $false )
& ( b48_buttercup10107("6")
<=> $false )
& ( b48_buttercup10107("7")
<=> $false ) ) ).
fof(b48_buttercup10108,fi_predicates,
( ( b48_buttercup10108("1")
<=> $false )
& ( b48_buttercup10108("2")
<=> $false )
& ( b48_buttercup10108("3")
<=> $false )
& ( b48_buttercup10108("4")
<=> $false )
& ( b48_buttercup10108("5")
<=> $true )
& ( b48_buttercup10108("6")
<=> $false )
& ( b48_buttercup10108("7")
<=> $false ) ) ).
fof(b48_buttercup10109,fi_predicates,
( ( b48_buttercup10109("1")
<=> $true )
& ( b48_buttercup10109("2")
<=> $false )
& ( b48_buttercup10109("3")
<=> $false )
& ( b48_buttercup10109("4")
<=> $false )
& ( b48_buttercup10109("5")
<=> $false )
& ( b48_buttercup10109("6")
<=> $false )
& ( b48_buttercup10109("7")
<=> $false ) ) ).
fof(b48_buttercup10110,fi_predicates,
( ( b48_buttercup10110("1")
<=> $false )
& ( b48_buttercup10110("2")
<=> $false )
& ( b48_buttercup10110("3")
<=> $false )
& ( b48_buttercup10110("4")
<=> $false )
& ( b48_buttercup10110("5")
<=> $false )
& ( b48_buttercup10110("6")
<=> $false )
& ( b48_buttercup10110("7")
<=> $true ) ) ).
fof(b48_buttercup10111,fi_predicates,
( ( b48_buttercup10111("1")
<=> $false )
& ( b48_buttercup10111("2")
<=> $false )
& ( b48_buttercup10111("3")
<=> $true )
& ( b48_buttercup10111("4")
<=> $false )
& ( b48_buttercup10111("5")
<=> $false )
& ( b48_buttercup10111("6")
<=> $false )
& ( b48_buttercup10111("7")
<=> $false ) ) ).
fof(k04_buttercup10100,fi_predicates,
( ( k04_buttercup10100("1")
<=> $true )
& ( k04_buttercup10100("2")
<=> $false )
& ( k04_buttercup10100("3")
<=> $true )
& ( k04_buttercup10100("4")
<=> $false )
& ( k04_buttercup10100("5")
<=> $false )
& ( k04_buttercup10100("6")
<=> $false )
& ( k04_buttercup10100("7")
<=> $false ) ) ).
fof(k04_buttercup10619,fi_predicates,
( ( k04_buttercup10619("1")
<=> $false )
& ( k04_buttercup10619("2")
<=> $true )
& ( k04_buttercup10619("3")
<=> $false )
& ( k04_buttercup10619("4")
<=> $true )
& ( k04_buttercup10619("5")
<=> $true )
& ( k04_buttercup10619("6")
<=> $true )
& ( k04_buttercup10619("7")
<=> $true ) ) ).
fof(k04_buttercup10620,fi_predicates,
( ( k04_buttercup10620("1")
<=> $false )
& ( k04_buttercup10620("2")
<=> $false )
& ( k04_buttercup10620("3")
<=> $false )
& ( k04_buttercup10620("4")
<=> $true )
& ( k04_buttercup10620("5")
<=> $false )
& ( k04_buttercup10620("6")
<=> $false )
& ( k04_buttercup10620("7")
<=> $false ) ) ).
fof(k04_buttercup10622,fi_predicates,
( ( k04_buttercup10622("1")
<=> $false )
& ( k04_buttercup10622("2")
<=> $true )
& ( k04_buttercup10622("3")
<=> $false )
& ( k04_buttercup10622("4")
<=> $false )
& ( k04_buttercup10622("5")
<=> $true )
& ( k04_buttercup10622("6")
<=> $true )
& ( k04_buttercup10622("7")
<=> $true ) ) ).
fof(sK100_sos_30_X86,fi_functors,
sK100_sos_30_X86 = "1" ).
fof(sK101_sos_31_X87,fi_functors,
sK101_sos_31_X87 = "3" ).
fof(sK102_sos_32_X88,fi_functors,
sK102_sos_32_X88 = "7" ).
fof(sK103_sos_33_X89,fi_functors,
sK103_sos_33_X89 = "6" ).
fof(sK104_sos_34_X90,fi_functors,
sK104_sos_34_X90 = "2" ).
fof(sK105_sos_35_X91,fi_functors,
sK105_sos_35_X91 = "4" ).
fof(sK106_sos_36_X92,fi_functors,
sK106_sos_36_X92 = "5" ).
fof(sK107_sos_37_X93,fi_functors,
sK107_sos_37_X93 = "1" ).
fof(sK10_sos_10_X15,fi_functors,
sK10_sos_10_X15 = "1" ).
fof(sK11_sos_10_X9,fi_functors,
sK11_sos_10_X9 = "1" ).
fof(sK12_sos_10_X10,fi_functors,
sK12_sos_10_X10 = "1" ).
fof(sK13_sos_10_X11,fi_functors,
sK13_sos_10_X11 = "2" ).
fof(sK156_goals_86_X142,fi_functors,
sK156_goals_86_X142 = "1" ).
fof(sK19_sos_11_X18,fi_functors,
sK19_sos_11_X18 = "3" ).
fof(sK21_sos_12_X23,fi_functors,
sK21_sos_12_X23 = "1" ).
fof(sK22_sos_12_X25,fi_functors,
sK22_sos_12_X25 = "1" ).
fof(sK23_sos_12_X20,fi_functors,
sK23_sos_12_X20 = "7" ).
fof(sK24_sos_12_X21,fi_functors,
sK24_sos_12_X21 = "1" ).
fof(sK25_sos_12_X19,fi_functors,
sK25_sos_12_X19 = "1" ).
fof(sK31_sos_13_X28,fi_functors,
sK31_sos_13_X28 = "1" ).
fof(sK33_sos_14_X33,fi_functors,
sK33_sos_14_X33 = "1" ).
fof(sK34_sos_14_X35,fi_functors,
sK34_sos_14_X35 = "7" ).
fof(sK35_sos_14_X30,fi_functors,
sK35_sos_14_X30 = "1" ).
fof(sK36_sos_14_X31,fi_functors,
sK36_sos_14_X31 = "1" ).
fof(sK37_sos_14_X29,fi_functors,
sK37_sos_14_X29 = "1" ).
fof(sK43_sos_15_X38,fi_functors,
sK43_sos_15_X38 = "1" ).
fof(sK45_sos_16_X43,fi_functors,
sK45_sos_16_X43 = "1" ).
fof(sK46_sos_16_X45,fi_functors,
sK46_sos_16_X45 = "1" ).
fof(sK47_sos_16_X40,fi_functors,
sK47_sos_16_X40 = "1" ).
fof(sK48_sos_16_X41,fi_functors,
sK48_sos_16_X41 = "1" ).
fof(sK49_sos_16_X39,fi_functors,
sK49_sos_16_X39 = "3" ).
fof(sK55_sos_17_X51,fi_functors,
sK55_sos_17_X51 = "3" ).
fof(sK56_sos_17_X53,fi_functors,
sK56_sos_17_X53 = "7" ).
fof(sK57_sos_17_X47,fi_functors,
sK57_sos_17_X47 = "3" ).
fof(sK58_sos_17_X48,fi_functors,
sK58_sos_17_X48 = "1" ).
fof(sK59_sos_17_X49,fi_functors,
sK59_sos_17_X49 = "1" ).
fof(sK65_sos_18_X56,fi_functors,
sK65_sos_18_X56 = "7" ).
fof(sK67_sos_19_X58,fi_functors,
sK67_sos_19_X58 = "2" ).
fof(sK69_sos_20_X60,fi_functors,
sK69_sos_20_X60 = "2" ).
fof(sK71_sos_21_X62,fi_functors,
sK71_sos_21_X62 = "2" ).
fof(sK73_sos_22_X67,fi_functors,
sK73_sos_22_X67 = "1" ).
fof(sK74_sos_22_X69,fi_functors,
sK74_sos_22_X69 = "7" ).
fof(sK75_sos_22_X63,fi_functors,
sK75_sos_22_X63 = "1" ).
fof(sK76_sos_22_X64,fi_functors,
sK76_sos_22_X64 = "2" ).
fof(sK77_sos_22_X65,fi_functors,
sK77_sos_22_X65 = "3" ).
fof(sK83_sos_23_X72,fi_functors,
sK83_sos_23_X72 = "7" ).
fof(sK86_sos_25_X80,fi_functors,
sK86_sos_25_X80 = "2" ).
fof(sK87_sos_25_X78,fi_functors,
sK87_sos_25_X78 = "1" ).
fof(sK88_sos_25_X74,fi_functors,
sK88_sos_25_X74 = "3" ).
fof(sK89_sos_25_X75,fi_functors,
sK89_sos_25_X75 = "1" ).
fof(sK90_sos_25_X76,fi_functors,
sK90_sos_25_X76 = "7" ).
fof(sK96_sos_26_X82,fi_functors,
sK96_sos_26_X82 = "1" ).
fof(sK97_sos_27_X83,fi_functors,
sK97_sos_27_X83 = "2" ).
fof(sK98_sos_28_X84,fi_functors,
sK98_sos_28_X84 = "4" ).
fof(sK99_sos_29_X85,fi_functors,
sK99_sos_29_X85 = "7" ).
fof(sK9_sos_10_X13,fi_functors,
sK9_sos_10_X13 = "1" ).
fof(sP14_sos_10_or,fi_predicates,
( sP14_sos_10_or
<=> $false ) ).
fof(sP15_sos_10_or,fi_predicates,
( sP15_sos_10_or
<=> $false ) ).
fof(sP26_sos_12_or,fi_predicates,
( sP26_sos_12_or
<=> $false ) ).
fof(sP27_sos_12_or,fi_predicates,
( sP27_sos_12_or
<=> $false ) ).
fof(sP38_sos_14_or,fi_predicates,
( sP38_sos_14_or
<=> $false ) ).
fof(sP39_sos_14_or,fi_predicates,
( sP39_sos_14_or
<=> $false ) ).
fof(sP50_sos_16_or,fi_predicates,
( sP50_sos_16_or
<=> $false ) ).
fof(sP51_sos_16_or,fi_predicates,
( sP51_sos_16_or
<=> $false ) ).
fof(sP60_sos_17_or,fi_predicates,
( sP60_sos_17_or
<=> $false ) ).
fof(sP61_sos_17_or,fi_predicates,
( sP61_sos_17_or
<=> $false ) ).
fof(sP78_sos_22_or,fi_predicates,
( sP78_sos_22_or
<=> $false ) ).
fof(sP79_sos_22_or,fi_predicates,
( sP79_sos_22_or
<=> $false ) ).
fof(sP91_sos_25_or,fi_predicates,
( sP91_sos_25_or
<=> $false ) ).
fof(sP92_sos_25_or,fi_predicates,
( sP92_sos_25_or
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0.
% 0.06/0.12 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jul 9 13:50:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 Paradox, version 4.0, 2010-06-29.
% 0.12/0.34 +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK
% 0.12/0.37 +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.51 +++ BEGIN MODEL
% 0.18/0.51 SZS output start FiniteModel for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.18/0.51 +++ END MODEL
% 0.18/0.51 +++ RESULT: CounterSatisfiable
% 0.18/0.51 SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------