%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 08:54:27 AM UTC 2026
% Result : Theorem 183.10s 183.41s
% Output : Proof 183.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(days_of_week,axiom,
! [X] :
( X = sunday
| X = saturday
| X = friday
| X = thursday
| X = wednesday
| X = tuesday
| X = monday ),
file('theBenchmark.p',days_of_week) ).
fof(uniquenames,axiom,
( saturday != sunday
& friday != sunday
& friday != saturday
& thursday != sunday
& thursday != saturday
& thursday != friday
& wednesday != sunday
& wednesday != saturday
& wednesday != friday
& wednesday != thursday
& tuesday != sunday
& tuesday != saturday
& tuesday != friday
& tuesday != thursday
& tuesday != wednesday
& monday != sunday
& monday != saturday
& monday != friday
& monday != thursday
& monday != wednesday
& monday != tuesday ),
file('theBenchmark.p',uniquenames) ).
fof(truth_unique,axiom,
! [X,Y] :
( ( truthday(Y)
& truthday(X) )
=> X = Y ),
file('theBenchmark.p',truth_unique) ).
fof(day1_unique,axiom,
! [X,Y] :
( ( day1(Y)
& day1(X) )
=> X = Y ),
file('theBenchmark.p',day1_unique) ).
fof(day2_unique,axiom,
! [X,Y] :
( ( day2(Y)
& day2(X) )
=> X = Y ),
file('theBenchmark.p',day2_unique) ).
fof(day3_unique,axiom,
! [X,Y] :
( ( day3(Y)
& day3(X) )
=> X = Y ),
file('theBenchmark.p',day3_unique) ).
fof(truth_once,axiom,
? [X] : truthday(X),
file('theBenchmark.p',truth_once) ).
fof(day1_once,axiom,
? [X] : day1(X),
file('theBenchmark.p',day1_once) ).
fof(day2_once,axiom,
? [X] : day2(X),
file('theBenchmark.p',day2_once) ).
fof(day3_once,axiom,
? [X] : day3(X),
file('theBenchmark.p',day3_once) ).
fof(monday_follows_sunday,axiom,
consecutive(sunday) = monday,
file('theBenchmark.p',monday_follows_sunday) ).
fof(tuesday_follows_monday,axiom,
consecutive(monday) = tuesday,
file('theBenchmark.p',tuesday_follows_monday) ).
fof(wednesday_follows_tuesday,axiom,
consecutive(tuesday) = wednesday,
file('theBenchmark.p',wednesday_follows_tuesday) ).
fof(thursday_follows_wednesday,axiom,
consecutive(wednesday) = thursday,
file('theBenchmark.p',thursday_follows_wednesday) ).
fof(friday_follows_thursday,axiom,
consecutive(thursday) = friday,
file('theBenchmark.p',friday_follows_thursday) ).
fof(saturday_follows_friday,axiom,
consecutive(friday) = saturday,
file('theBenchmark.p',saturday_follows_friday) ).
fof(sunday_follows_saturday,axiom,
consecutive(saturday) = sunday,
file('theBenchmark.p',sunday_follows_saturday) ).
fof(day2_follows_day1,axiom,
! [X] :
( day1(X)
<=> day2(consecutive(X)) ),
file('theBenchmark.p',day2_follows_day1) ).
fof(day3_follows_day2,axiom,
! [X] :
( day2(X)
<=> day3(consecutive(X)) ),
file('theBenchmark.p',day3_follows_day2) ).
fof(statement1,axiom,
! [X] :
( day1(X)
=> ( truthday(X)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ),
file('theBenchmark.p',statement1) ).
fof(statement2,axiom,
! [X] :
( day2(X)
=> ( truthday(X)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ),
file('theBenchmark.p',statement2) ).
fof(statement3,axiom,
! [X] :
( day3(X)
=> ( truthday(X)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ),
file('theBenchmark.p',statement3) ).
fof(tuesday_leo_tells_truths,conjecture,
truthday(tuesday),
file('theBenchmark.p',tuesday_leo_tells_truths) ).
fof(f_1_1,plain,
! [X] :
( X = sunday
| X = saturday
| X = friday
| X = thursday
| X = wednesday
| X = tuesday
| X = monday ),
inference(fof_nnf,[status(thm)],[days_of_week]) ).
fof(f_1_2,plain,
! [U_0] :
( U_0 = sunday
| U_0 = saturday
| U_0 = friday
| U_0 = thursday
| U_0 = wednesday
| U_0 = tuesday
| U_0 = monday ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( U_0 = sunday
| U_0 = saturday
| U_0 = friday
| U_0 = thursday
| U_0 = wednesday
| U_0 = tuesday
| U_0 = monday ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
( saturday != sunday
& friday != sunday
& friday != saturday
& thursday != sunday
& thursday != saturday
& thursday != friday
& wednesday != sunday
& wednesday != saturday
& wednesday != friday
& wednesday != thursday
& tuesday != sunday
& tuesday != saturday
& tuesday != friday
& tuesday != thursday
& tuesday != wednesday
& monday != sunday
& monday != saturday
& monday != friday
& monday != thursday
& monday != wednesday
& monday != tuesday ),
inference(fof_nnf,[status(thm)],[uniquenames]) ).
cnf(f_2_2,plain,
monday != tuesday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
monday != wednesday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_4,plain,
monday != thursday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_5,plain,
monday != friday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_6,plain,
monday != saturday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_7,plain,
monday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_8,plain,
tuesday != wednesday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_9,plain,
tuesday != thursday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_10,plain,
tuesday != friday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_11,plain,
tuesday != saturday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_12,plain,
tuesday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_13,plain,
wednesday != thursday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_14,plain,
wednesday != friday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_15,plain,
wednesday != saturday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_16,plain,
wednesday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_17,plain,
thursday != friday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_18,plain,
thursday != saturday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_19,plain,
thursday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_20,plain,
friday != saturday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_21,plain,
friday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
cnf(f_2_22,plain,
saturday != sunday,
inference(clausify,[status(thm)],[f_2_1]) ).
fof(f_3_1,plain,
! [X,Y] :
( X = Y
| ~ truthday(Y)
| ~ truthday(X) ),
inference(fof_nnf,[status(thm)],[truth_unique]) ).
fof(f_3_2,plain,
! [U_2,U_1] :
( U_2 = U_1
| ~ truthday(U_1)
| ~ truthday(U_2) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( U_2 = U_1
| ~ truthday(U_1)
| ~ truthday(U_2) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [X,Y] :
( X = Y
| ~ day1(Y)
| ~ day1(X) ),
inference(fof_nnf,[status(thm)],[day1_unique]) ).
fof(f_4_2,plain,
! [U_4,U_3] :
( U_4 = U_3
| ~ day1(U_3)
| ~ day1(U_4) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( U_4 = U_3
| ~ day1(U_3)
| ~ day1(U_4) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [X,Y] :
( X = Y
| ~ day2(Y)
| ~ day2(X) ),
inference(fof_nnf,[status(thm)],[day2_unique]) ).
fof(f_5_2,plain,
! [U_6,U_5] :
( U_6 = U_5
| ~ day2(U_5)
| ~ day2(U_6) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( U_6 = U_5
| ~ day2(U_5)
| ~ day2(U_6) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [X,Y] :
( X = Y
| ~ day3(Y)
| ~ day3(X) ),
inference(fof_nnf,[status(thm)],[day3_unique]) ).
fof(f_6_2,plain,
! [U_8,U_7] :
( U_8 = U_7
| ~ day3(U_7)
| ~ day3(U_8) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( U_8 = U_7
| ~ day3(U_7)
| ~ day3(U_8) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
? [X] : truthday(X),
inference(fof_nnf,[status(thm)],[truth_once]) ).
fof(f_7_2,plain,
? [U_9] : truthday(U_9),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
truthday(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_9,sK1)],[f_7_2]) ).
cnf(f_7_4,plain,
truthday(sK1),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
? [X] : day1(X),
inference(fof_nnf,[status(thm)],[day1_once]) ).
fof(f_8_2,plain,
? [U_10] : day1(U_10),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
day1(sK2),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_10,sK2)],[f_8_2]) ).
cnf(f_8_4,plain,
day1(sK2),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
? [X] : day2(X),
inference(fof_nnf,[status(thm)],[day2_once]) ).
fof(f_9_2,plain,
? [U_11] : day2(U_11),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
day2(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_11,sK3)],[f_9_2]) ).
cnf(f_9_4,plain,
day2(sK3),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
? [X] : day3(X),
inference(fof_nnf,[status(thm)],[day3_once]) ).
fof(f_10_2,plain,
? [U_12] : day3(U_12),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
day3(sK4),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_12,sK4)],[f_10_2]) ).
cnf(f_10_4,plain,
day3(sK4),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
consecutive(sunday) = monday,
inference(fof_nnf,[status(thm)],[monday_follows_sunday]) ).
cnf(f_11_2,plain,
consecutive(sunday) = monday,
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
consecutive(monday) = tuesday,
inference(fof_nnf,[status(thm)],[tuesday_follows_monday]) ).
cnf(f_12_2,plain,
consecutive(monday) = tuesday,
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_13_1,plain,
consecutive(tuesday) = wednesday,
inference(fof_nnf,[status(thm)],[wednesday_follows_tuesday]) ).
cnf(f_13_2,plain,
consecutive(tuesday) = wednesday,
inference(clausify,[status(thm)],[f_13_1]) ).
fof(f_14_1,plain,
consecutive(wednesday) = thursday,
inference(fof_nnf,[status(thm)],[thursday_follows_wednesday]) ).
cnf(f_14_2,plain,
consecutive(wednesday) = thursday,
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_15_1,plain,
consecutive(thursday) = friday,
inference(fof_nnf,[status(thm)],[friday_follows_thursday]) ).
cnf(f_15_2,plain,
consecutive(thursday) = friday,
inference(clausify,[status(thm)],[f_15_1]) ).
fof(f_16_1,plain,
consecutive(friday) = saturday,
inference(fof_nnf,[status(thm)],[saturday_follows_friday]) ).
cnf(f_16_2,plain,
consecutive(friday) = saturday,
inference(clausify,[status(thm)],[f_16_1]) ).
fof(f_17_1,plain,
consecutive(saturday) = sunday,
inference(fof_nnf,[status(thm)],[sunday_follows_saturday]) ).
cnf(f_17_2,plain,
consecutive(saturday) = sunday,
inference(clausify,[status(thm)],[f_17_1]) ).
fof(f_18_1,plain,
! [X] :
( ( day1(X)
| ~ day2(consecutive(X)) )
& ( day2(consecutive(X))
| ~ day1(X) ) ),
inference(fof_nnf,[status(thm)],[day2_follows_day1]) ).
fof(f_18_2,plain,
! [U_13] :
( ( day1(U_13)
| ~ day2(consecutive(U_13)) )
& ( day2(consecutive(U_13))
| ~ day1(U_13) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_15] :
( day1(U_15)
| ~ day2(consecutive(U_15)) )
& ! [U_14] :
( day2(consecutive(U_14))
| ~ day1(U_14) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
cnf(f_18_4,plain,
( day2(consecutive(U_14))
| ~ day1(U_14) ),
inference(clausify,[status(thm)],[f_18_3]) ).
cnf(f_18_5,plain,
( day1(U_15)
| ~ day2(consecutive(U_15)) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_19_1,plain,
! [X] :
( ( day2(X)
| ~ day3(consecutive(X)) )
& ( day3(consecutive(X))
| ~ day2(X) ) ),
inference(fof_nnf,[status(thm)],[day3_follows_day2]) ).
fof(f_19_2,plain,
! [U_16] :
( ( day2(U_16)
| ~ day3(consecutive(U_16)) )
& ( day3(consecutive(U_16))
| ~ day2(U_16) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_18] :
( day2(U_18)
| ~ day3(consecutive(U_18)) )
& ! [U_17] :
( day3(consecutive(U_17))
| ~ day2(U_17) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( day3(consecutive(U_17))
| ~ day2(U_17) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( day2(U_18)
| ~ day3(consecutive(U_18)) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X] :
( ( ( truthday(X)
| truthday(tuesday)
| truthday(monday) )
& ( ( ~ truthday(tuesday)
& ~ truthday(monday) )
| ~ truthday(X) ) )
| ~ day1(X) ),
inference(fof_nnf,[status(thm)],[statement1]) ).
fof(f_20_2,plain,
! [U_19] :
( ( ( truthday(U_19)
| truthday(tuesday)
| truthday(monday) )
& ( ( ~ truthday(tuesday)
& ~ truthday(monday) )
| ~ truthday(U_19) ) )
| ~ day1(U_19) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( ~ truthday(monday)
| ~ truthday(U_19)
| ~ day1(U_19) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( ~ truthday(tuesday)
| ~ truthday(U_19)
| ~ day1(U_19) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_5,plain,
( truthday(U_19)
| truthday(tuesday)
| truthday(monday)
| ~ day1(U_19) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X] :
( ( ( truthday(X)
| ( ~ day2(sunday)
& ~ day2(saturday)
& ~ day2(thursday) ) )
& ( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ truthday(X) ) )
| ~ day2(X) ),
inference(fof_nnf,[status(thm)],[statement2]) ).
fof(f_21_2,plain,
! [U_20] :
( ( ( truthday(U_20)
| ( ~ day2(sunday)
& ~ day2(saturday)
& ~ day2(thursday) ) )
& ( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ truthday(U_20) ) )
| ~ day2(U_20) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ truthday(U_20)
| ~ day2(U_20) ),
inference(clausify,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( ~ day2(thursday)
| truthday(U_20)
| ~ day2(U_20) ),
inference(clausify,[status(thm)],[f_21_2]) ).
cnf(f_21_5,plain,
( ~ day2(saturday)
| truthday(U_20)
| ~ day2(U_20) ),
inference(clausify,[status(thm)],[f_21_2]) ).
cnf(f_21_6,plain,
( ~ day2(sunday)
| truthday(U_20)
| ~ day2(U_20) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X] :
( ( ( truthday(X)
| truthday(friday)
| truthday(wednesday) )
& ( ( ~ truthday(friday)
& ~ truthday(wednesday) )
| ~ truthday(X) ) )
| ~ day3(X) ),
inference(fof_nnf,[status(thm)],[statement3]) ).
fof(f_22_2,plain,
! [U_21] :
( ( ( truthday(U_21)
| truthday(friday)
| truthday(wednesday) )
& ( ( ~ truthday(friday)
& ~ truthday(wednesday) )
| ~ truthday(U_21) ) )
| ~ day3(U_21) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( ~ truthday(wednesday)
| ~ truthday(U_21)
| ~ day3(U_21) ),
inference(clausify,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( ~ truthday(friday)
| ~ truthday(U_21)
| ~ day3(U_21) ),
inference(clausify,[status(thm)],[f_22_2]) ).
cnf(f_22_5,plain,
( truthday(U_21)
| truthday(friday)
| truthday(wednesday)
| ~ day3(U_21) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,negated_conjecture,
~ truthday(tuesday),
inference(negate,[status(cth)],[tuesday_leo_tells_truths]) ).
fof(f_23_2,negated_conjecture,
~ truthday(tuesday),
inference(definitional_conversion,[status(esa)],[f_23_1]) ).
cnf(f_23_3,negated_conjecture,
~ truthday(tuesday),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( consecutive(Eq_x_0) = consecutive(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( truthday(Eq_y_0)
| ~ truthday(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_6,axiom,
( day1(Eq_y_0)
| ~ day1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_7,axiom,
( day2(Eq_y_0)
| ~ day2(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_8,axiom,
( day3(Eq_y_0)
| ~ day3(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.39 % Computer : n019.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sat Sep 19 20:03:35 UTC 2026
% 0.10/0.40 % CPUTime :
% 183.10/183.41 % SZS status Theorem for theBenchmark
% 183.10/183.41 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------