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