%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NLP007+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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 : 300s
% DateTime : Sat Jun 21 05:17:38 AM UTC 2025
% Result : Theorem 0.11s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NLP007+1 : TPTP v9.0.0. Released v2.4.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n007.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 23:40:05 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.11/0.37 % SZS status Theorem
% 0.11/0.37 % SZS output start Proof
% 0.11/0.37 tff(in_type, type, (
% 0.11/0.37 in: ( $i * $i ) > $o)).
% 0.11/0.37 tff(young_type, type, (
% 0.11/0.37 young: $i > $o)).
% 0.11/0.37 tff(man_type, type, (
% 0.11/0.37 man: $i > $o)).
% 0.11/0.37 tff(fellow_type, type, (
% 0.11/0.37 fellow: $i > $o)).
% 0.11/0.37 tff(front_type, type, (
% 0.11/0.37 front: $i > $o)).
% 0.11/0.37 tff(furniture_type, type, (
% 0.11/0.37 furniture: $i > $o)).
% 0.11/0.37 tff(seat_type, type, (
% 0.11/0.37 seat: $i > $o)).
% 0.11/0.37 tff(down_type, type, (
% 0.11/0.37 down: ( $i * $i ) > $o)).
% 0.11/0.37 tff(barrel_type, type, (
% 0.11/0.37 barrel: ( $i * $i ) > $o)).
% 0.11/0.37 tff(lonely_type, type, (
% 0.11/0.37 lonely: $i > $o)).
% 0.11/0.37 tff(way_type, type, (
% 0.11/0.37 way: $i > $o)).
% 0.11/0.37 tff(street_type, type, (
% 0.11/0.37 street: $i > $o)).
% 0.11/0.37 tff(old_type, type, (
% 0.11/0.37 old: $i > $o)).
% 0.11/0.37 tff(dirty_type, type, (
% 0.11/0.37 dirty: $i > $o)).
% 0.11/0.37 tff(white_type, type, (
% 0.11/0.37 white: $i > $o)).
% 0.11/0.37 tff(car_type, type, (
% 0.11/0.37 car: $i > $o)).
% 0.11/0.37 tff(chevy_type, type, (
% 0.11/0.37 chevy: $i > $o)).
% 0.11/0.37 tff(event_type, type, (
% 0.11/0.37 event: $i > $o)).
% 0.11/0.37 tff(city_type, type, (
% 0.11/0.37 city: $i > $o)).
% 0.11/0.37 tff(hollywood_type, type, (
% 0.11/0.37 hollywood: $i > $o)).
% 0.11/0.37 tff(tptp_fun_X15_15_type, type, (
% 0.11/0.37 tptp_fun_X15_15: $i)).
% 0.11/0.37 tff(tptp_fun_X23_9_type, type, (
% 0.11/0.37 tptp_fun_X23_9: $i)).
% 0.11/0.37 tff(tptp_fun_X22_10_type, type, (
% 0.11/0.37 tptp_fun_X22_10: $i)).
% 0.11/0.37 tff(tptp_fun_X24_8_type, type, (
% 0.11/0.37 tptp_fun_X24_8: $i)).
% 0.11/0.37 tff(tptp_fun_X16_14_type, type, (
% 0.11/0.37 tptp_fun_X16_14: $i)).
% 0.11/0.37 tff(tptp_fun_X17_13_type, type, (
% 0.11/0.37 tptp_fun_X17_13: $i)).
% 0.11/0.37 tff(tptp_fun_X19_11_type, type, (
% 0.11/0.37 tptp_fun_X19_11: $i)).
% 0.11/0.37 tff(tptp_fun_X18_12_type, type, (
% 0.11/0.37 tptp_fun_X18_12: $i)).
% 0.11/0.37 tff(tptp_fun_Y_3_type, type, (
% 0.11/0.37 tptp_fun_Y_3: $i)).
% 0.11/0.37 tff(tptp_fun_X2_2_type, type, (
% 0.11/0.37 tptp_fun_X2_2: $i)).
% 0.11/0.37 tff(tptp_fun_X3_1_type, type, (
% 0.11/0.37 tptp_fun_X3_1: $i)).
% 0.11/0.37 tff(tptp_fun_X4_0_type, type, (
% 0.11/0.37 tptp_fun_X4_0: $i)).
% 0.11/0.37 tff(tptp_fun_V_6_type, type, (
% 0.11/0.37 tptp_fun_V_6: $i)).
% 0.11/0.37 tff(tptp_fun_W_5_type, type, (
% 0.11/0.37 tptp_fun_W_5: $i)).
% 0.11/0.37 tff(tptp_fun_X_4_type, type, (
% 0.11/0.37 tptp_fun_X_4: $i)).
% 0.11/0.37 tff(tptp_fun_U_7_type, type, (
% 0.11/0.37 tptp_fun_U_7: $i)).
% 0.11/0.37 tff(1,assumption,(~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))), introduced(assumption)).
% 0.11/0.37 tff(2,plain,
% 0.11/0.37 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(3,plain,
% 0.18/0.37 (![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.18/0.37 tff(4,plain,
% 0.18/0.37 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | lonely(Y!3)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(5,plain,
% 0.18/0.37 (lonely(Y!3)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.18/0.37 tff(6,plain,
% 0.18/0.37 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | way(Y!3)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(7,plain,
% 0.18/0.37 (way(Y!3)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[6, 1])).
% 0.18/0.37 tff(8,plain,
% 0.18/0.37 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | in(X3!1, X2!2)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(9,plain,
% 0.18/0.38 (in(X3!1, X2!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[8, 1])).
% 0.18/0.38 tff(10,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | young(X4!0)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(11,plain,
% 0.18/0.38 (young(X4!0)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[10, 1])).
% 0.18/0.38 tff(12,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | man(X4!0)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(13,plain,
% 0.18/0.38 (man(X4!0)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[12, 1])).
% 0.18/0.38 tff(14,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | fellow(X4!0)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(15,plain,
% 0.18/0.38 (fellow(X4!0)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[14, 1])).
% 0.18/0.38 tff(16,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | young(X3!1)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(17,plain,
% 0.18/0.38 (young(X3!1)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[16, 1])).
% 0.18/0.38 tff(18,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | man(X3!1)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(19,plain,
% 0.18/0.38 (man(X3!1)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[18, 1])).
% 0.18/0.38 tff(20,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | fellow(X3!1)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(21,plain,
% 0.18/0.38 (fellow(X3!1)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[20, 1])).
% 0.18/0.38 tff(22,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | front(X2!2)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(23,plain,
% 0.18/0.38 (front(X2!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[22, 1])).
% 0.18/0.38 tff(24,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | furniture(X2!2)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(25,plain,
% 0.18/0.38 (furniture(X2!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[24, 1])).
% 0.18/0.38 tff(26,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | seat(X2!2)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(27,plain,
% 0.18/0.38 (seat(X2!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[26, 1])).
% 0.18/0.38 tff(28,plain,
% 0.18/0.38 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | in(W!5, V!6)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(29,plain,
% 0.18/0.39 (in(W!5, V!6)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[28, 1])).
% 0.18/0.39 tff(30,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | down(W!5, Y!3)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(31,plain,
% 0.18/0.39 (down(W!5, Y!3)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[30, 1])).
% 0.18/0.39 tff(32,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | barrel(W!5, X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(33,plain,
% 0.18/0.39 (barrel(W!5, X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[32, 1])).
% 0.18/0.39 tff(34,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | street(Y!3)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(35,plain,
% 0.18/0.39 (street(Y!3)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[34, 1])).
% 0.18/0.39 tff(36,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | old(X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(37,plain,
% 0.18/0.39 (old(X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[36, 1])).
% 0.18/0.39 tff(38,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | dirty(X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(39,plain,
% 0.18/0.39 (dirty(X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[38, 1])).
% 0.18/0.39 tff(40,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | white(X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(41,plain,
% 0.18/0.39 (white(X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[40, 1])).
% 0.18/0.39 tff(42,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | car(X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(43,plain,
% 0.18/0.39 (car(X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[42, 1])).
% 0.18/0.39 tff(44,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | chevy(X!4)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(45,plain,
% 0.18/0.39 (chevy(X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[44, 1])).
% 0.18/0.39 tff(46,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | event(W!5)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(47,plain,
% 0.18/0.39 (event(W!5)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[46, 1])).
% 0.18/0.39 tff(48,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | city(V!6)),
% 0.18/0.39 inference(tautology,[status(thm)],[])).
% 0.18/0.39 tff(49,plain,
% 0.18/0.39 (city(V!6)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[48, 1])).
% 0.18/0.39 tff(50,plain,
% 0.18/0.39 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | hollywood(V!6)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(51,plain,
% 0.18/0.40 (hollywood(V!6)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[50, 1])).
% 0.18/0.40 tff(52,plain,
% 0.18/0.40 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | front(U!7)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(53,plain,
% 0.18/0.40 (front(U!7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[52, 1])).
% 0.18/0.40 tff(54,plain,
% 0.18/0.40 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | furniture(U!7)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(55,plain,
% 0.18/0.40 (furniture(U!7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[54, 1])).
% 0.18/0.40 tff(56,plain,
% 0.18/0.40 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | seat(U!7)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(57,plain,
% 0.18/0.40 (seat(U!7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[56, 1])).
% 0.18/0.40 tff(58,plain,
% 0.18/0.40 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | in(X4!0, U!7)),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(59,plain,
% 0.18/0.40 (in(X4!0, U!7)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[58, 1])).
% 0.18/0.40 tff(60,plain,
% 0.18/0.40 (((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) | (~(X3!1 = X4!0))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(61,plain,
% 0.18/0.40 (~(X3!1 = X4!0)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[60, 1])).
% 0.18/0.40 tff(62,plain,
% 0.18/0.40 (((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | ((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(63,plain,
% 0.18/0.40 (((~in(X4!0, U!7)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~way(Y!3)) | (~lonely(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (X3!1 = X4!0)) <=> ((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(64,plain,
% 0.18/0.40 (((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | ((~in(X4!0, U!7)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~way(Y!3)) | (~lonely(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (X3!1 = X4!0))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | ((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3))))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[63])).
% 0.18/0.41 tff(65,plain,
% 0.18/0.41 (((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | ((~in(X4!0, U!7)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~way(Y!3)) | (~lonely(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (X3!1 = X4!0))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)))),
% 0.18/0.41 inference(transitivity,[status(thm)],[64, 62])).
% 0.18/0.41 tff(66,plain,
% 0.18/0.41 ((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | ((~in(X4!0, U!7)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~way(Y!3)) | (~lonely(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (X3!1 = X4!0))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(67,plain,
% 0.18/0.41 ((~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.18/0.41 tff(68,plain,
% 0.18/0.41 ($false),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[67, 61, 59, 57, 55, 53, 51, 49, 47, 45, 43, 41, 39, 37, 35, 33, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9, 7, 5, 3])).
% 0.18/0.41 tff(69,plain,((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.41 tff(70,plain,
% 0.18/0.41 (((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))))))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(71,plain,
% 0.18/0.41 ((~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)))) <=> (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(72,plain,
% 0.18/0.42 ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) <=> (~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(73,plain,
% 0.18/0.42 (((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))))))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[72, 71])).
% 0.18/0.42 tff(74,plain,
% 0.18/0.42 (((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~way(Y!3)) | (~lonely(Y!3)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))))))),
% 0.18/0.43 inference(transitivity,[status(thm)],[73, 70])).
% 0.18/0.43 tff(75,plain,
% 0.18/0.43 (((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)))))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(76,plain,
% 0.18/0.43 (((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)))))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(77,plain,
% 0.18/0.43 ((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) <=> (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(78,plain,
% 0.18/0.43 (^[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : trans(monotonicity(rewrite((in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)) <=> (~((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))), ((~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))) <=> (~(~((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))))), rewrite((~(~((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))) <=> ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))), ((~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))) <=> ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))))),
% 0.18/0.44 inference(bind,[status(th)],[])).
% 0.18/0.44 tff(79,plain,
% 0.18/0.44 (![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))) <=> ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))),
% 0.18/0.44 inference(quant_intro,[status(thm)],[78])).
% 0.18/0.44 tff(80,plain,
% 0.18/0.44 ((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))) <=> (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34)))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[79])).
% 0.18/0.44 tff(81,plain,
% 0.18/0.44 ((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))) <=> (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15))))),
% 0.18/0.44 inference(transitivity,[status(thm)],[80, 77])).
% 0.18/0.44 tff(82,plain,
% 0.18/0.44 ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) <=> (~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3))))),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(83,plain,
% 0.18/0.44 (^[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : trans(monotonicity(rewrite((in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)) <=> (~((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))), ((~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) <=> (~(~((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))))), rewrite((~(~((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))) <=> ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))), ((~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) <=> ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))))),
% 0.18/0.44 inference(bind,[status(th)],[])).
% 0.18/0.44 tff(84,plain,
% 0.18/0.44 (![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) <=> ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))),
% 0.18/0.44 inference(quant_intro,[status(thm)],[83])).
% 0.18/0.44 tff(85,plain,
% 0.18/0.44 ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) <=> (in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14)))),
% 0.18/0.44 inference(monotonicity,[status(thm)],[84])).
% 0.18/0.44 tff(86,plain,
% 0.18/0.44 ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) <=> (~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3))))),
% 0.18/0.45 inference(transitivity,[status(thm)],[85, 82])).
% 0.18/0.45 tff(87,plain,
% 0.18/0.45 (((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)))))),
% 0.18/0.45 inference(monotonicity,[status(thm)],[86, 81])).
% 0.18/0.45 tff(88,plain,
% 0.18/0.45 (((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> ((~((X3!1 = X4!0) | (~in(X4!0, U!7)) | (~seat(U!7)) | (~furniture(U!7)) | (~front(U!7)) | (~hollywood(V!6)) | (~city(V!6)) | (~event(W!5)) | (~chevy(X!4)) | (~car(X!4)) | (~white(X!4)) | (~dirty(X!4)) | (~old(X!4)) | (~street(Y!3)) | (~barrel(W!5, X!4)) | (~down(W!5, Y!3)) | (~in(W!5, V!6)) | (~seat(X2!2)) | (~furniture(X2!2)) | (~front(X2!2)) | (~fellow(X3!1)) | (~man(X3!1)) | (~young(X3!1)) | (~fellow(X4!0)) | (~man(X4!0)) | (~young(X4!0)) | (~in(X3!1, X2!2)) | (~![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : ((~in(X14, X12)) | (~seat(X5)) | (~furniture(X5)) | (~front(X5)) | (~hollywood(X6)) | (~city(X6)) | (~event(X7)) | (~chevy(X8)) | (~car(X8)) | (~white(X8)) | (~dirty(X8)) | (~old(X8)) | (~street(X9)) | (~way(X9)) | (~lonely(X9)) | (~barrel(X7, X8)) | (~down(X7, X9)) | (~in(X7, X6)) | (~seat(X12)) | (~furniture(X12)) | (~front(X12)) | (~fellow(X13)) | (~man(X13)) | (~young(X13)) | (~fellow(X14)) | (~man(X14)) | (~young(X14)) | (~in(X13, X5)) | (X13 = X14))) | (~way(Y!3)) | (~lonely(Y!3)))) | (~((X23!9 = X24!8) | (~in(X24!8, X22!10)) | (~seat(X15!15)) | (~furniture(X15!15)) | (~front(X15!15)) | (~hollywood(X16!14)) | (~city(X16!14)) | (~event(X17!13)) | (~chevy(X18!12)) | (~car(X18!12)) | (~white(X18!12)) | (~dirty(X18!12)) | (~old(X18!12)) | (~street(X19!11)) | (~way(X19!11)) | (~lonely(X19!11)) | (~barrel(X17!13, X18!12)) | (~down(X17!13, X19!11)) | (~in(X17!13, X16!14)) | (~seat(X22!10)) | (~furniture(X22!10)) | (~fellow(X24!8)) | (~man(X23!9)) | (~young(X23!9)) | (~young(X24!8)) | (~man(X24!8)) | (~![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : ((~seat(X25)) | (~furniture(X25)) | (~front(X25)) | (~hollywood(X26)) | (~city(X26)) | (~event(X27)) | (~chevy(X28)) | (~car(X28)) | (~white(X28)) | (~dirty(X28)) | (~old(X28)) | (~street(X29)) | (~way(X29)) | (~lonely(X29)) | (~barrel(X27, X28)) | (~down(X27, X29)) | (~in(X27, X26)) | (~seat(X32)) | (~furniture(X32)) | (~front(X32)) | (~fellow(X33)) | (~man(X33)) | (~young(X33)) | (~fellow(X34)) | (~man(X34)) | (~young(X34)) | (~in(X34, X25)) | (~in(X33, X32)) | (X33 = X34))) | (~front(X22!10)) | (~fellow(X23!9)) | (~in(X23!9, X15!15)))))),
% 0.18/0.45 inference(transitivity,[status(thm)],[87, 76])).
% 0.18/0.45 tff(89,plain,
% 0.18/0.45 (((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(90,plain,
% 0.18/0.46 (((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15)) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))) <=> (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(91,plain,
% 0.18/0.46 (((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2)) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) <=> (in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(92,plain,
% 0.18/0.46 ((((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2)) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | ((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15)) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[91, 90])).
% 0.18/0.46 tff(93,plain,
% 0.18/0.46 ((((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2)) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | ((in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15)) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> ((in(X4!0, U!7) & seat(U!7) & furniture(U!7) & front(U!7) & hollywood(V!6) & city(V!6) & event(W!5) & chevy(X!4) & car(X!4) & white(X!4) & dirty(X!4) & old(X!4) & street(Y!3) & way(Y!3) & lonely(Y!3) & barrel(W!5, X!4) & down(W!5, Y!3) & in(W!5, V!6) & seat(X2!2) & furniture(X2!2) & front(X2!2) & (~(X3!1 = X4!0)) & fellow(X3!1) & man(X3!1) & young(X3!1) & fellow(X4!0) & man(X4!0) & young(X4!0) & in(X3!1, X2!2) & ![X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (~(in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))) | (in(X24!8, X22!10) & seat(X15!15) & furniture(X15!15) & front(X15!15) & hollywood(X16!14) & city(X16!14) & event(X17!13) & chevy(X18!12) & car(X18!12) & white(X18!12) & dirty(X18!12) & old(X18!12) & street(X19!11) & way(X19!11) & lonely(X19!11) & barrel(X17!13, X18!12) & down(X17!13, X19!11) & in(X17!13, X16!14) & seat(X22!10) & furniture(X22!10) & front(X22!10) & (~(X23!9 = X24!8)) & fellow(X23!9) & man(X23!9) & young(X23!9) & fellow(X24!8) & man(X24!8) & young(X24!8) & in(X23!9, X15!15) & ![X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (~(in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.46 inference(transitivity,[status(thm)],[92, 89])).
% 0.18/0.46 tff(94,plain,
% 0.18/0.46 (((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))) <=> ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(95,plain,
% 0.18/0.46 (((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) <=> ((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5)))),
% 0.18/0.46 inference(rewrite,[status(thm)],[])).
% 0.18/0.46 tff(96,plain,
% 0.18/0.46 ((((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))) <=> (((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[95, 94])).
% 0.18/0.46 tff(97,plain,
% 0.18/0.46 ((~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.46 inference(monotonicity,[status(thm)],[96])).
% 0.18/0.46 tff(98,plain,
% 0.18/0.46 ((~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(99,plain,
% 0.18/0.47 ((~((?[U: $i, V: $i, W: $i, X: $i, Y: $i, Z: $i, X1: $i, X2: $i, X3: $i, X4: $i] : ((((((((((((((((((((((((((((((seat(U) & furniture(U)) & front(U)) & hollywood(V)) & city(V)) & event(W)) & chevy(X)) & car(X)) & white(X)) & dirty(X)) & old(X)) & street(Y)) & way(Y)) & lonely(Y)) & barrel(W, X)) & down(W, Y)) & in(W, V)) & seat(X2)) & furniture(X2)) & front(X2)) & (~(Z = X1))) & fellow(Z)) & man(Z)) & young(Z)) & fellow(X1)) & man(X1)) & young(X1)) & (Z = X3)) & in(X3, X2)) & (X1 = X4)) & in(X4, U)) => ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X10: $i, X11: $i, X12: $i, X13: $i, X14: $i] : ((((((((((((((((((((((((((((((seat(X5) & furniture(X5)) & front(X5)) & hollywood(X6)) & city(X6)) & event(X7)) & chevy(X8)) & car(X8)) & white(X8)) & dirty(X8)) & old(X8)) & street(X9)) & way(X9)) & lonely(X9)) & barrel(X7, X8)) & down(X7, X9)) & in(X7, X6)) & seat(X12)) & furniture(X12)) & front(X12)) & (~(X10 = X11))) & fellow(X10)) & man(X10)) & young(X10)) & fellow(X11)) & man(X11)) & young(X11)) & (X10 = X13)) & in(X13, X5)) & (X11 = X14)) & in(X14, X12))) & (?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X20: $i, X21: $i, X22: $i, X23: $i, X24: $i] : ((((((((((((((((((((((((((((((seat(X15) & furniture(X15)) & front(X15)) & hollywood(X16)) & city(X16)) & event(X17)) & chevy(X18)) & car(X18)) & white(X18)) & dirty(X18)) & old(X18)) & street(X19)) & way(X19)) & lonely(X19)) & barrel(X17, X18)) & down(X17, X19)) & in(X17, X16)) & seat(X22)) & furniture(X22)) & front(X22)) & (~(X20 = X21))) & fellow(X20)) & man(X20)) & young(X20)) & fellow(X21)) & man(X21)) & young(X21)) & (X20 = X23)) & in(X23, X15)) & (X21 = X24)) & in(X24, X22)) => ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X30: $i, X31: $i, X32: $i, X33: $i, X34: $i] : ((((((((((((((((((((((((((((((seat(X25) & furniture(X25)) & front(X25)) & hollywood(X26)) & city(X26)) & event(X27)) & chevy(X28)) & car(X28)) & white(X28)) & dirty(X28)) & old(X28)) & street(X29)) & way(X29)) & lonely(X29)) & barrel(X27, X28)) & down(X27, X29)) & in(X27, X26)) & seat(X32)) & furniture(X32)) & front(X32)) & (~(X30 = X31))) & fellow(X30)) & man(X30)) & young(X30)) & fellow(X31)) & man(X31)) & young(X31)) & (X30 = X33)) & in(X33, X32)) & (X31 = X34)) & in(X34, X25))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32)))))),
% 0.18/0.47 inference(rewrite,[status(thm)],[])).
% 0.18/0.47 tff(100,axiom,(~((?[U: $i, V: $i, W: $i, X: $i, Y: $i, Z: $i, X1: $i, X2: $i, X3: $i, X4: $i] : ((((((((((((((((((((((((((((((seat(U) & furniture(U)) & front(U)) & hollywood(V)) & city(V)) & event(W)) & chevy(X)) & car(X)) & white(X)) & dirty(X)) & old(X)) & street(Y)) & way(Y)) & lonely(Y)) & barrel(W, X)) & down(W, Y)) & in(W, V)) & seat(X2)) & furniture(X2)) & front(X2)) & (~(Z = X1))) & fellow(Z)) & man(Z)) & young(Z)) & fellow(X1)) & man(X1)) & young(X1)) & (Z = X3)) & in(X3, X2)) & (X1 = X4)) & in(X4, U)) => ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X10: $i, X11: $i, X12: $i, X13: $i, X14: $i] : ((((((((((((((((((((((((((((((seat(X5) & furniture(X5)) & front(X5)) & hollywood(X6)) & city(X6)) & event(X7)) & chevy(X8)) & car(X8)) & white(X8)) & dirty(X8)) & old(X8)) & street(X9)) & way(X9)) & lonely(X9)) & barrel(X7, X8)) & down(X7, X9)) & in(X7, X6)) & seat(X12)) & furniture(X12)) & front(X12)) & (~(X10 = X11))) & fellow(X10)) & man(X10)) & young(X10)) & fellow(X11)) & man(X11)) & young(X11)) & (X10 = X13)) & in(X13, X5)) & (X11 = X14)) & in(X14, X12))) & (?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X20: $i, X21: $i, X22: $i, X23: $i, X24: $i] : ((((((((((((((((((((((((((((((seat(X15) & furniture(X15)) & front(X15)) & hollywood(X16)) & city(X16)) & event(X17)) & chevy(X18)) & car(X18)) & white(X18)) & dirty(X18)) & old(X18)) & street(X19)) & way(X19)) & lonely(X19)) & barrel(X17, X18)) & down(X17, X19)) & in(X17, X16)) & seat(X22)) & furniture(X22)) & front(X22)) & (~(X20 = X21))) & fellow(X20)) & man(X20)) & young(X20)) & fellow(X21)) & man(X21)) & young(X21)) & (X20 = X23)) & in(X23, X15)) & (X21 = X24)) & in(X24, X22)) => ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X30: $i, X31: $i, X32: $i, X33: $i, X34: $i] : ((((((((((((((((((((((((((((((seat(X25) & furniture(X25)) & front(X25)) & hollywood(X26)) & city(X26)) & event(X27)) & chevy(X28)) & car(X28)) & white(X28)) & dirty(X28)) & old(X28)) & street(X29)) & way(X29)) & lonely(X29)) & barrel(X27, X28)) & down(X27, X29)) & in(X27, X26)) & seat(X32)) & furniture(X32)) & front(X32)) & (~(X30 = X31))) & fellow(X30)) & man(X30)) & young(X30)) & fellow(X31)) & man(X31)) & young(X31)) & (X30 = X33)) & in(X33, X32)) & (X31 = X34)) & in(X34, X25))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')).
% 0.18/0.47 tff(101,plain,
% 0.18/0.47 (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.18/0.47 tff(102,plain,
% 0.18/0.47 (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[101, 97])).
% 0.18/0.47 tff(103,plain,
% 0.18/0.47 (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.47 inference(modus_ponens,[status(thm)],[102, 98])).
% 0.18/0.47 tff(104,plain,
% 0.18/0.47 (~(((~?[U: $i, V: $i, W: $i, X: $i, Y: $i, X2: $i, X3: $i, X4: $i] : (in(X4, U) & seat(U) & furniture(U) & front(U) & hollywood(V) & city(V) & event(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & street(Y) & way(Y) & lonely(Y) & barrel(W, X) & down(W, Y) & in(W, V) & seat(X2) & furniture(X2) & front(X2) & (~(X3 = X4)) & fellow(X3) & man(X3) & young(X3) & fellow(X4) & man(X4) & young(X4) & in(X3, X2))) | ?[X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X12: $i, X13: $i, X14: $i] : (in(X14, X12) & seat(X5) & furniture(X5) & front(X5) & hollywood(X6) & city(X6) & event(X7) & chevy(X8) & car(X8) & white(X8) & dirty(X8) & old(X8) & street(X9) & way(X9) & lonely(X9) & barrel(X7, X8) & down(X7, X9) & in(X7, X6) & seat(X12) & furniture(X12) & front(X12) & (~(X13 = X14)) & fellow(X13) & man(X13) & young(X13) & fellow(X14) & man(X14) & young(X14) & in(X13, X5))) & ((~?[X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X22: $i, X23: $i, X24: $i] : (in(X24, X22) & seat(X15) & furniture(X15) & front(X15) & hollywood(X16) & city(X16) & event(X17) & chevy(X18) & car(X18) & white(X18) & dirty(X18) & old(X18) & street(X19) & way(X19) & lonely(X19) & barrel(X17, X18) & down(X17, X19) & in(X17, X16) & seat(X22) & furniture(X22) & front(X22) & (~(X23 = X24)) & fellow(X23) & man(X23) & young(X23) & fellow(X24) & man(X24) & young(X24) & in(X23, X15))) | ?[X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X32: $i, X33: $i, X34: $i] : (in(X34, X25) & seat(X25) & furniture(X25) & front(X25) & hollywood(X26) & city(X26) & event(X27) & chevy(X28) & car(X28) & white(X28) & dirty(X28) & old(X28) & street(X29) & way(X29) & lonely(X29) & barrel(X27, X28) & down(X27, X29) & in(X27, X26) & seat(X32) & furniture(X32) & front(X32) & (~(X33 = X34)) & fellow(X33) & man(X33) & young(X33) & fellow(X34) & man(X34) & young(X34) & in(X33, X32))))),
% 0.18/0.48 inference(modus_ponens,[status(thm)],[103, 97])).
% 0.18/0.48 unexpected number of arguments: (let ((a!1 (exists ((U $i) (V $i) (W $i) (X $i) (Y $i) (X2 $i) (X3 $i) (X4 $i))
% 0.18/0.48 (and (in X4 U)
% 0.18/0.48 (seat U)
% 0.18/0.48 (furniture U)
% 0.18/0.48 (front U)
% 0.18/0.48 (hollywood V)
% 0.18/0.48 (city V)
% 0.18/0.48 (event W)
% 0.18/0.48 (chevy X)
% 0.18/0.48 (car X)
% 0.18/0.48 (white X)
% 0.18/0.48 (dirty X)
% 0.18/0.48 (old X)
% 0.18/0.48 (street Y)
% 0.18/0.48 (way Y)
% 0.18/0.48 (lonely Y)
% 0.18/0.48 (barrel W X)
% 0.18/0.48 (down W Y)
% 0.18/0.48 (in W V)
% 0.18/0.48 (seat X2)
% 0.18/0.48 (furniture X2)
% 0.18/0.48 (front X2)
% 0.18/0.48 (not (= X3 X4))
% 0.18/0.48 (fellow X3)
% 0.18/0.48 (man X3)
% 0.18/0.48 (young X3)
% 0.18/0.48 (fellow X4)
% 0.18/0.48 (man X4)
% 0.18/0.48 (young X4)
% 0.18/0.48 (in X3 X2))))
% 0.18/0.48 (a!2 (and (in X4!0 U!7)
% 0.18/0.48 (seat U!7)
% 0.18/0.48 (furniture U!7)
% 0.18/0.48 (front U!7)
% 0.18/0.48 (hollywood V!6)
% 0.18/0.48 (city V!6)
% 0.18/0.48 (event W!5)
% 0.18/0.48 (chevy X!4)
% 0.18/0.48 (car X!4)
% 0.18/0.48 (white X!4)
% 0.18/0.48 (dirty X!4)
% 0.18/0.48 (old X!4)
% 0.18/0.48 (street Y!3)
% 0.18/0.48 (way Y!3)
% 0.18/0.48 (lonely Y!3)
% 0.18/0.48 (barrel W!5 X!4)
% 0.18/0.48 (down W!5 Y!3)
% 0.18/0.48 (in W!5 V!6)
% 0.18/0.48 (seat X2!2)
% 0.18/0.48 (furniture X2!2)
% 0.18/0.48 (front X2!2)
% 0.18/0.48 (not (= X3!1 X4!0))
% 0.18/0.48 (fellow X3!1)
% 0.18/0.48 (man X3!1)
% 0.18/0.48 (young X3!1)
% 0.18/0.48 (fellow X4!0)
% 0.18/0.48 (man X4!0)
% 0.18/0.48 (young X4!0)
% 0.18/0.48 (in X3!1 X2!2)))
% 0.18/0.48 (a!4 (lambda ((X5 $i)
% 0.18/0.48 (X6 $i)
% 0.18/0.48 (X7 $i)
% 0.18/0.48 (X8 $i)
% 0.18/0.48 (X9 $i)
% 0.18/0.48 (X12 $i)
% 0.18/0.48 (X13 $i)
% 0.18/0.48 (X14 $i))
% 0.18/0.48 (let ((a!1 (and (in X14 X12)
% 0.18/0.48 (seat X5)
% 0.18/0.48 (furniture X5)
% 0.18/0.48 (front X5)
% 0.18/0.48 (hollywood X6)
% 0.18/0.48 (city X6)
% 0.18/0.48 (event X7)
% 0.18/0.48 (chevy X8)
% 0.18/0.48 (car X8)
% 0.18/0.48 (white X8)
% 0.18/0.48 (dirty X8)
% 0.18/0.48 (old X8)
% 0.18/0.48 (street X9)
% 0.18/0.48 (way X9)
% 0.18/0.48 (lonely X9)
% 0.18/0.48 (barrel X7 X8)
% 0.18/0.48 (down X7 X9)
% 0.18/0.48 (in X7 X6)
% 0.18/0.48 (seat X12)
% 0.18/0.48 (furniture X12)
% 0.18/0.48 (front X12)
% 0.18/0.48 (not (= X13 X14))
% 0.18/0.48 (fellow X13)
% 0.18/0.48 (man X13)
% 0.18/0.48 (young X13)
% 0.18/0.48 (fellow X14)
% 0.18/0.48 (man X14)
% 0.18/0.48 (young X14)
% 0.18/0.48 (in X13 X5))))
% 0.18/0.48 (refl (~ (not a!1) (not a!1))))))
% 0.18/0.48 (a!5 (exists ((X5 $i)
% 0.18/0.48 (X6 $i)
% 0.18/0.48 (X7 $i)
% 0.18/0.48 (X8 $i)
% 0.18/0.48 (X9 $i)
% 0.18/0.48 (X12 $i)
% 0.18/0.48 (X13 $i)
% 0.18/0.48 (X14 $i))
% 0.18/0.48 (and (in X14 X12)
% 0.18/0.48 (seat X5)
% 0.18/0.48 (furniture X5)
% 0.18/0.48 (front X5)
% 0.18/0.48 (hollywood X6)
% 0.18/0.48 (city X6)
% 0.18/0.48 (event X7)
% 0.18/0.48 (chevy X8)
% 0.18/0.48 (car X8)
% 0.18/0.48 (white X8)
% 0.18/0.48 (dirty X8)
% 0.18/0.48 (old X8)
% 0.18/0.48 (street X9)
% 0.18/0.48 (way X9)
% 0.18/0.48 (lonely X9)
% 0.18/0.48 (barrel X7 X8)
% 0.18/0.48 (down X7 X9)
% 0.18/0.48 (in X7 X6)
% 0.18/0.48 (seat X12)
% 0.18/0.48 (furniture X12)
% 0.18/0.48 (front X12)
% 0.18/0.48 (not (= X13 X14))
% 0.18/0.48 (fellow X13)
% 0.18/0.48 (man X13)
% 0.18/0.48 (young X13)
% 0.18/0.48 (fellow X14)
% 0.18/0.48 (man X14)
% 0.18/0.48 (young X14)
% 0.18/0.48 (in X13 X5))))
% 0.18/0.48 (a!6 (forall ((X5 $i)
% 0.18/0.48 (X6 $i)
% 0.18/0.48 (X7 $i)
% 0.18/0.48 (X8 $i)
% 0.18/0.48 (X9 $i)
% 0.18/0.48 (X12 $i)
% 0.18/0.48 (X13 $i)
% 0.18/0.48 (X14 $i))
% 0.18/0.48 (let ((a!1 (and (in X14 X12)
% 0.18/0.48 (seat X5)
% 0.18/0.48 (furniture X5)
% 0.18/0.48 (front X5)
% 0.18/0.48 (hollywood X6)
% 0.18/0.48 (city X6)
% 0.18/0.48 (event X7)
% 0.18/0.48 (chevy X8)
% 0.18/0.48 (car X8)
% 0.18/0.48 (white X8)
% 0.18/0.48 (dirty X8)
% 0.18/0.48 (old X8)
% 0.18/0.48 (street X9)
% 0.18/0.48 (way X9)
% 0.18/0.48 (lonely X9)
% 0.18/0.48 (barrel X7 X8)
% 0.18/0.48 (down X7 X9)
% 0.18/0.48 (in X7 X6)
% 0.18/0.48 (seat X12)
% 0.18/0.48 (furniture X12)
% 0.18/0.48 (front X12)
% 0.18/0.48 (not (= X13 X14))
% 0.18/0.48 (fellow X13)
% 0.18/0.48 (man X13)
% 0.18/0.48 (young X13)
% 0.18/0.48 (fellow X14)
% 0.18/0.48 (man X14)
% 0.18/0.48 (young X14)
% 0.18/0.48 (in X13 X5))))
% 0.18/0.48 (not a!1))))
% 0.18/0.48 (a!9 (exists ((X15 $i)
% 0.18/0.48 (X16 $i)
% 0.18/0.48 (X17 $i)
% 0.18/0.48 (X18 $i)
% 0.18/0.48 (X19 $i)
% 0.18/0.48 (X22 $i)
% 0.18/0.48 (X23 $i)
% 0.18/0.48 (X24 $i))
% 0.18/0.48 (and (in X24 X22)
% 0.18/0.48 (seat X15)
% 0.18/0.48 (furniture X15)
% 0.18/0.48 (front X15)
% 0.18/0.48 (hollywood X16)
% 0.18/0.48 (city X16)
% 0.18/0.48 (event X17)
% 0.18/0.48 (chevy X18)
% 0.18/0.48 (car X18)
% 0.18/0.48 (white X18)
% 0.18/0.48 (dirty X18)
% 0.18/0.48 (old X18)
% 0.18/0.48 (street X19)
% 0.18/0.48 (way X19)
% 0.18/0.48 (lonely X19)
% 0.18/0.48 (barrel X17 X18)
% 0.18/0.48 (down X17 X19)
% 0.18/0.48 (in X17 X16)
% 0.18/0.48 (seat X22)
% 0.18/0.48 (furniture X22)
% 0.18/0.48 (front X22)
% 0.18/0.48 (not (= X23 X24))
% 0.18/0.48 (fellow X23)
% 0.18/0.48 (man X23)
% 0.18/0.48 (young X23)
% 0.18/0.48 (fellow X24)
% 0.18/0.48 (man X24)
% 0.18/0.48 (young X24)
% 0.18/0.48 (in X23 X15))))
% 0.18/0.48 (a!10 (and (in X24!8 X22!10)
% 0.18/0.48 (seat X15!15)
% 0.18/0.48 (furniture X15!15)
% 0.18/0.48 (front X15!15)
% 0.18/0.48 (hollywood X16!14)
% 0.18/0.48 (city X16!14)
% 0.18/0.48 (event X17!13)
% 0.18/0.48 (chevy X18!12)
% 0.18/0.48 (car X18!12)
% 0.18/0.48 (white X18!12)
% 0.18/0.48 (dirty X18!12)
% 0.18/0.48 (old X18!12)
% 0.18/0.48 (street X19!11)
% 0.18/0.48 (way X19!11)
% 0.18/0.48 (lonely X19!11)
% 0.18/0.48 (barrel X17!13 X18!12)
% 0.18/0.48 (down X17!13 X19!11)
% 0.18/0.48 (in X17!13 X16!14)
% 0.18/0.48 (seat X22!10)
% 0.18/0.48 (furniture X22!10)
% 0.18/0.48 (front X22!10)
% 0.18/0.48 (not (= X23!9 X24!8))
% 0.18/0.48 (fellow X23!9)
% 0.18/0.48 (man X23!9)
% 0.18/0.48 (young X23!9)
% 0.18/0.48 (fellow X24!8)
% 0.18/0.48 (man X24!8)
% 0.18/0.48 (young X24!8)
% 0.18/0.48 (in X23!9 X15!15)))
% 0.18/0.48 (a!12 (lambda ((X25 $i)
% 0.18/0.48 (X26 $i)
% 0.18/0.48 (X27 $i)
% 0.18/0.48 (X28 $i)
% 0.18/0.48 (X29 $i)
% 0.18/0.48 (X32 $i)
% 0.18/0.48 (X33 $i)
% 0.18/0.48 (X34 $i))
% 0.18/0.48 (let ((a!1 (and (in X34 X25)
% 0.18/0.48 (seat X25)
% 0.18/0.48 (furniture X25)
% 0.18/0.48 (front X25)
% 0.18/0.48 (hollywood X26)
% 0.18/0.48 (city X26)
% 0.18/0.48 (event X27)
% 0.18/0.48 (chevy X28)
% 0.18/0.48 (car X28)
% 0.18/0.48 (white X28)
% 0.18/0.48 (dirty X28)
% 0.18/0.48 (old X28)
% 0.18/0.48 (street X29)
% 0.18/0.48 (way X29)
% 0.18/0.48 (lonely X29)
% 0.18/0.48 (barrel X27 X28)
% 0.18/0.48 (down X27 X29)
% 0.18/0.48 (in X27 X26)
% 0.18/0.48 (seat X32)
% 0.18/0.48 (furniture X32)
% 0.18/0.48 (front X32)
% 0.18/0.48 (not (= X33 X34))
% 0.18/0.48 (fellow X33)
% 0.18/0.48 (man X33)
% 0.18/0.48 (young X33)
% 0.18/0.48 (fellow X34)
% 0.18/0.48 (man X34)
% 0.18/0.48 (young X34)
% 0.18/0.48 (in X33 X32))))
% 0.18/0.48 (refl (~ (not a!1) (not a!1))))))
% 0.18/0.48 (a!13 (exists ((X25 $i)
% 0.18/0.48 (X26 $i)
% 0.18/0.48 (X27 $i)
% 0.18/0.48 (X28 $i)
% 0.18/0.48 (X29 $i)
% 0.18/0.48 (X32 $i)
% 0.18/0.48 (X33 $i)
% 0.18/0.48 (X34 $i))
% 0.18/0.48 (and (in X34 X25)
% 0.18/0.48 (seat X25)
% 0.18/0.48 (furniture X25)
% 0.18/0.48 (front X25)
% 0.18/0.48 (hollywood X26)
% 0.18/0.48 (city X26)
% 0.18/0.48 (event X27)
% 0.18/0.48 (chevy X28)
% 0.18/0.48 (car X28)
% 0.18/0.48 (white X28)
% 0.18/0.48 (dirty X28)
% 0.18/0.48 (old X28)
% 0.18/0.48 (street X29)
% 0.18/0.48 (way X29)
% 0.18/0.48 (lonely X29)
% 0.18/0.48 (barrel X27 X28)
% 0.18/0.48 (down X27 X29)
% 0.18/0.48 (in X27 X26)
% 0.18/0.48 (seat X32)
% 0.18/0.48 (furniture X32)
% 0.18/0.48 (front X32)
% 0.18/0.48 (not (= X33 X34))
% 0.18/0.48 (fellow X33)
% 0.18/0.48 (man X33)
% 0.18/0.48 (young X33)
% 0.18/0.48 (fellow X34)
% 0.18/0.48 (man X34)
% 0.18/0.48 (young X34)
% 0.18/0.48 (in X33 X32))))
% 0.18/0.48 (a!14 (forall ((X25 $i)
% 0.18/0.48 (X26 $i)
% 0.18/0.48 (X27 $i)
% 0.18/0.48 (X28 $i)
% 0.18/0.48 (X29 $i)
% 0.18/0.48 (X32 $i)
% 0.18/0.48 (X33 $i)
% 0.18/0.48 (X34 $i))
% 0.18/0.48 (let ((a!1 (and (in X34 X25)
% 0.18/0.48 (seat X25)
% 0.18/0.48 (furniture X25)
% 0.18/0.48 (front X25)
% 0.18/0.48 (hollywood X26)
% 0.18/0.48 (city X26)
% 0.18/0.48 (event X27)
% 0.18/0.48 (chevy X28)
% 0.18/0.48 (car X28)
% 0.18/0.48 (white X28)
% 0.18/0.48 (dirty X28)
% 0.18/0.48 (old X28)
% 0.18/0.48 (street X29)
% 0.18/0.48 (way X29)
% 0.18/0.48 (lonely X29)
% 0.18/0.48 (barrel X27 X28)
% 0.18/0.48 (down X27 X29)
% 0.18/0.48 (in X27 X26)
% 0.18/0.48 (seat X32)
% 0.18/0.48 (furniture X32)
% 0.18/0.48 (front X32)
% 0.18/0.48 (not (= X33 X34))
% 0.18/0.48 (fellow X33)
% 0.18/0.48 (man X33)
% 0.18/0.48 (young X33)
% 0.18/0.48 (fellow X34)
% 0.18/0.48 (man X34)
% 0.18/0.48 (young X34)
% 0.18/0.48 (in X33 X32))))
% 0.18/0.48 (not a!1)))))
% 0.18/0.48 (let ((a!3 (nnf-neg (sk (~ a!1 a!2)) (~ (not (not a!1)) a!2)))
% 0.18/0.48 (a!7 (~ (not (or (not a!1) a!5)) (and a!2 a!6)))
% 0.18/0.48 (a!11 (nnf-neg (sk (~ a!9 a!10)) (~ (not (not a!9)) a!10)))
% 0.18/0.48 (a!15 (~ (not (or (not a!9) a!13)) (and a!10 a!14)))
% 0.18/0.48 (a!17 (not (and (or (not a!1) a!5) (or (not a!9) a!13)))))
% 0.18/0.48 (let ((a!8 (nnf-neg a!3 (nnf-neg (proof-bind a!4) (~ (not a!5) a!6)) a!7))
% 0.18/0.48 (a!16 (nnf-neg a!11 (nnf-neg (proof-bind a!12) (~ (not a!13) a!14)) a!15)))
% 0.18/0.48 (nnf-neg a!8 a!16 (~ a!17 (or (and a!2 a!6) (and a!10 a!14)))))))
% 0.18/0.48 Proof display could not be completed: unexpected number of arguments
% 0.18/0.48 % E exiting
%------------------------------------------------------------------------------