%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP038+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:47:59 PM UTC 2025
% Result : CounterSatisfiable 5.40s 2.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NLP038+1 : TPTP v9.0.0. Released v2.4.0.
% 0.00/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.09/0.30 % Computer : n004.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Apr 8 08:13:07 EDT 2025
% 0.09/0.30 % CPUTime :
% 5.40/2.25
% 5.40/2.25 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.40/2.25
% 5.40/2.25 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.40/2.26 %$ with > member > at > agent > young > unisex > three > thing > table > substance_matter > specific > sit > singleton > set > present > organism > object > nonliving > nonexistent > multiple > meat > man > male > living > instrumentality > impartial > human_person > human > hamburger > guy > group > furniture > food > existent > eventuality > event > entity > burger > artifact > animate > actual_world > #nlpp > #skF_8 > #skF_7 > #skF_3 > #skF_5 > #skF_6 > #skF_1 > #skF_2 > #skF_9 > #skF_4
% 5.40/2.26
% 5.40/2.26 %Foreground sorts:
% 5.40/2.26
% 5.40/2.26
% 5.40/2.26 %Background operators:
% 5.40/2.26
% 5.40/2.26
% 5.40/2.26 %Foreground operators:
% 5.40/2.26 tff(nonliving, type, nonliving: ($i * $i) > $o).
% 5.40/2.26 tff(guy, type, guy: ($i * $i) > $o).
% 5.40/2.26 tff(member, type, member: ($i * $i * $i) > $o).
% 5.40/2.26 tff(living, type, living: ($i * $i) > $o).
% 5.40/2.26 tff(meat, type, meat: ($i * $i) > $o).
% 5.40/2.26 tff(human_person, type, human_person: ($i * $i) > $o).
% 5.40/2.26 tff(present, type, present: ($i * $i) > $o).
% 5.40/2.26 tff(three, type, three: ($i * $i) > $o).
% 5.40/2.26 tff(entity, type, entity: ($i * $i) > $o).
% 5.40/2.26 tff(substance_matter, type, substance_matter: ($i * $i) > $o).
% 5.40/2.26 tff(eventuality, type, eventuality: ($i * $i) > $o).
% 5.40/2.26 tff(existent, type, existent: ($i * $i) > $o).
% 5.40/2.26 tff(singleton, type, singleton: ($i * $i) > $o).
% 5.40/2.26 tff(young, type, young: ($i * $i) > $o).
% 5.40/2.26 tff(male, type, male: ($i * $i) > $o).
% 5.40/2.26 tff(burger, type, burger: ($i * $i) > $o).
% 5.40/2.26 tff(multiple, type, multiple: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_8', type, '#skF_8': $i > $i).
% 5.40/2.26 tff(organism, type, organism: ($i * $i) > $o).
% 5.40/2.26 tff(animate, type, animate: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_7', type, '#skF_7': $i).
% 5.40/2.26 tff('#skF_3', type, '#skF_3': ($i * $i) > $i).
% 5.40/2.26 tff(actual_world, type, actual_world: $i > $o).
% 5.40/2.26 tff(agent, type, agent: ($i * $i * $i) > $o).
% 5.40/2.26 tff(instrumentality, type, instrumentality: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_5', type, '#skF_5': $i).
% 5.40/2.26 tff(group, type, group: ($i * $i) > $o).
% 5.40/2.26 tff(artifact, type, artifact: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_6', type, '#skF_6': $i).
% 5.40/2.26 tff(food, type, food: ($i * $i) > $o).
% 5.40/2.26 tff(hamburger, type, hamburger: ($i * $i) > $o).
% 5.40/2.26 tff(event, type, event: ($i * $i) > $o).
% 5.40/2.26 tff(nonexistent, type, nonexistent: ($i * $i) > $o).
% 5.40/2.26 tff(thing, type, thing: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_1', type, '#skF_1': ($i * $i * $i * $i * $i) > $i).
% 5.40/2.26 tff(human, type, human: ($i * $i) > $o).
% 5.40/2.26 tff(man, type, man: ($i * $i) > $o).
% 5.40/2.26 tff(table, type, table: ($i * $i) > $o).
% 5.40/2.26 tff(furniture, type, furniture: ($i * $i) > $o).
% 5.40/2.26 tff(unisex, type, unisex: ($i * $i) > $o).
% 5.40/2.26 tff(set, type, set: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_2', type, '#skF_2': ($i * $i) > $i).
% 5.40/2.26 tff(impartial, type, impartial: ($i * $i) > $o).
% 5.40/2.26 tff(object, type, object: ($i * $i) > $o).
% 5.40/2.26 tff(specific, type, specific: ($i * $i) > $o).
% 5.40/2.26 tff(at, type, at: ($i * $i * $i) > $o).
% 5.40/2.26 tff('#skF_9', type, '#skF_9': ($i * $i) > $i).
% 5.40/2.26 tff(sit, type, sit: ($i * $i) > $o).
% 5.40/2.26 tff('#skF_4', type, '#skF_4': ($i * $i) > $i).
% 5.40/2.26 tff(with, type, with: ($i * $i * $i) > $o).
% 5.40/2.26
% 5.40/2.26 %Saturated clause set:
% 5.40/2.26 tff(c_775, plain, (![X_203, X_445, Y_447, W_448]: (agent('#skF_5', '#skF_9'(X_203, '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448)), X_203) | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_776, plain, (![X_203, X_445, Y_447, W_448]: (at('#skF_5', '#skF_9'(X_203, '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448)), '#skF_6') | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_895, plain, (![X_501, Y_503, W_504, X_502]: (~member('#skF_5', X_501, '#skF_7') | three('#skF_5', '#skF_8'(X_501)) | Y_503=W_504 | Y_503=X_502 | ~member('#skF_5', Y_503, '#skF_8'(X_501)) | X_502=W_504 | ~member('#skF_5', X_502, '#skF_8'(X_501)) | ~member('#skF_5', W_504, '#skF_8'(X_501)) | ~artifact('#skF_5', '#skF_9'(X_501, '#skF_1'('#skF_8'(X_501), X_502, '#skF_5', Y_503, W_504)))))).
% 5.40/2.26 tff(c_894, plain, (![X_501, Y_503, W_504, X_502]: (~member('#skF_5', X_501, '#skF_7') | three('#skF_5', '#skF_8'(X_501)) | Y_503=W_504 | Y_503=X_502 | ~member('#skF_5', Y_503, '#skF_8'(X_501)) | X_502=W_504 | ~member('#skF_5', X_502, '#skF_8'(X_501)) | ~member('#skF_5', W_504, '#skF_8'(X_501)) | ~burger('#skF_5', '#skF_9'(X_501, '#skF_1'('#skF_8'(X_501), X_502, '#skF_5', Y_503, W_504)))))).
% 5.40/2.26 tff(c_881, plain, (![X_493, X_494, Y_495, W_496]: (~entity('#skF_5', '#skF_9'(X_493, '#skF_1'('#skF_8'(X_493), X_494, '#skF_5', Y_495, W_496))) | ~member('#skF_5', X_493, '#skF_7') | three('#skF_5', '#skF_8'(X_493)) | Y_495=W_496 | Y_495=X_494 | ~member('#skF_5', Y_495, '#skF_8'(X_493)) | X_494=W_496 | ~member('#skF_5', X_494, '#skF_8'(X_493)) | ~member('#skF_5', W_496, '#skF_8'(X_493))))).
% 5.40/2.26 tff(c_779, plain, (![X_203, X_445, Y_447, W_448]: (sit('#skF_5', '#skF_9'(X_203, '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448))) | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_777, plain, (![X_203, X_445, Y_447, W_448]: (event('#skF_5', '#skF_9'(X_203, '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448))) | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_875, plain, (![X_485, X_486, Y_487, W_488]: (~animate('#skF_5', '#skF_1'('#skF_8'(X_485), X_486, '#skF_5', Y_487, W_488)) | ~member('#skF_5', X_485, '#skF_7') | three('#skF_5', '#skF_8'(X_485)) | Y_487=W_488 | Y_487=X_486 | ~member('#skF_5', Y_487, '#skF_8'(X_485)) | X_486=W_488 | ~member('#skF_5', X_486, '#skF_8'(X_485)) | ~member('#skF_5', W_488, '#skF_8'(X_485))))).
% 5.40/2.26 tff(c_869, plain, (![X_477, X_478, Y_479, W_480]: (burger('#skF_5', '#skF_1'('#skF_8'(X_477), X_478, '#skF_5', Y_479, W_480)) | ~member('#skF_5', X_477, '#skF_7') | three('#skF_5', '#skF_8'(X_477)) | Y_479=W_480 | Y_479=X_478 | ~member('#skF_5', Y_479, '#skF_8'(X_477)) | X_478=W_480 | ~member('#skF_5', X_478, '#skF_8'(X_477)) | ~member('#skF_5', W_480, '#skF_8'(X_477))))).
% 5.40/2.26 tff(c_778, plain, (![X_203, X_445, Y_447, W_448]: (present('#skF_5', '#skF_9'(X_203, '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448))) | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_780, plain, (![X_203, X_445, Y_447, W_448]: (hamburger('#skF_5', '#skF_1'('#skF_8'(X_203), X_445, '#skF_5', Y_447, W_448)) | ~member('#skF_5', X_203, '#skF_7') | three('#skF_5', '#skF_8'(X_203)) | Y_447=W_448 | Y_447=X_445 | ~member('#skF_5', Y_447, '#skF_8'(X_203)) | X_445=W_448 | ~member('#skF_5', X_445, '#skF_8'(X_203)) | ~member('#skF_5', W_448, '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_545, plain, (![X_203]: (agent('#skF_5', '#skF_9'(X_203, '#skF_2'('#skF_5', '#skF_8'(X_203))), X_203) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_440, plain, (![X_203]: (at('#skF_5', '#skF_9'(X_203, '#skF_4'('#skF_5', '#skF_8'(X_203))), '#skF_6') | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_502, plain, (![X_382]: (agent('#skF_5', '#skF_9'(X_382, '#skF_3'('#skF_5', '#skF_8'(X_382))), X_382) | ~member('#skF_5', X_382, '#skF_7') | ~three('#skF_5', '#skF_8'(X_382))))).
% 5.40/2.26 tff(c_843, plain, (![X_464]: (~member('#skF_5', X_464, '#skF_7') | ~three('#skF_5', '#skF_8'(X_464)) | ~burger('#skF_5', '#skF_9'(X_464, '#skF_2'('#skF_5', '#skF_8'(X_464))))))).
% 5.40/2.26 tff(c_546, plain, (![X_203]: (at('#skF_5', '#skF_9'(X_203, '#skF_2'('#skF_5', '#skF_8'(X_203))), '#skF_6') | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.26 tff(c_835, plain, (![X_463]: (~member('#skF_5', X_463, '#skF_7') | ~three('#skF_5', '#skF_8'(X_463)) | ~artifact('#skF_5', '#skF_9'(X_463, '#skF_3'('#skF_5', '#skF_8'(X_463))))))).
% 5.40/2.26 tff(c_834, plain, (![X_463]: (~member('#skF_5', X_463, '#skF_7') | ~three('#skF_5', '#skF_8'(X_463)) | ~burger('#skF_5', '#skF_9'(X_463, '#skF_3'('#skF_5', '#skF_8'(X_463))))))).
% 5.40/2.26 tff(c_853, plain, (![X_465]: (~member('#skF_5', X_465, '#skF_7') | ~three('#skF_5', '#skF_8'(X_465)) | ~artifact('#skF_5', '#skF_9'(X_465, '#skF_4'('#skF_5', '#skF_8'(X_465))))))).
% 5.40/2.26 tff(c_394, plain, (![X_356]: (at('#skF_5', '#skF_9'(X_356, '#skF_3'('#skF_5', '#skF_8'(X_356))), '#skF_6') | ~member('#skF_5', X_356, '#skF_7') | ~three('#skF_5', '#skF_8'(X_356))))).
% 5.40/2.26 tff(c_852, plain, (![X_465]: (~member('#skF_5', X_465, '#skF_7') | ~three('#skF_5', '#skF_8'(X_465)) | ~burger('#skF_5', '#skF_9'(X_465, '#skF_4'('#skF_5', '#skF_8'(X_465))))))).
% 5.40/2.26 tff(c_844, plain, (![X_464]: (~member('#skF_5', X_464, '#skF_7') | ~three('#skF_5', '#skF_8'(X_464)) | ~artifact('#skF_5', '#skF_9'(X_464, '#skF_2'('#skF_5', '#skF_8'(X_464))))))).
% 5.40/2.27 tff(c_812, plain, (![X_456]: (~entity('#skF_5', '#skF_9'(X_456, '#skF_4'('#skF_5', '#skF_8'(X_456)))) | ~member('#skF_5', X_456, '#skF_7') | ~three('#skF_5', '#skF_8'(X_456))))).
% 5.40/2.27 tff(c_807, plain, (![X_455]: (~entity('#skF_5', '#skF_9'(X_455, '#skF_2'('#skF_5', '#skF_8'(X_455)))) | ~member('#skF_5', X_455, '#skF_7') | ~three('#skF_5', '#skF_8'(X_455))))).
% 5.40/2.27 tff(c_796, plain, (![X_452]: (~entity('#skF_5', '#skF_9'(X_452, '#skF_3'('#skF_5', '#skF_8'(X_452)))) | ~member('#skF_5', X_452, '#skF_7') | ~three('#skF_5', '#skF_8'(X_452))))).
% 5.40/2.27 tff(c_501, plain, (![X_382]: (agent('#skF_5', '#skF_9'(X_382, '#skF_4'('#skF_5', '#skF_8'(X_382))), X_382) | ~member('#skF_5', X_382, '#skF_7') | ~three('#skF_5', '#skF_8'(X_382))))).
% 5.40/2.27 tff(c_548, plain, (![X_203]: (present('#skF_5', '#skF_9'(X_203, '#skF_2'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_326, plain, (![X_203]: (present('#skF_5', '#skF_9'(X_203, '#skF_3'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_442, plain, (![X_203]: (present('#skF_5', '#skF_9'(X_203, '#skF_4'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_549, plain, (![X_203]: (sit('#skF_5', '#skF_9'(X_203, '#skF_2'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_443, plain, (![X_203]: (sit('#skF_5', '#skF_9'(X_203, '#skF_4'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_441, plain, (![X_203]: (event('#skF_5', '#skF_9'(X_203, '#skF_4'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_547, plain, (![X_203]: (event('#skF_5', '#skF_9'(X_203, '#skF_2'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_327, plain, (![X_203]: (sit('#skF_5', '#skF_9'(X_203, '#skF_3'('#skF_5', '#skF_8'(X_203)))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_789, plain, (![X_449]: (~animate('#skF_5', '#skF_4'('#skF_5', '#skF_8'(X_449))) | ~member('#skF_5', X_449, '#skF_7') | ~three('#skF_5', '#skF_8'(X_449))))).
% 5.40/2.27 tff(c_345, plain, (![X_340]: (event('#skF_5', '#skF_9'(X_340, '#skF_3'('#skF_5', '#skF_8'(X_340)))) | ~member('#skF_5', X_340, '#skF_7') | ~three('#skF_5', '#skF_8'(X_340))))).
% 5.40/2.27 tff(c_733, plain, (![X_442]: (~animate('#skF_5', '#skF_3'('#skF_5', '#skF_8'(X_442))) | ~member('#skF_5', X_442, '#skF_7') | ~three('#skF_5', '#skF_8'(X_442))))).
% 5.40/2.27 tff(c_738, plain, (![X_443]: (~animate('#skF_5', '#skF_2'('#skF_5', '#skF_8'(X_443))) | ~member('#skF_5', X_443, '#skF_7') | ~three('#skF_5', '#skF_8'(X_443))))).
% 5.40/2.27 tff(c_725, plain, (![X_438]: (burger('#skF_5', '#skF_4'('#skF_5', '#skF_8'(X_438))) | ~member('#skF_5', X_438, '#skF_7') | ~three('#skF_5', '#skF_8'(X_438))))).
% 5.40/2.27 tff(c_102, plain, (![V_82, Y_125, X_121, W_113, U_81]: (member(U_81, '#skF_1'(V_82, X_121, U_81, Y_125, W_113), V_82) | three(U_81, V_82) | Y_125=W_113 | Y_125=X_121 | ~member(U_81, Y_125, V_82) | X_121=W_113 | ~member(U_81, X_121, V_82) | ~member(U_81, W_113, V_82)))).
% 5.40/2.27 tff(c_682, plain, (![X_423]: (burger('#skF_5', '#skF_2'('#skF_5', '#skF_8'(X_423))) | ~member('#skF_5', X_423, '#skF_7') | ~three('#skF_5', '#skF_8'(X_423))))).
% 5.40/2.27 tff(c_573, plain, (![X_390]: (burger('#skF_5', '#skF_3'('#skF_5', '#skF_8'(X_390))) | ~member('#skF_5', X_390, '#skF_7') | ~three('#skF_5', '#skF_8'(X_390))))).
% 5.40/2.27 tff(c_719, plain, (![X_437]: (~member('#skF_5', X_437, '#skF_7') | ~burger('#skF_5', '#skF_8'(X_437))))).
% 5.40/2.27 tff(c_720, plain, (![X_437]: (~member('#skF_5', X_437, '#skF_7') | ~artifact('#skF_5', '#skF_8'(X_437))))).
% 5.40/2.27 tff(c_652, plain, (![X_409]: (~member('#skF_5', X_409, '#skF_7') | ~event('#skF_5', '#skF_8'(X_409))))).
% 5.40/2.27 tff(c_444, plain, (![X_203]: (hamburger('#skF_5', '#skF_4'('#skF_5', '#skF_8'(X_203))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_695, plain, (![X_203]: (~entity('#skF_5', '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.27 tff(c_687, plain, (![U_65, V_66]: (~food(U_65, V_66) | ~human_person(U_65, V_66)))).
% 5.40/2.27 tff(c_677, plain, (![U_227, V_228]: (~animate(U_227, V_228) | ~burger(U_227, V_228)))).
% 5.40/2.27 tff(c_100, plain, (![V_82, Y_125, X_121, W_113, U_81]: ('#skF_1'(V_82, X_121, U_81, Y_125, W_113)!=Y_125 | three(U_81, V_82) | Y_125=W_113 | Y_125=X_121 | ~member(U_81, Y_125, V_82) | X_121=W_113 | ~member(U_81, X_121, V_82) | ~member(U_81, W_113, V_82)))).
% 5.40/2.27 tff(c_704, plain, (~artifact('#skF_5', '#skF_7'))).
% 5.40/2.27 tff(c_703, plain, (~burger('#skF_5', '#skF_7'))).
% 5.40/2.27 tff(c_696, plain, (~entity('#skF_5', '#skF_7'))).
% 5.40/2.27 tff(c_465, plain, (![U_265, V_266]: (~entity(U_265, V_266) | ~group(U_265, V_266)))).
% 5.40/2.27 tff(c_388, plain, (![U_354, V_355]: (~living(U_354, V_355) | ~food(U_354, V_355)))).
% 5.40/2.27 tff(c_550, plain, (![X_203]: (hamburger('#skF_5', '#skF_2'('#skF_5', '#skF_8'(X_203))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.27 tff(c_387, plain, (![U_354, V_355]: (~animate(U_354, V_355) | ~food(U_354, V_355)))).
% 5.40/2.27 tff(c_470, plain, (![U_65, V_66]: (~artifact(U_65, V_66) | ~human_person(U_65, V_66)))).
% 5.40/2.27 tff(c_666, plain, (~artifact('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_98, plain, (![V_82, Y_125, X_121, W_113, U_81]: ('#skF_1'(V_82, X_121, U_81, Y_125, W_113)!=X_121 | three(U_81, V_82) | Y_125=W_113 | Y_125=X_121 | ~member(U_81, Y_125, V_82) | X_121=W_113 | ~member(U_81, X_121, V_82) | ~member(U_81, W_113, V_82)))).
% 5.40/2.27 tff(c_665, plain, (~artifact('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_664, plain, (~artifact('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_399, plain, (![U_69, V_70]: (~artifact(U_69, V_70) | ~guy(U_69, V_70)))).
% 5.40/2.27 tff(c_460, plain, (![U_227, V_228]: (entity(U_227, V_228) | ~burger(U_227, V_228)))).
% 5.40/2.27 tff(c_647, plain, (~burger('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_615, plain, (![X_203]: (~eventuality('#skF_5', '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.27 tff(c_638, plain, (~burger('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_642, plain, (~burger('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_633, plain, (~food('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_96, plain, (![V_82, Y_125, X_121, W_113, U_81]: ('#skF_1'(V_82, X_121, U_81, Y_125, W_113)!=W_113 | three(U_81, V_82) | Y_125=W_113 | Y_125=X_121 | ~member(U_81, Y_125, V_82) | X_121=W_113 | ~member(U_81, X_121, V_82) | ~member(U_81, W_113, V_82)))).
% 5.40/2.27 tff(c_634, plain, (~food('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_632, plain, (~food('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_410, plain, (![U_69, V_70]: (~food(U_69, V_70) | ~guy(U_69, V_70)))).
% 5.40/2.27 tff(c_507, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~event(U_17, V_18)))).
% 5.40/2.27 tff(c_620, plain, (~event('#skF_5', '#skF_7'))).
% 5.40/2.27 tff(c_616, plain, (~eventuality('#skF_5', '#skF_7'))).
% 5.40/2.27 tff(c_578, plain, (![U_265, V_266]: (~eventuality(U_265, V_266) | ~group(U_265, V_266)))).
% 5.40/2.27 tff(c_590, plain, (animate('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.27 tff(c_591, plain, (animate('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_82, plain, (![Z_138, U_81, V_82]: (Z_138='#skF_2'(U_81, V_82) | Z_138='#skF_3'(U_81, V_82) | Z_138='#skF_4'(U_81, V_82) | ~member(U_81, Z_138, V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_589, plain, (animate('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_270, plain, (![U_316, V_317]: (animate(U_316, V_317) | ~guy(U_316, V_317)))).
% 5.40/2.28 tff(c_281, plain, (![U_320, V_321]: (~multiple(U_320, V_321) | ~eventuality(U_320, V_321)))).
% 5.40/2.28 tff(c_568, plain, (~event('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_564, plain, (entity('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_328, plain, (![X_203]: (hamburger('#skF_5', '#skF_3'('#skF_5', '#skF_8'(X_203))) | ~member('#skF_5', X_203, '#skF_7') | ~three('#skF_5', '#skF_8'(X_203))))).
% 5.40/2.28 tff(c_563, plain, (~eventuality('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_556, plain, (young('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_553, plain, (guy('#skF_5', '#skF_2'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_94, plain, (![U_81, V_82]: (member(U_81, '#skF_2'(U_81, V_82), V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_512, plain, (~animate('#skF_5', '#skF_6'))).
% 5.40/2.28 tff(c_296, plain, (![U_328, V_329]: (~animate(U_328, V_329) | ~artifact(U_328, V_329)))).
% 5.40/2.28 tff(c_288, plain, (![U_55, V_56]: (~eventuality(U_55, V_56) | ~entity(U_55, V_56)))).
% 5.40/2.28 tff(c_485, plain, ('#skF_3'('#skF_5', '#skF_7')!='#skF_4'('#skF_5', '#skF_7'))).
% 5.40/2.28 tff(c_493, plain, (~event('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_130, plain, (![X_203, Z_217]: (agent('#skF_5', '#skF_9'(X_203, Z_217), X_203) | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_489, plain, (~event('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_480, plain, (~eventuality('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_479, plain, (~eventuality('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_86, plain, (![U_81, V_82]: ('#skF_3'(U_81, V_82)!='#skF_4'(U_81, V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_304, plain, (![U_334, V_335]: (~eventuality(U_334, V_335) | ~guy(U_334, V_335)))).
% 5.40/2.28 tff(c_271, plain, (![U_316, V_317]: (human(U_316, V_317) | ~guy(U_316, V_317)))).
% 5.40/2.28 tff(c_297, plain, (![U_328, V_329]: (~living(U_328, V_329) | ~artifact(U_328, V_329)))).
% 5.40/2.28 tff(c_351, plain, (![U_344, V_345]: (~multiple(U_344, V_345) | ~entity(U_344, V_345)))).
% 5.40/2.28 tff(c_362, plain, (![U_346, V_347]: (entity(U_346, V_347) | ~food(U_346, V_347)))).
% 5.40/2.28 tff(c_122, plain, (![X_203, Z_217]: (with('#skF_5', '#skF_9'(X_203, Z_217), Z_217) | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_454, plain, (entity('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_450, plain, (young('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_447, plain, (guy('#skF_5', '#skF_4'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_88, plain, (![U_81, V_82]: (member(U_81, '#skF_4'(U_81, V_82), V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_378, plain, (![U_246, V_247]: (~male(U_246, V_247) | ~food(U_246, V_247)))).
% 5.40/2.28 tff(c_405, plain, (entity('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_269, plain, (![U_316, V_317]: (entity(U_316, V_317) | ~guy(U_316, V_317)))).
% 5.40/2.28 tff(c_363, plain, (![U_346, V_347]: (impartial(U_346, V_347) | ~food(U_346, V_347)))).
% 5.40/2.28 tff(c_379, plain, (![U_1, V_2]: (~male(U_1, V_2) | ~artifact(U_1, V_2)))).
% 5.40/2.28 tff(c_124, plain, (![X_203, Z_217]: (at('#skF_5', '#skF_9'(X_203, Z_217), '#skF_6') | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_364, plain, (![U_346, V_347]: (nonliving(U_346, V_347) | ~food(U_346, V_347)))).
% 5.40/2.28 tff(c_370, plain, ('#skF_2'('#skF_5', '#skF_7')!='#skF_4'('#skF_5', '#skF_7'))).
% 5.40/2.28 tff(c_206, plain, (![U_21, V_22]: (~male(U_21, V_22) | ~object(U_21, V_22)))).
% 5.40/2.28 tff(c_84, plain, (![U_81, V_82]: ('#skF_2'(U_81, V_82)!='#skF_4'(U_81, V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_140, plain, (![U_227, V_228]: (food(U_227, V_228) | ~burger(U_227, V_228)))).
% 5.40/2.28 tff(c_162, plain, (![U_246, V_247]: (object(U_246, V_247) | ~food(U_246, V_247)))).
% 5.40/2.28 tff(c_193, plain, (![U_274, V_275]: (singleton(U_274, V_275) | ~entity(U_274, V_275)))).
% 5.40/2.28 tff(c_212, plain, (![U_1, V_2]: (impartial(U_1, V_2) | ~artifact(U_1, V_2)))).
% 5.40/2.28 tff(c_339, plain, (artifact('#skF_5', '#skF_6'))).
% 5.40/2.28 tff(c_132, plain, (![X_203, Z_217]: (event('#skF_5', '#skF_9'(X_203, Z_217)) | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_220, plain, (![U_288, V_289]: (artifact(U_288, V_289) | ~furniture(U_288, V_289)))).
% 5.40/2.28 tff(c_334, plain, (young('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_331, plain, (guy('#skF_5', '#skF_3'('#skF_5', '#skF_7')))).
% 5.40/2.28 tff(c_92, plain, (![U_81, V_82]: (member(U_81, '#skF_3'(U_81, V_82), V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_167, plain, (![U_69, V_70]: (male(U_69, V_70) | ~guy(U_69, V_70)))).
% 5.40/2.28 tff(c_184, plain, (![U_265, V_266]: (multiple(U_265, V_266) | ~group(U_265, V_266)))).
% 5.40/2.28 tff(c_198, plain, (![U_65, V_66]: (living(U_65, V_66) | ~human_person(U_65, V_66)))).
% 5.40/2.28 tff(c_149, plain, (![U_236, V_237]: (nonliving(U_236, V_237) | ~artifact(U_236, V_237)))).
% 5.40/2.28 tff(c_225, plain, (![U_290, V_291]: (~existent(U_290, V_291) | ~eventuality(U_290, V_291)))).
% 5.40/2.28 tff(c_128, plain, (![X_203, Z_217]: (present('#skF_5', '#skF_9'(X_203, Z_217)) | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_276, plain, ('#skF_3'('#skF_5', '#skF_7')!='#skF_2'('#skF_5', '#skF_7'))).
% 5.40/2.28 tff(c_207, plain, (![U_9, V_10]: (~male(U_9, V_10) | ~eventuality(U_9, V_10)))).
% 5.40/2.28 tff(c_255, plain, (![U_308, V_309]: (singleton(U_308, V_309) | ~eventuality(U_308, V_309)))).
% 5.40/2.28 tff(c_90, plain, (![U_81, V_82]: ('#skF_3'(U_81, V_82)!='#skF_2'(U_81, V_82) | ~three(U_81, V_82)))).
% 5.40/2.28 tff(c_248, plain, (![U_69, V_70]: (human_person(U_69, V_70) | ~guy(U_69, V_70)))).
% 5.40/2.28 tff(c_156, plain, (![U_242, V_243]: (entity(U_242, V_243) | ~human_person(U_242, V_243)))).
% 5.40/2.28 tff(c_238, plain, (![U_65, V_66]: (impartial(U_65, V_66) | ~human_person(U_65, V_66)))).
% 5.40/2.28 tff(c_243, plain, (![U_1, V_2]: (entity(U_1, V_2) | ~artifact(U_1, V_2)))).
% 5.40/2.28 tff(c_16, plain, (![U_15, V_16]: (thing(U_15, V_16) | ~eventuality(U_15, V_16)))).
% 5.40/2.28 tff(c_126, plain, (![X_203, Z_217]: (sit('#skF_5', '#skF_9'(X_203, Z_217)) | ~member('#skF_5', Z_217, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_38, plain, (![U_37, V_38]: (burger(U_37, V_38) | ~hamburger(U_37, V_38)))).
% 5.40/2.28 tff(c_68, plain, (![U_67, V_68]: (human_person(U_67, V_68) | ~man(U_67, V_68)))).
% 5.40/2.28 tff(c_28, plain, (![U_27, V_28]: (entity(U_27, V_28) | ~object(U_27, V_28)))).
% 5.40/2.28 tff(c_54, plain, (![U_53, V_54]: (impartial(U_53, V_54) | ~organism(U_53, V_54)))).
% 5.40/2.28 tff(c_40, plain, (![U_39, V_40]: (group(U_39, V_40) | ~three(U_39, V_40)))).
% 5.40/2.28 tff(c_56, plain, (![U_55, V_56]: (existent(U_55, V_56) | ~entity(U_55, V_56)))).
% 5.40/2.28 tff(c_72, plain, (![U_71, V_72]: (~nonliving(U_71, V_72) | ~animate(U_71, V_72)))).
% 5.40/2.28 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))).
% 5.40/2.28 tff(c_6, plain, (![U_5, V_6]: (instrumentality(U_5, V_6) | ~furniture(U_5, V_6)))).
% 5.40/2.28 tff(c_118, plain, (![X2_219, X_203]: (hamburger('#skF_5', X2_219) | ~member('#skF_5', X2_219, '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.28 tff(c_48, plain, (![U_47, V_48]: (animate(U_47, V_48) | ~human_person(U_47, V_48)))).
% 5.40/2.28 tff(c_74, plain, (![U_73, V_74]: (~nonexistent(U_73, V_74) | ~existent(U_73, V_74)))).
% 5.40/2.29 tff(c_24, plain, (![U_23, V_24]: (impartial(U_23, V_24) | ~object(U_23, V_24)))).
% 5.40/2.29 tff(c_80, plain, (![U_79, V_80]: (~male(U_79, V_80) | ~unisex(U_79, V_80)))).
% 5.40/2.29 tff(c_52, plain, (![U_51, V_52]: (living(U_51, V_52) | ~organism(U_51, V_52)))).
% 5.40/2.29 tff(c_62, plain, (![U_61, V_62]: (thing(U_61, V_62) | ~entity(U_61, V_62)))).
% 5.40/2.29 tff(c_60, plain, (![U_59, V_60]: (singleton(U_59, V_60) | ~thing(U_59, V_60)))).
% 5.40/2.29 tff(c_50, plain, (![U_49, V_50]: (human(U_49, V_50) | ~human_person(U_49, V_50)))).
% 5.40/2.29 tff(c_20, plain, (![U_19, V_20]: (event(U_19, V_20) | ~sit(U_19, V_20)))).
% 5.40/2.29 tff(c_120, plain, (![X_203]: (group('#skF_5', '#skF_8'(X_203)) | ~member('#skF_5', X_203, '#skF_7')))).
% 5.40/2.29 tff(c_44, plain, (![U_43, V_44]: (set(U_43, V_44) | ~group(U_43, V_44)))).
% 5.40/2.29 tff(c_78, plain, (![U_77, V_78]: (~multiple(U_77, V_78) | ~singleton(U_77, V_78)))).
% 5.40/2.29 tff(c_177, plain, (furniture('#skF_5', '#skF_6'))).
% 5.40/2.29 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))).
% 5.40/2.29 tff(c_8, plain, (![U_7, V_8]: (furniture(U_7, V_8) | ~table(U_7, V_8)))).
% 5.40/2.29 tff(c_22, plain, (![U_21, V_22]: (unisex(U_21, V_22) | ~object(U_21, V_22)))).
% 5.40/2.29 tff(c_4, plain, (![U_3, V_4]: (artifact(U_3, V_4) | ~instrumentality(U_3, V_4)))).
% 5.40/2.29 tff(c_14, plain, (![U_13, V_14]: (specific(U_13, V_14) | ~eventuality(U_13, V_14)))).
% 5.40/2.29 tff(c_18, plain, (![U_17, V_18]: (eventuality(U_17, V_18) | ~event(U_17, V_18)))).
% 5.40/2.29 tff(c_116, plain, (![X3_220]: (guy('#skF_5', X3_220) | ~member('#skF_5', X3_220, '#skF_7')))).
% 5.40/2.29 tff(c_46, plain, (![U_45, V_46]: (male(U_45, V_46) | ~man(U_45, V_46)))).
% 5.40/2.29 tff(c_32, plain, (![U_31, V_32]: (substance_matter(U_31, V_32) | ~food(U_31, V_32)))).
% 5.40/2.29 tff(c_76, plain, (![U_75, V_76]: (~living(U_75, V_76) | ~nonliving(U_75, V_76)))).
% 5.40/2.29 tff(c_66, plain, (![U_65, V_66]: (organism(U_65, V_66) | ~human_person(U_65, V_66)))).
% 5.40/2.29 tff(c_64, plain, (![U_63, V_64]: (entity(U_63, V_64) | ~organism(U_63, V_64)))).
% 5.40/2.29 tff(c_42, plain, (![U_41, V_42]: (multiple(U_41, V_42) | ~set(U_41, V_42)))).
% 5.40/2.29 tff(c_2, plain, (![U_1, V_2]: (object(U_1, V_2) | ~artifact(U_1, V_2)))).
% 5.40/2.29 tff(c_26, plain, (![U_25, V_26]: (nonliving(U_25, V_26) | ~object(U_25, V_26)))).
% 5.40/2.29 tff(c_30, plain, (![U_29, V_30]: (object(U_29, V_30) | ~substance_matter(U_29, V_30)))).
% 5.40/2.29 tff(c_114, plain, (![X3_220]: (young('#skF_5', X3_220) | ~member('#skF_5', X3_220, '#skF_7')))).
% 5.40/2.29 tff(c_70, plain, (![U_69, V_70]: (man(U_69, V_70) | ~guy(U_69, V_70)))).
% 5.40/2.29 tff(c_36, plain, (![U_35, V_36]: (meat(U_35, V_36) | ~burger(U_35, V_36)))).
% 5.40/2.29 tff(c_34, plain, (![U_33, V_34]: (food(U_33, V_34) | ~meat(U_33, V_34)))).
% 5.40/2.29 tff(c_10, plain, (![U_9, V_10]: (unisex(U_9, V_10) | ~eventuality(U_9, V_10)))).
% 5.40/2.29 tff(c_104, plain, (![U_139, V_140]: (~member(U_139, V_140, V_140)))).
% 5.40/2.29 tff(c_106, plain, (group('#skF_5', '#skF_7'))).
% 5.40/2.29 tff(c_108, plain, (three('#skF_5', '#skF_7'))).
% 5.40/2.29 tff(c_110, plain, (table('#skF_5', '#skF_6'))).
% 5.40/2.29 tff(c_112, plain, (actual_world('#skF_5'))).
% 5.40/2.29 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.40/2.29
%------------------------------------------------------------------------------