%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NLP009+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:17:38 AM UTC 2025
% Result : Theorem 0.18s 0.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NLP009+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.11 % Command : run_E %s %d THM
% 0.10/0.31 % Computer : n006.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Thu Jun 19 23:38:20 EDT 2025
% 0.16/0.31 % CPUTime :
% 0.18/0.36 % SZS status Theorem
% 0.18/0.36 % SZS output start Proof
% 0.18/0.36 tff(in_type, type, (
% 0.18/0.36 in: ( $i * $i ) > $o)).
% 0.18/0.36 tff(young_type, type, (
% 0.18/0.36 young: $i > $o)).
% 0.18/0.36 tff(man_type, type, (
% 0.18/0.36 man: $i > $o)).
% 0.18/0.36 tff(fellow_type, type, (
% 0.18/0.36 fellow: $i > $o)).
% 0.18/0.36 tff(front_type, type, (
% 0.18/0.36 front: $i > $o)).
% 0.18/0.36 tff(furniture_type, type, (
% 0.18/0.36 furniture: $i > $o)).
% 0.18/0.36 tff(seat_type, type, (
% 0.18/0.36 seat: $i > $o)).
% 0.18/0.36 tff(down_type, type, (
% 0.18/0.36 down: ( $i * $i ) > $o)).
% 0.18/0.36 tff(barrel_type, type, (
% 0.18/0.36 barrel: ( $i * $i ) > $o)).
% 0.18/0.36 tff(lonely_type, type, (
% 0.18/0.36 lonely: $i > $o)).
% 0.18/0.36 tff(way_type, type, (
% 0.18/0.36 way: $i > $o)).
% 0.18/0.36 tff(street_type, type, (
% 0.18/0.36 street: $i > $o)).
% 0.18/0.36 tff(old_type, type, (
% 0.18/0.36 old: $i > $o)).
% 0.18/0.36 tff(dirty_type, type, (
% 0.18/0.36 dirty: $i > $o)).
% 0.18/0.36 tff(white_type, type, (
% 0.18/0.36 white: $i > $o)).
% 0.18/0.36 tff(car_type, type, (
% 0.18/0.36 car: $i > $o)).
% 0.18/0.36 tff(chevy_type, type, (
% 0.18/0.36 chevy: $i > $o)).
% 0.18/0.36 tff(event_type, type, (
% 0.18/0.36 event: $i > $o)).
% 0.18/0.36 tff(city_type, type, (
% 0.18/0.36 city: $i > $o)).
% 0.18/0.36 tff(hollywood_type, type, (
% 0.18/0.36 hollywood: $i > $o)).
% 0.18/0.36 tff(tptp_fun_X1_2_type, type, (
% 0.18/0.36 tptp_fun_X1_2: $i)).
% 0.18/0.36 tff(tptp_fun_X2_1_type, type, (
% 0.18/0.36 tptp_fun_X2_1: $i)).
% 0.18/0.36 tff(tptp_fun_X3_0_type, type, (
% 0.18/0.36 tptp_fun_X3_0: $i)).
% 0.18/0.36 tff(tptp_fun_U_6_type, type, (
% 0.18/0.36 tptp_fun_U_6: $i)).
% 0.18/0.36 tff(tptp_fun_V_5_type, type, (
% 0.18/0.36 tptp_fun_V_5: $i)).
% 0.18/0.36 tff(tptp_fun_W_4_type, type, (
% 0.18/0.36 tptp_fun_W_4: $i)).
% 0.18/0.36 tff(tptp_fun_X_3_type, type, (
% 0.18/0.36 tptp_fun_X_3: $i)).
% 0.18/0.36 tff(tptp_fun_X19_9_type, type, (
% 0.18/0.36 tptp_fun_X19_9: $i)).
% 0.18/0.36 tff(tptp_fun_X20_8_type, type, (
% 0.18/0.36 tptp_fun_X20_8: $i)).
% 0.18/0.36 tff(tptp_fun_X21_7_type, type, (
% 0.18/0.36 tptp_fun_X21_7: $i)).
% 0.18/0.36 tff(tptp_fun_X13_13_type, type, (
% 0.18/0.36 tptp_fun_X13_13: $i)).
% 0.18/0.36 tff(tptp_fun_X14_12_type, type, (
% 0.18/0.36 tptp_fun_X14_12: $i)).
% 0.18/0.36 tff(tptp_fun_X16_10_type, type, (
% 0.18/0.36 tptp_fun_X16_10: $i)).
% 0.18/0.36 tff(tptp_fun_X15_11_type, type, (
% 0.18/0.36 tptp_fun_X15_11: $i)).
% 0.18/0.36 tff(1,assumption,(~((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))))), introduced(assumption)).
% 0.18/0.36 tff(2,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(3,plain,
% 0.18/0.36 (![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.18/0.36 tff(4,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | in(X20!8, X19!9)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(5,plain,
% 0.18/0.36 (in(X20!8, X19!9)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.18/0.36 tff(6,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | young(X21!7)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(7,plain,
% 0.18/0.36 (young(X21!7)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[6, 1])).
% 0.18/0.36 tff(8,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | man(X21!7)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(9,plain,
% 0.18/0.36 (man(X21!7)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[8, 1])).
% 0.18/0.36 tff(10,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | fellow(X21!7)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(11,plain,
% 0.18/0.36 (fellow(X21!7)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[10, 1])).
% 0.18/0.36 tff(12,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | young(X20!8)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(13,plain,
% 0.18/0.36 (young(X20!8)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[12, 1])).
% 0.18/0.36 tff(14,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | man(X20!8)),
% 0.18/0.36 inference(tautology,[status(thm)],[])).
% 0.18/0.36 tff(15,plain,
% 0.18/0.36 (man(X20!8)),
% 0.18/0.36 inference(unit_resolution,[status(thm)],[14, 1])).
% 0.18/0.36 tff(16,plain,
% 0.18/0.36 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | fellow(X20!8)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(17,plain,
% 0.18/0.37 (fellow(X20!8)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[16, 1])).
% 0.18/0.37 tff(18,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | front(X19!9)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(19,plain,
% 0.18/0.37 (front(X19!9)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[18, 1])).
% 0.18/0.37 tff(20,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | furniture(X19!9)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(21,plain,
% 0.18/0.37 (furniture(X19!9)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[20, 1])).
% 0.18/0.37 tff(22,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | seat(X19!9)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(23,plain,
% 0.18/0.37 (seat(X19!9)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[22, 1])).
% 0.18/0.37 tff(24,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | in(X14!12, X13!13)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(25,plain,
% 0.18/0.37 (in(X14!12, X13!13)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[24, 1])).
% 0.18/0.37 tff(26,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | down(X14!12, X16!10)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(27,plain,
% 0.18/0.37 (down(X14!12, X16!10)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[26, 1])).
% 0.18/0.37 tff(28,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | barrel(X14!12, X15!11)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(29,plain,
% 0.18/0.37 (barrel(X14!12, X15!11)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[28, 1])).
% 0.18/0.37 tff(30,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | lonely(X16!10)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(31,plain,
% 0.18/0.37 (lonely(X16!10)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[30, 1])).
% 0.18/0.37 tff(32,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | way(X16!10)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(33,plain,
% 0.18/0.37 (way(X16!10)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[32, 1])).
% 0.18/0.37 tff(34,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | street(X16!10)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(35,plain,
% 0.18/0.37 (street(X16!10)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[34, 1])).
% 0.18/0.37 tff(36,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | old(X15!11)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(37,plain,
% 0.18/0.37 (old(X15!11)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[36, 1])).
% 0.18/0.37 tff(38,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | dirty(X15!11)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(39,plain,
% 0.18/0.37 (dirty(X15!11)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[38, 1])).
% 0.18/0.37 tff(40,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | white(X15!11)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(41,plain,
% 0.18/0.37 (white(X15!11)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[40, 1])).
% 0.18/0.37 tff(42,plain,
% 0.18/0.37 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | car(X15!11)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(43,plain,
% 0.18/0.37 (car(X15!11)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[42, 1])).
% 0.18/0.37 tff(44,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | chevy(X15!11)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(45,plain,
% 0.18/0.38 (chevy(X15!11)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[44, 1])).
% 0.18/0.38 tff(46,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | event(X14!12)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(47,plain,
% 0.18/0.38 (event(X14!12)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[46, 1])).
% 0.18/0.38 tff(48,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | city(X13!13)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(49,plain,
% 0.18/0.38 (city(X13!13)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[48, 1])).
% 0.18/0.38 tff(50,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | hollywood(X13!13)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(51,plain,
% 0.18/0.38 (hollywood(X13!13)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[50, 1])).
% 0.18/0.38 tff(52,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | in(X21!7, X19!9)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(53,plain,
% 0.18/0.38 (in(X21!7, X19!9)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[52, 1])).
% 0.18/0.38 tff(54,plain,
% 0.18/0.38 (((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))) | (~(X20!8 = X21!7))),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(55,plain,
% 0.18/0.38 (~(X20!8 = X21!7)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[54, 1])).
% 0.18/0.38 tff(56,plain,
% 0.18/0.38 (((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | ((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)))) <=> ((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | (X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(57,plain,
% 0.18/0.39 (((~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (X20!8 = X21!7) | (~way(X16!10)) | (~street(X16!10)) | (~lonely(X16!10)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~down(X14!12, X16!10)) | (~old(X15!11)) | (~barrel(X14!12, X15!11))) <=> ((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(58,plain,
% 0.18/0.39 (((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | ((~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (X20!8 = X21!7) | (~way(X16!10)) | (~street(X16!10)) | (~lonely(X16!10)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~down(X14!12, X16!10)) | (~old(X15!11)) | (~barrel(X14!12, X15!11)))) <=> ((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | ((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9))))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[57])).
% 0.18/0.39 tff(59,plain,
% 0.18/0.39 (((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | ((~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (X20!8 = X21!7) | (~way(X16!10)) | (~street(X16!10)) | (~lonely(X16!10)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~down(X14!12, X16!10)) | (~old(X15!11)) | (~barrel(X14!12, X15!11)))) <=> ((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | (X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)))),
% 0.18/0.39 inference(transitivity,[status(thm)],[58, 56])).
% 0.18/0.39 tff(60,plain,
% 0.18/0.39 ((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | ((~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (X20!8 = X21!7) | (~way(X16!10)) | (~street(X16!10)) | (~lonely(X16!10)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~down(X14!12, X16!10)) | (~old(X15!11)) | (~barrel(X14!12, X15!11)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(61,plain,
% 0.18/0.39 ((~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))) | (X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.18/0.39 tff(62,plain,
% 0.18/0.39 ($false),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[61, 55, 53, 51, 49, 47, 45, 43, 41, 39, 37, 35, 33, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9, 7, 5, 3])).
% 0.18/0.39 tff(63,plain,((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.39 tff(64,plain,
% 0.18/0.39 (((~((X2!1 = X3!0) | (~in(X3!0, X1!2)) | (~hollywood(U!6)) | (~city(U!6)) | (~event(V!5)) | (~street(W!4)) | (~way(W!4)) | (~lonely(W!4)) | (~chevy(X!3)) | (~car(X!3)) | (~white(X!3)) | (~dirty(X!3)) | (~old(X!3)) | (~barrel(V!5, X!3)) | (~down(V!5, W!4)) | (~in(V!5, U!6)) | (~seat(X1!2)) | (~furniture(X1!2)) | (~front(X1!2)) | (~fellow(X2!1)) | (~man(X2!1)) | (~young(X2!1)) | (~fellow(X3!0)) | (~man(X3!0)) | (~young(X3!0)) | (~in(X2!1, X1!2)) | (~![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : ((~in(X12, X10)) | (~hollywood(X4)) | (~city(X4)) | (~event(X5)) | (~chevy(X6)) | (~car(X6)) | (~white(X6)) | (~dirty(X6)) | (~old(X6)) | (~street(X7)) | (~way(X7)) | (~lonely(X7)) | (~barrel(X5, X6)) | (~down(X5, X7)) | (~in(X5, X4)) | (~seat(X10)) | (~furniture(X10)) | (~front(X10)) | (~fellow(X11)) | (~man(X11)) | (~young(X11)) | (~fellow(X12)) | (~man(X12)) | (~young(X12)) | (~in(X11, X10)) | (X11 = X12))))) | (~((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25))))))) <=> ((~((X2!1 = X3!0) | (~in(X3!0, X1!2)) | (~hollywood(U!6)) | (~city(U!6)) | (~event(V!5)) | (~street(W!4)) | (~way(W!4)) | (~lonely(W!4)) | (~chevy(X!3)) | (~car(X!3)) | (~white(X!3)) | (~dirty(X!3)) | (~old(X!3)) | (~barrel(V!5, X!3)) | (~down(V!5, W!4)) | (~in(V!5, U!6)) | (~seat(X1!2)) | (~furniture(X1!2)) | (~front(X1!2)) | (~fellow(X2!1)) | (~man(X2!1)) | (~young(X2!1)) | (~fellow(X3!0)) | (~man(X3!0)) | (~young(X3!0)) | (~in(X2!1, X1!2)) | (~![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : ((~in(X12, X10)) | (~hollywood(X4)) | (~city(X4)) | (~event(X5)) | (~chevy(X6)) | (~car(X6)) | (~white(X6)) | (~dirty(X6)) | (~old(X6)) | (~street(X7)) | (~way(X7)) | (~lonely(X7)) | (~barrel(X5, X6)) | (~down(X5, X7)) | (~in(X5, X4)) | (~seat(X10)) | (~furniture(X10)) | (~front(X10)) | (~fellow(X11)) | (~man(X11)) | (~young(X11)) | (~fellow(X12)) | (~man(X12)) | (~young(X12)) | (~in(X11, X10)) | (X11 = X12))))) | (~((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(65,plain,
% 0.18/0.40 (((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> ((~((X2!1 = X3!0) | (~in(X3!0, X1!2)) | (~hollywood(U!6)) | (~city(U!6)) | (~event(V!5)) | (~street(W!4)) | (~way(W!4)) | (~lonely(W!4)) | (~chevy(X!3)) | (~car(X!3)) | (~white(X!3)) | (~dirty(X!3)) | (~old(X!3)) | (~barrel(V!5, X!3)) | (~down(V!5, W!4)) | (~in(V!5, U!6)) | (~seat(X1!2)) | (~furniture(X1!2)) | (~front(X1!2)) | (~fellow(X2!1)) | (~man(X2!1)) | (~young(X2!1)) | (~fellow(X3!0)) | (~man(X3!0)) | (~young(X3!0)) | (~in(X2!1, X1!2)) | (~![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : ((~in(X12, X10)) | (~hollywood(X4)) | (~city(X4)) | (~event(X5)) | (~chevy(X6)) | (~car(X6)) | (~white(X6)) | (~dirty(X6)) | (~old(X6)) | (~street(X7)) | (~way(X7)) | (~lonely(X7)) | (~barrel(X5, X6)) | (~down(X5, X7)) | (~in(X5, X4)) | (~seat(X10)) | (~furniture(X10)) | (~front(X10)) | (~fellow(X11)) | (~man(X11)) | (~young(X11)) | (~fellow(X12)) | (~man(X12)) | (~young(X12)) | (~in(X11, X10)) | (X11 = X12))))) | (~((X20!8 = X21!7) | (~in(X21!7, X19!9)) | (~hollywood(X13!13)) | (~city(X13!13)) | (~event(X14!12)) | (~chevy(X15!11)) | (~car(X15!11)) | (~white(X15!11)) | (~dirty(X15!11)) | (~old(X15!11)) | (~street(X16!10)) | (~way(X16!10)) | (~lonely(X16!10)) | (~barrel(X14!12, X15!11)) | (~down(X14!12, X16!10)) | (~in(X14!12, X13!13)) | (~seat(X19!9)) | (~furniture(X19!9)) | (~front(X19!9)) | (~fellow(X20!8)) | (~man(X20!8)) | (~young(X20!8)) | (~fellow(X21!7)) | (~man(X21!7)) | (~young(X21!7)) | (~in(X20!8, X19!9)) | (~![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : ((~in(X30, X28)) | (~hollywood(X22)) | (~city(X22)) | (~event(X23)) | (~in(X23, X22)) | (~seat(X28)) | (~furniture(X28)) | (~front(X28)) | (~fellow(X29)) | (~man(X29)) | (~young(X29)) | (~fellow(X30)) | (~man(X30)) | (~young(X30)) | (~in(X29, X28)) | (X29 = X30) | (~way(X24)) | (~street(X24)) | (~lonely(X24)) | (~chevy(X25)) | (~car(X25)) | (~white(X25)) | (~dirty(X25)) | (~down(X23, X24)) | (~old(X25)) | (~barrel(X23, X25)))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(66,plain,
% 0.18/0.40 (((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> ((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(67,plain,
% 0.18/0.40 (((in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9)) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))) <=> (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(68,plain,
% 0.18/0.40 (((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2)) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) <=> (in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(69,plain,
% 0.18/0.40 ((((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2)) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | ((in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9)) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> ((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[68, 67])).
% 0.18/0.41 tff(70,plain,
% 0.18/0.41 ((((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2)) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | ((in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9)) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> ((in(X3!0, X1!2) & hollywood(U!6) & city(U!6) & event(V!5) & street(W!4) & way(W!4) & lonely(W!4) & chevy(X!3) & car(X!3) & white(X!3) & dirty(X!3) & old(X!3) & barrel(V!5, X!3) & down(V!5, W!4) & in(V!5, U!6) & seat(X1!2) & furniture(X1!2) & front(X1!2) & (~(X2!1 = X3!0)) & fellow(X2!1) & man(X2!1) & young(X2!1) & fellow(X3!0) & man(X3!0) & young(X3!0) & in(X2!1, X1!2) & ![X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (~(in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))) | (in(X21!7, X19!9) & hollywood(X13!13) & city(X13!13) & event(X14!12) & chevy(X15!11) & car(X15!11) & white(X15!11) & dirty(X15!11) & old(X15!11) & street(X16!10) & way(X16!10) & lonely(X16!10) & barrel(X14!12, X15!11) & down(X14!12, X16!10) & in(X14!12, X13!13) & seat(X19!9) & furniture(X19!9) & front(X19!9) & (~(X20!8 = X21!7)) & fellow(X20!8) & man(X20!8) & young(X20!8) & fellow(X21!7) & man(X21!7) & young(X21!7) & in(X20!8, X19!9) & ![X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (~(in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.41 inference(transitivity,[status(thm)],[69, 66])).
% 0.18/0.41 tff(71,plain,
% 0.18/0.41 (((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))) <=> ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(72,plain,
% 0.18/0.41 (((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) <=> ((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(73,plain,
% 0.18/0.41 ((((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))) <=> (((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[72, 71])).
% 0.18/0.41 tff(74,plain,
% 0.18/0.41 ((~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[73])).
% 0.18/0.42 tff(75,plain,
% 0.18/0.42 ((~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(76,plain,
% 0.18/0.42 ((~((?[U: $i, V: $i, W: $i, X: $i, Y: $i, Z: $i, X1: $i, X2: $i, X3: $i] : (((((((((((((((((((((((((((hollywood(U) & city(U)) & event(V)) & street(W)) & way(W)) & lonely(W)) & chevy(X)) & car(X)) & white(X)) & dirty(X)) & old(X)) & barrel(V, X)) & down(V, W)) & in(V, U)) & seat(X1)) & furniture(X1)) & front(X1)) & (~(Y = Z))) & fellow(Y)) & man(Y)) & young(Y)) & fellow(Z)) & man(Z)) & young(Z)) & (Y = X2)) & in(X2, X1)) & (Z = X3)) & in(X3, X1)) => ?[X4: $i, X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X10: $i, X11: $i, X12: $i] : (((((((((((((((((((((((((((hollywood(X4) & city(X4)) & event(X5)) & chevy(X6)) & car(X6)) & white(X6)) & dirty(X6)) & old(X6)) & street(X7)) & way(X7)) & lonely(X7)) & barrel(X5, X6)) & down(X5, X7)) & in(X5, X4)) & seat(X10)) & furniture(X10)) & front(X10)) & (~(X8 = X9))) & fellow(X8)) & man(X8)) & young(X8)) & fellow(X9)) & man(X9)) & young(X9)) & (X8 = X11)) & in(X11, X10)) & (X9 = X12)) & in(X12, X10))) & (?[X13: $i, X14: $i, X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X20: $i, X21: $i] : (((((((((((((((((((((((((((hollywood(X13) & city(X13)) & event(X14)) & chevy(X15)) & car(X15)) & white(X15)) & dirty(X15)) & old(X15)) & street(X16)) & way(X16)) & lonely(X16)) & barrel(X14, X15)) & down(X14, X16)) & in(X14, X13)) & seat(X19)) & furniture(X19)) & front(X19)) & (~(X17 = X18))) & fellow(X17)) & man(X17)) & young(X17)) & fellow(X18)) & man(X18)) & young(X18)) & (X17 = X20)) & in(X20, X19)) & (X18 = X21)) & in(X21, X19)) => ?[X22: $i, X23: $i, X24: $i, X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X30: $i] : (((((((((((((((((((((((((((hollywood(X22) & city(X22)) & event(X23)) & street(X24)) & way(X24)) & lonely(X24)) & chevy(X25)) & car(X25)) & white(X25)) & dirty(X25)) & old(X25)) & barrel(X23, X25)) & down(X23, X24)) & in(X23, X22)) & seat(X28)) & furniture(X28)) & front(X28)) & (~(X26 = X27))) & fellow(X26)) & man(X26)) & young(X26)) & fellow(X27)) & man(X27)) & young(X27)) & (X26 = X29)) & in(X29, X28)) & (X27 = X30)) & in(X30, X28))))) <=> (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28)))))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(77,axiom,(~((?[U: $i, V: $i, W: $i, X: $i, Y: $i, Z: $i, X1: $i, X2: $i, X3: $i] : (((((((((((((((((((((((((((hollywood(U) & city(U)) & event(V)) & street(W)) & way(W)) & lonely(W)) & chevy(X)) & car(X)) & white(X)) & dirty(X)) & old(X)) & barrel(V, X)) & down(V, W)) & in(V, U)) & seat(X1)) & furniture(X1)) & front(X1)) & (~(Y = Z))) & fellow(Y)) & man(Y)) & young(Y)) & fellow(Z)) & man(Z)) & young(Z)) & (Y = X2)) & in(X2, X1)) & (Z = X3)) & in(X3, X1)) => ?[X4: $i, X5: $i, X6: $i, X7: $i, X8: $i, X9: $i, X10: $i, X11: $i, X12: $i] : (((((((((((((((((((((((((((hollywood(X4) & city(X4)) & event(X5)) & chevy(X6)) & car(X6)) & white(X6)) & dirty(X6)) & old(X6)) & street(X7)) & way(X7)) & lonely(X7)) & barrel(X5, X6)) & down(X5, X7)) & in(X5, X4)) & seat(X10)) & furniture(X10)) & front(X10)) & (~(X8 = X9))) & fellow(X8)) & man(X8)) & young(X8)) & fellow(X9)) & man(X9)) & young(X9)) & (X8 = X11)) & in(X11, X10)) & (X9 = X12)) & in(X12, X10))) & (?[X13: $i, X14: $i, X15: $i, X16: $i, X17: $i, X18: $i, X19: $i, X20: $i, X21: $i] : (((((((((((((((((((((((((((hollywood(X13) & city(X13)) & event(X14)) & chevy(X15)) & car(X15)) & white(X15)) & dirty(X15)) & old(X15)) & street(X16)) & way(X16)) & lonely(X16)) & barrel(X14, X15)) & down(X14, X16)) & in(X14, X13)) & seat(X19)) & furniture(X19)) & front(X19)) & (~(X17 = X18))) & fellow(X17)) & man(X17)) & young(X17)) & fellow(X18)) & man(X18)) & young(X18)) & (X17 = X20)) & in(X20, X19)) & (X18 = X21)) & in(X21, X19)) => ?[X22: $i, X23: $i, X24: $i, X25: $i, X26: $i, X27: $i, X28: $i, X29: $i, X30: $i] : (((((((((((((((((((((((((((hollywood(X22) & city(X22)) & event(X23)) & street(X24)) & way(X24)) & lonely(X24)) & chevy(X25)) & car(X25)) & white(X25)) & dirty(X25)) & old(X25)) & barrel(X23, X25)) & down(X23, X24)) & in(X23, X22)) & seat(X28)) & furniture(X28)) & front(X28)) & (~(X26 = X27))) & fellow(X26)) & man(X26)) & young(X26)) & fellow(X27)) & man(X27)) & young(X27)) & (X26 = X29)) & in(X29, X28)) & (X27 = X30)) & in(X30, X28))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','co1')).
% 0.18/0.42 tff(78,plain,
% 0.18/0.42 (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.18/0.42 tff(79,plain,
% 0.18/0.42 (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[78, 74])).
% 0.18/0.43 tff(80,plain,
% 0.18/0.43 (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.18/0.43 tff(81,plain,
% 0.18/0.43 (~(((~?[U: $i, V: $i, W: $i, X: $i, X1: $i, X2: $i, X3: $i] : (in(X3, X1) & hollywood(U) & city(U) & event(V) & street(W) & way(W) & lonely(W) & chevy(X) & car(X) & white(X) & dirty(X) & old(X) & barrel(V, X) & down(V, W) & in(V, U) & seat(X1) & furniture(X1) & front(X1) & (~(X2 = X3)) & fellow(X2) & man(X2) & young(X2) & fellow(X3) & man(X3) & young(X3) & in(X2, X1))) | ?[X4: $i, X5: $i, X6: $i, X7: $i, X10: $i, X11: $i, X12: $i] : (in(X12, X10) & hollywood(X4) & city(X4) & event(X5) & chevy(X6) & car(X6) & white(X6) & dirty(X6) & old(X6) & street(X7) & way(X7) & lonely(X7) & barrel(X5, X6) & down(X5, X7) & in(X5, X4) & seat(X10) & furniture(X10) & front(X10) & (~(X11 = X12)) & fellow(X11) & man(X11) & young(X11) & fellow(X12) & man(X12) & young(X12) & in(X11, X10))) & ((~?[X13: $i, X14: $i, X15: $i, X16: $i, X19: $i, X20: $i, X21: $i] : (in(X21, X19) & hollywood(X13) & city(X13) & event(X14) & chevy(X15) & car(X15) & white(X15) & dirty(X15) & old(X15) & street(X16) & way(X16) & lonely(X16) & barrel(X14, X15) & down(X14, X16) & in(X14, X13) & seat(X19) & furniture(X19) & front(X19) & (~(X20 = X21)) & fellow(X20) & man(X20) & young(X20) & fellow(X21) & man(X21) & young(X21) & in(X20, X19))) | ?[X22: $i, X23: $i, X24: $i, X25: $i, X28: $i, X29: $i, X30: $i] : (in(X30, X28) & hollywood(X22) & city(X22) & event(X23) & street(X24) & way(X24) & lonely(X24) & chevy(X25) & car(X25) & white(X25) & dirty(X25) & old(X25) & barrel(X23, X25) & down(X23, X24) & in(X23, X22) & seat(X28) & furniture(X28) & front(X28) & (~(X29 = X30)) & fellow(X29) & man(X29) & young(X29) & fellow(X30) & man(X30) & young(X30) & in(X29, X28))))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[80, 74])).
% 0.18/0.43 unexpected number of arguments: (let ((a!1 (exists ((U $i) (V $i) (W $i) (X $i) (X1 $i) (X2 $i) (X3 $i))
% 0.18/0.43 (and (in X3 X1)
% 0.18/0.43 (hollywood U)
% 0.18/0.43 (city U)
% 0.18/0.43 (event V)
% 0.18/0.43 (street W)
% 0.18/0.43 (way W)
% 0.18/0.43 (lonely W)
% 0.18/0.43 (chevy X)
% 0.18/0.43 (car X)
% 0.18/0.43 (white X)
% 0.18/0.43 (dirty X)
% 0.18/0.43 (old X)
% 0.18/0.43 (barrel V X)
% 0.18/0.43 (down V W)
% 0.18/0.43 (in V U)
% 0.18/0.43 (seat X1)
% 0.18/0.43 (furniture X1)
% 0.18/0.43 (front X1)
% 0.18/0.43 (not (= X2 X3))
% 0.18/0.43 (fellow X2)
% 0.18/0.43 (man X2)
% 0.18/0.43 (young X2)
% 0.18/0.43 (fellow X3)
% 0.18/0.43 (man X3)
% 0.18/0.43 (young X3)
% 0.18/0.43 (in X2 X1))))
% 0.18/0.43 (a!2 (and (in X3!0 X1!2)
% 0.18/0.43 (hollywood U!6)
% 0.18/0.43 (city U!6)
% 0.18/0.43 (event V!5)
% 0.18/0.43 (street W!4)
% 0.18/0.43 (way W!4)
% 0.18/0.43 (lonely W!4)
% 0.18/0.43 (chevy X!3)
% 0.18/0.43 (car X!3)
% 0.18/0.43 (white X!3)
% 0.18/0.43 (dirty X!3)
% 0.18/0.43 (old X!3)
% 0.18/0.43 (barrel V!5 X!3)
% 0.18/0.43 (down V!5 W!4)
% 0.18/0.43 (in V!5 U!6)
% 0.18/0.43 (seat X1!2)
% 0.18/0.43 (furniture X1!2)
% 0.18/0.43 (front X1!2)
% 0.18/0.43 (not (= X2!1 X3!0))
% 0.18/0.43 (fellow X2!1)
% 0.18/0.43 (man X2!1)
% 0.18/0.43 (young X2!1)
% 0.18/0.43 (fellow X3!0)
% 0.18/0.43 (man X3!0)
% 0.18/0.43 (young X3!0)
% 0.18/0.43 (in X2!1 X1!2)))
% 0.18/0.43 (a!4 (lambda ((X4 $i) (X5 $i) (X6 $i) (X7 $i) (X10 $i) (X11 $i) (X12 $i))
% 0.18/0.43 (let ((a!1 (and (in X12 X10)
% 0.18/0.43 (hollywood X4)
% 0.18/0.43 (city X4)
% 0.18/0.43 (event X5)
% 0.18/0.43 (chevy X6)
% 0.18/0.43 (car X6)
% 0.18/0.43 (white X6)
% 0.18/0.43 (dirty X6)
% 0.18/0.43 (old X6)
% 0.18/0.43 (street X7)
% 0.18/0.43 (way X7)
% 0.18/0.43 (lonely X7)
% 0.18/0.43 (barrel X5 X6)
% 0.18/0.43 (down X5 X7)
% 0.18/0.43 (in X5 X4)
% 0.18/0.43 (seat X10)
% 0.18/0.43 (furniture X10)
% 0.18/0.43 (front X10)
% 0.18/0.43 (not (= X11 X12))
% 0.18/0.43 (fellow X11)
% 0.18/0.43 (man X11)
% 0.18/0.43 (young X11)
% 0.18/0.43 (fellow X12)
% 0.18/0.43 (man X12)
% 0.18/0.43 (young X12)
% 0.18/0.43 (in X11 X10))))
% 0.18/0.43 (refl (~ (not a!1) (not a!1))))))
% 0.18/0.43 (a!5 (exists ((X4 $i) (X5 $i) (X6 $i) (X7 $i) (X10 $i) (X11 $i) (X12 $i))
% 0.18/0.43 (and (in X12 X10)
% 0.18/0.43 (hollywood X4)
% 0.18/0.43 (city X4)
% 0.18/0.43 (event X5)
% 0.18/0.43 (chevy X6)
% 0.18/0.43 (car X6)
% 0.18/0.43 (white X6)
% 0.18/0.43 (dirty X6)
% 0.18/0.43 (old X6)
% 0.18/0.43 (street X7)
% 0.18/0.43 (way X7)
% 0.18/0.43 (lonely X7)
% 0.18/0.43 (barrel X5 X6)
% 0.18/0.43 (down X5 X7)
% 0.18/0.43 (in X5 X4)
% 0.18/0.43 (seat X10)
% 0.18/0.43 (furniture X10)
% 0.18/0.43 (front X10)
% 0.18/0.43 (not (= X11 X12))
% 0.18/0.43 (fellow X11)
% 0.18/0.43 (man X11)
% 0.18/0.43 (young X11)
% 0.18/0.43 (fellow X12)
% 0.18/0.43 (man X12)
% 0.18/0.43 (young X12)
% 0.18/0.43 (in X11 X10))))
% 0.18/0.43 (a!6 (forall ((X4 $i) (X5 $i) (X6 $i) (X7 $i) (X10 $i) (X11 $i) (X12 $i))
% 0.18/0.43 (let ((a!1 (and (in X12 X10)
% 0.18/0.43 (hollywood X4)
% 0.18/0.43 (city X4)
% 0.18/0.43 (event X5)
% 0.18/0.43 (chevy X6)
% 0.18/0.43 (car X6)
% 0.18/0.43 (white X6)
% 0.18/0.43 (dirty X6)
% 0.18/0.43 (old X6)
% 0.18/0.43 (street X7)
% 0.18/0.43 (way X7)
% 0.18/0.43 (lonely X7)
% 0.18/0.43 (barrel X5 X6)
% 0.18/0.43 (down X5 X7)
% 0.18/0.43 (in X5 X4)
% 0.18/0.43 (seat X10)
% 0.18/0.43 (furniture X10)
% 0.18/0.43 (front X10)
% 0.18/0.43 (not (= X11 X12))
% 0.18/0.43 (fellow X11)
% 0.18/0.43 (man X11)
% 0.18/0.43 (young X11)
% 0.18/0.43 (fellow X12)
% 0.18/0.43 (man X12)
% 0.18/0.43 (young X12)
% 0.18/0.43 (in X11 X10))))
% 0.18/0.43 (not a!1))))
% 0.18/0.43 (a!9 (exists ((X13 $i)
% 0.18/0.43 (X14 $i)
% 0.18/0.43 (X15 $i)
% 0.18/0.43 (X16 $i)
% 0.18/0.43 (X19 $i)
% 0.18/0.43 (X20 $i)
% 0.18/0.43 (X21 $i))
% 0.18/0.43 (and (in X21 X19)
% 0.18/0.43 (hollywood X13)
% 0.18/0.43 (city X13)
% 0.18/0.43 (event X14)
% 0.18/0.43 (chevy X15)
% 0.18/0.43 (car X15)
% 0.18/0.43 (white X15)
% 0.18/0.43 (dirty X15)
% 0.18/0.43 (old X15)
% 0.18/0.43 (street X16)
% 0.18/0.43 (way X16)
% 0.18/0.43 (lonely X16)
% 0.18/0.43 (barrel X14 X15)
% 0.18/0.43 (down X14 X16)
% 0.18/0.43 (in X14 X13)
% 0.18/0.43 (seat X19)
% 0.18/0.43 (furniture X19)
% 0.18/0.43 (front X19)
% 0.18/0.43 (not (= X20 X21))
% 0.18/0.43 (fellow X20)
% 0.18/0.43 (man X20)
% 0.18/0.43 (young X20)
% 0.18/0.43 (fellow X21)
% 0.18/0.43 (man X21)
% 0.18/0.43 (young X21)
% 0.18/0.43 (in X20 X19))))
% 0.18/0.43 (a!10 (and (in X21!7 X19!9)
% 0.18/0.43 (hollywood X13!13)
% 0.18/0.43 (city X13!13)
% 0.18/0.43 (event X14!12)
% 0.18/0.43 (chevy X15!11)
% 0.18/0.43 (car X15!11)
% 0.18/0.43 (white X15!11)
% 0.18/0.43 (dirty X15!11)
% 0.18/0.43 (old X15!11)
% 0.18/0.43 (street X16!10)
% 0.18/0.43 (way X16!10)
% 0.18/0.43 (lonely X16!10)
% 0.18/0.43 (barrel X14!12 X15!11)
% 0.18/0.43 (down X14!12 X16!10)
% 0.18/0.43 (in X14!12 X13!13)
% 0.18/0.43 (seat X19!9)
% 0.18/0.43 (furniture X19!9)
% 0.18/0.43 (front X19!9)
% 0.18/0.43 (not (= X20!8 X21!7))
% 0.18/0.43 (fellow X20!8)
% 0.18/0.43 (man X20!8)
% 0.18/0.43 (young X20!8)
% 0.18/0.43 (fellow X21!7)
% 0.18/0.43 (man X21!7)
% 0.18/0.43 (young X21!7)
% 0.18/0.43 (in X20!8 X19!9)))
% 0.18/0.43 (a!12 (lambda ((X22 $i)
% 0.18/0.43 (X23 $i)
% 0.18/0.43 (X24 $i)
% 0.18/0.43 (X25 $i)
% 0.18/0.43 (X28 $i)
% 0.18/0.43 (X29 $i)
% 0.18/0.43 (X30 $i))
% 0.18/0.43 (let ((a!1 (and (in X30 X28)
% 0.18/0.43 (hollywood X22)
% 0.18/0.43 (city X22)
% 0.18/0.43 (event X23)
% 0.18/0.43 (street X24)
% 0.18/0.43 (way X24)
% 0.18/0.43 (lonely X24)
% 0.18/0.43 (chevy X25)
% 0.18/0.43 (car X25)
% 0.18/0.43 (white X25)
% 0.18/0.43 (dirty X25)
% 0.18/0.43 (old X25)
% 0.18/0.43 (barrel X23 X25)
% 0.18/0.43 (down X23 X24)
% 0.18/0.43 (in X23 X22)
% 0.18/0.43 (seat X28)
% 0.18/0.43 (furniture X28)
% 0.18/0.43 (front X28)
% 0.18/0.43 (not (= X29 X30))
% 0.18/0.43 (fellow X29)
% 0.18/0.43 (man X29)
% 0.18/0.43 (young X29)
% 0.18/0.43 (fellow X30)
% 0.18/0.43 (man X30)
% 0.18/0.43 (young X30)
% 0.18/0.43 (in X29 X28))))
% 0.18/0.43 (refl (~ (not a!1) (not a!1))))))
% 0.18/0.43 (a!13 (exists ((X22 $i)
% 0.18/0.43 (X23 $i)
% 0.18/0.43 (X24 $i)
% 0.18/0.43 (X25 $i)
% 0.18/0.43 (X28 $i)
% 0.18/0.43 (X29 $i)
% 0.18/0.43 (X30 $i))
% 0.18/0.43 (and (in X30 X28)
% 0.18/0.43 (hollywood X22)
% 0.18/0.43 (city X22)
% 0.18/0.43 (event X23)
% 0.18/0.43 (street X24)
% 0.18/0.43 (way X24)
% 0.18/0.43 (lonely X24)
% 0.18/0.43 (chevy X25)
% 0.18/0.43 (car X25)
% 0.18/0.43 (white X25)
% 0.18/0.43 (dirty X25)
% 0.18/0.43 (old X25)
% 0.18/0.43 (barrel X23 X25)
% 0.18/0.43 (down X23 X24)
% 0.18/0.43 (in X23 X22)
% 0.18/0.43 (seat X28)
% 0.18/0.43 (furniture X28)
% 0.18/0.43 (front X28)
% 0.18/0.43 (not (= X29 X30))
% 0.18/0.43 (fellow X29)
% 0.18/0.43 (man X29)
% 0.18/0.43 (young X29)
% 0.18/0.43 (fellow X30)
% 0.18/0.43 (man X30)
% 0.18/0.43 (young X30)
% 0.18/0.43 (in X29 X28))))
% 0.18/0.43 (a!14 (forall ((X22 $i)
% 0.18/0.43 (X23 $i)
% 0.18/0.43 (X24 $i)
% 0.18/0.43 (X25 $i)
% 0.18/0.43 (X28 $i)
% 0.18/0.43 (X29 $i)
% 0.18/0.43 (X30 $i))
% 0.18/0.43 (let ((a!1 (and (in X30 X28)
% 0.18/0.43 (hollywood X22)
% 0.18/0.43 (city X22)
% 0.18/0.43 (event X23)
% 0.18/0.43 (street X24)
% 0.18/0.43 (way X24)
% 0.18/0.43 (lonely X24)
% 0.18/0.43 (chevy X25)
% 0.18/0.43 (car X25)
% 0.18/0.43 (white X25)
% 0.18/0.43 (dirty X25)
% 0.18/0.43 (old X25)
% 0.18/0.43 (barrel X23 X25)
% 0.18/0.43 (down X23 X24)
% 0.18/0.43 (in X23 X22)
% 0.18/0.43 (seat X28)
% 0.18/0.43 (furniture X28)
% 0.18/0.43 (front X28)
% 0.18/0.43 (not (= X29 X30))
% 0.18/0.43 (fellow X29)
% 0.18/0.43 (man X29)
% 0.18/0.43 (young X29)
% 0.18/0.43 (fellow X30)
% 0.18/0.43 (man X30)
% 0.18/0.43 (young X30)
% 0.18/0.43 (in X29 X28))))
% 0.18/0.43 (not a!1)))))
% 0.18/0.43 (let ((a!3 (nnf-neg (sk (~ a!1 a!2)) (~ (not (not a!1)) a!2)))
% 0.18/0.43 (a!7 (~ (not (or (not a!1) a!5)) (and a!2 a!6)))
% 0.18/0.43 (a!11 (nnf-neg (sk (~ a!9 a!10)) (~ (not (not a!9)) a!10)))
% 0.18/0.43 (a!15 (~ (not (or (not a!9) a!13)) (and a!10 a!14)))
% 0.18/0.43 (a!17 (not (and (or (not a!1) a!5) (or (not a!9) a!13)))))
% 0.18/0.43 (let ((a!8 (nnf-neg a!3 (nnf-neg (proof-bind a!4) (~ (not a!5) a!6)) a!7))
% 0.18/0.43 (a!16 (nnf-neg a!11 (nnf-neg (proof-bind a!12) (~ (not a!13) a!14)) a!15)))
% 0.18/0.43 (nnf-neg a!8 a!16 (~ a!17 (or (and a!2 a!6) (and a!10 a!14)))))))
% 0.18/0.43 Proof display could not be completed: unexpected number of arguments
% 0.18/0.44 % E exiting
%------------------------------------------------------------------------------