%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:22:05 AM UTC 2026
% Result : Unsatisfiable 39.37s 5.89s
% Output : CNFRefutation 39.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 46
% Syntax : Number of clauses : 227 ( 69 unt; 130 nHn; 225 RR)
% Number of literals : 998 ( 0 equ; 165 neg)
% Maximal clause size : 17 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 106 ( 46 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(symmetry_of_equal_jobs,axiom,
( 'equal$ujobs'(X1,X0)
| ~ 'equal$ujobs'(X0,X1) ) ).
cnf(chef_not_guard,axiom,
~ 'equal$ujobs'(chef,guard) ).
cnf(chef_not_nurse,axiom,
~ 'equal$ujobs'(chef,nurse) ).
cnf(chef_not_actor,axiom,
~ 'equal$ujobs'(chef,actor) ).
cnf(chef_not_boxer,axiom,
~ 'equal$ujobs'(chef,boxer) ).
cnf(chef_not_teacher,axiom,
~ 'equal$ujobs'(chef,teacher) ).
cnf(guard_not_nurse,axiom,
~ 'equal$ujobs'(guard,nurse) ).
cnf(guard_not_operator,axiom,
~ 'equal$ujobs'(guard,operator) ).
cnf(guard_not_police,axiom,
~ 'equal$ujobs'(guard,police) ).
cnf(guard_not_actor,axiom,
~ 'equal$ujobs'(guard,actor) ).
cnf(guard_not_boxer,axiom,
~ 'equal$ujobs'(guard,boxer) ).
cnf(nurse_not_operator,axiom,
~ 'equal$ujobs'(nurse,operator) ).
cnf(nurse_not_police,axiom,
~ 'equal$ujobs'(nurse,police) ).
cnf(nurse_not_actor,axiom,
~ 'equal$ujobs'(nurse,actor) ).
cnf(nurse_not_boxer,axiom,
~ 'equal$ujobs'(nurse,boxer) ).
cnf(nurse_not_teacher,axiom,
~ 'equal$ujobs'(nurse,teacher) ).
cnf(operator_not_police,axiom,
~ 'equal$ujobs'(operator,police) ).
cnf(operator_not_actor,axiom,
~ 'equal$ujobs'(operator,actor) ).
cnf(operator_not_boxer,axiom,
~ 'equal$ujobs'(operator,boxer) ).
cnf(police_not_actor,axiom,
~ 'equal$ujobs'(police,actor) ).
cnf(police_not_boxer,axiom,
~ 'equal$ujobs'(police,boxer) ).
cnf(police_not_teacher,axiom,
~ 'equal$ujobs'(police,teacher) ).
cnf(actor_not_boxer,axiom,
~ 'equal$ujobs'(actor,boxer) ).
cnf(boxer_not_teacher,axiom,
~ 'equal$ujobs'(boxer,teacher) ).
cnf(nurse_is_male,axiom,
( male(X0)
| ~ 'has$ujob'(X0,nurse) ) ).
cnf(actor_is_male,axiom,
( male(X0)
| ~ 'has$ujob'(X0,actor) ) ).
cnf(chef_is_female,axiom,
( female(X0)
| ~ 'has$ujob'(X0,chef) ) ).
cnf(nurse_is_educated,axiom,
( educated(X0)
| ~ 'has$ujob'(X0,nurse) ) ).
cnf(teacher_is_educated,axiom,
( educated(X0)
| ~ 'has$ujob'(X0,teacher) ) ).
cnf(police_is_educated,axiom,
( educated(X0)
| ~ 'has$ujob'(X0,police) ) ).
cnf(chef_is_not_also_police,axiom,
( ~ 'has$ujob'(X0,police)
| ~ 'has$ujob'(X0,chef) ) ).
cnf(males_are_not_female,axiom,
( ~ female(X0)
| ~ male(X0) ) ).
cnf(husband_is_male,axiom,
( male(X1)
| ~ husband(X0,X1) ) ).
cnf(husband_of_chef_is_operator1,hypothesis,
( husband(X0,X1)
| ~ 'has$ujob'(X1,operator)
| ~ 'has$ujob'(X0,chef) ) ).
cnf(husband_of_chef_is_operator2,hypothesis,
( ~ husband(X0,X1)
| 'has$ujob'(X1,operator)
| ~ 'has$ujob'(X0,chef) ) ).
cnf(each_has_maximum_of_two_jobs,hypothesis,
( 'equal$ujobs'(X2,X3)
| 'equal$ujobs'(X1,X3)
| 'equal$ujobs'(X1,X2)
| ~ 'has$ujob'(X0,X3)
| ~ 'has$ujob'(X0,X2)
| ~ 'has$ujob'(X0,X1) ) ).
cnf(every_job_is_used,hypothesis,
( 'has$ujob'(steve,X0)
| 'has$ujob'(pete,X0)
| 'has$ujob'(thelma,X0)
| 'has$ujob'(roberta,X0) ) ).
cnf(pete_is_not_educated,hypothesis,
~ educated(pete) ).
cnf(roberta_is_not_chef,hypothesis,
~ 'has$ujob'(roberta,chef) ).
cnf(roberta_is_not_boxer,hypothesis,
~ 'has$ujob'(roberta,boxer) ).
cnf(roberta_is_not_police,hypothesis,
~ 'has$ujob'(roberta,police) ).
cnf(steve_is_male,hypothesis,
male(steve) ).
cnf(pete_is_male,hypothesis,
male(pete) ).
cnf(roberta_is_female,hypothesis,
female(roberta) ).
cnf(thelma_is_female,hypothesis,
female(thelma) ).
cnf(find_who_has_each_job,negated_conjecture,
( ~ 'has$ujob'(X7,boxer)
| ~ 'has$ujob'(X6,actor)
| ~ 'has$ujob'(X5,teacher)
| ~ 'has$ujob'(X4,police)
| ~ 'has$ujob'(X3,operator)
| ~ 'has$ujob'(X2,nurse)
| ~ 'has$ujob'(X1,guard)
| ~ 'has$ujob'(X0,chef) ) ).
cnf(c3,plain,
( 'equal$ujobs'(X1,X0)
| ~ 'equal$ujobs'(X0,X1) ),
inference(clausification,[status(esa)],[symmetry_of_equal_jobs]) ).
cnf(c10,plain,
~ 'equal$ujobs'(chef,guard),
inference(clausification,[status(esa)],[chef_not_guard]) ).
cnf(c11,plain,
~ 'equal$ujobs'(chef,nurse),
inference(clausification,[status(esa)],[chef_not_nurse]) ).
cnf(c14,plain,
~ 'equal$ujobs'(chef,actor),
inference(clausification,[status(esa)],[chef_not_actor]) ).
cnf(c15,plain,
~ 'equal$ujobs'(chef,boxer),
inference(clausification,[status(esa)],[chef_not_boxer]) ).
cnf(c16,plain,
~ 'equal$ujobs'(chef,teacher),
inference(clausification,[status(esa)],[chef_not_teacher]) ).
cnf(c17,plain,
~ 'equal$ujobs'(guard,nurse),
inference(clausification,[status(esa)],[guard_not_nurse]) ).
cnf(c18,plain,
~ 'equal$ujobs'(guard,operator),
inference(clausification,[status(esa)],[guard_not_operator]) ).
cnf(c19,plain,
~ 'equal$ujobs'(guard,police),
inference(clausification,[status(esa)],[guard_not_police]) ).
cnf(c20,plain,
~ 'equal$ujobs'(guard,actor),
inference(clausification,[status(esa)],[guard_not_actor]) ).
cnf(c21,plain,
~ 'equal$ujobs'(guard,boxer),
inference(clausification,[status(esa)],[guard_not_boxer]) ).
cnf(c23,plain,
~ 'equal$ujobs'(nurse,operator),
inference(clausification,[status(esa)],[nurse_not_operator]) ).
cnf(c24,plain,
~ 'equal$ujobs'(nurse,police),
inference(clausification,[status(esa)],[nurse_not_police]) ).
cnf(c25,plain,
~ 'equal$ujobs'(nurse,actor),
inference(clausification,[status(esa)],[nurse_not_actor]) ).
cnf(c26,plain,
~ 'equal$ujobs'(nurse,boxer),
inference(clausification,[status(esa)],[nurse_not_boxer]) ).
cnf(c27,plain,
~ 'equal$ujobs'(nurse,teacher),
inference(clausification,[status(esa)],[nurse_not_teacher]) ).
cnf(c28,plain,
~ 'equal$ujobs'(operator,police),
inference(clausification,[status(esa)],[operator_not_police]) ).
cnf(c29,plain,
~ 'equal$ujobs'(operator,actor),
inference(clausification,[status(esa)],[operator_not_actor]) ).
cnf(c30,plain,
~ 'equal$ujobs'(operator,boxer),
inference(clausification,[status(esa)],[operator_not_boxer]) ).
cnf(c32,plain,
~ 'equal$ujobs'(police,actor),
inference(clausification,[status(esa)],[police_not_actor]) ).
cnf(c33,plain,
~ 'equal$ujobs'(police,boxer),
inference(clausification,[status(esa)],[police_not_boxer]) ).
cnf(c34,plain,
~ 'equal$ujobs'(police,teacher),
inference(clausification,[status(esa)],[police_not_teacher]) ).
cnf(c35,plain,
~ 'equal$ujobs'(actor,boxer),
inference(clausification,[status(esa)],[actor_not_boxer]) ).
cnf(c37,plain,
~ 'equal$ujobs'(boxer,teacher),
inference(clausification,[status(esa)],[boxer_not_teacher]) ).
cnf(c38,plain,
( male(X0)
| ~ 'has$ujob'(X0,nurse) ),
inference(clausification,[status(esa)],[nurse_is_male]) ).
cnf(c39,plain,
( male(X0)
| ~ 'has$ujob'(X0,actor) ),
inference(clausification,[status(esa)],[actor_is_male]) ).
cnf(c40,plain,
( female(X0)
| ~ 'has$ujob'(X0,chef) ),
inference(clausification,[status(esa)],[chef_is_female]) ).
cnf(c41,plain,
( educated(X0)
| ~ 'has$ujob'(X0,nurse) ),
inference(clausification,[status(esa)],[nurse_is_educated]) ).
cnf(c42,plain,
( educated(X0)
| ~ 'has$ujob'(X0,teacher) ),
inference(clausification,[status(esa)],[teacher_is_educated]) ).
cnf(c43,plain,
( educated(X0)
| ~ 'has$ujob'(X0,police) ),
inference(clausification,[status(esa)],[police_is_educated]) ).
cnf(c44,plain,
( ~ 'has$ujob'(X0,police)
| ~ 'has$ujob'(X0,chef) ),
inference(clausification,[status(esa)],[chef_is_not_also_police]) ).
cnf(c45,plain,
( ~ female(X0)
| ~ male(X0) ),
inference(clausification,[status(esa)],[males_are_not_female]) ).
cnf(c47,plain,
( male(X1)
| ~ husband(X0,X1) ),
inference(clausification,[status(esa)],[husband_is_male]) ).
cnf(c49,plain,
( husband(X1,X0)
| ~ 'has$ujob'(X1,chef)
| ~ 'has$ujob'(X0,operator) ),
inference(clausification,[status(esa)],[husband_of_chef_is_operator1]) ).
cnf(c50,plain,
( ~ husband(X1,X0)
| ~ 'has$ujob'(X1,chef)
| 'has$ujob'(X0,operator) ),
inference(clausification,[status(esa)],[husband_of_chef_is_operator2]) ).
cnf(c52,plain,
( ~ 'has$ujob'(X3,X1)
| ~ 'has$ujob'(X3,X2)
| ~ 'has$ujob'(X3,X0)
| 'equal$ujobs'(X2,X1)
| 'equal$ujobs'(X0,X2)
| 'equal$ujobs'(X0,X1) ),
inference(clausification,[status(esa)],[each_has_maximum_of_two_jobs]) ).
cnf(c53,plain,
( 'has$ujob'(steve,X0)
| 'has$ujob'(thelma,X0)
| 'has$ujob'(roberta,X0)
| 'has$ujob'(pete,X0) ),
inference(clausification,[status(esa)],[every_job_is_used]) ).
cnf(c55,plain,
~ educated(pete),
inference(clausification,[status(esa)],[pete_is_not_educated]) ).
cnf(c56,plain,
~ 'has$ujob'(roberta,chef),
inference(clausification,[status(esa)],[roberta_is_not_chef]) ).
cnf(c57,plain,
~ 'has$ujob'(roberta,boxer),
inference(clausification,[status(esa)],[roberta_is_not_boxer]) ).
cnf(c58,plain,
~ 'has$ujob'(roberta,police),
inference(clausification,[status(esa)],[roberta_is_not_police]) ).
cnf(c59,plain,
male(steve),
inference(clausification,[status(esa)],[steve_is_male]) ).
cnf(c60,plain,
male(pete),
inference(clausification,[status(esa)],[pete_is_male]) ).
cnf(c61,plain,
female(roberta),
inference(clausification,[status(esa)],[roberta_is_female]) ).
cnf(c62,plain,
female(thelma),
inference(clausification,[status(esa)],[thelma_is_female]) ).
cnf(c63,plain,
( ~ 'has$ujob'(X7,actor)
| ~ 'has$ujob'(X6,guard)
| ~ 'has$ujob'(X5,chef)
| ~ 'has$ujob'(X4,nurse)
| ~ 'has$ujob'(X3,teacher)
| ~ 'has$ujob'(X2,police)
| ~ 'has$ujob'(X1,boxer)
| ~ 'has$ujob'(X0,operator) ),
inference(clausification,[status(esa)],[find_who_has_each_job]) ).
cnf(d0,plain,
( 'has$ujob'(steve,police)
| 'has$ujob'(pete,police)
| 'has$ujob'(thelma,police) ),
inference(resolution,[status(thm)],[c53,c58]) ).
cnf(d1,plain,
( 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| 'has$ujob'(thelma,chef) ),
inference(resolution,[status(thm)],[c53,c56]) ).
cnf(d2,plain,
( ~ 'has$ujob'(thelma,police)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d1,c44]) ).
cnf(d3,plain,
( 'has$ujob'(steve,police)
| 'has$ujob'(pete,police)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d2,d0]) ).
cnf(d4,plain,
( female(pete)
| 'has$ujob'(steve,police)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,police) ),
inference(resolution,[status(thm)],[d3,c40]) ).
cnf(d5,plain,
~ female(pete),
inference(resolution,[status(thm)],[c45,c60]) ).
cnf(d6,plain,
( 'has$ujob'(steve,police)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,police) ),
inference(resolution,[status(thm)],[d5,d4]) ).
cnf(d7,plain,
( educated(pete)
| 'has$ujob'(steve,police)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d6,c43]) ).
cnf(d8,plain,
( 'has$ujob'(steve,police)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[c55,d7]) ).
cnf(d9,plain,
( female(steve)
| 'has$ujob'(steve,police) ),
inference(resolution,[status(thm)],[d8,c40]) ).
cnf(d10,plain,
~ female(steve),
inference(resolution,[status(thm)],[c45,c59]) ).
cnf(d11,plain,
'has$ujob'(steve,police),
inference(resolution,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
( male(roberta)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(thelma,nurse) ),
inference(resolution,[status(thm)],[c53,c38]) ).
cnf(d13,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(pete,nurse) ),
inference(resolution,[status(thm)],[d12,c38]) ).
cnf(d14,plain,
( educated(pete)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,nurse) ),
inference(resolution,[status(thm)],[d13,c41]) ).
cnf(d15,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,nurse) ),
inference(resolution,[status(thm)],[c55,d14]) ).
cnf(d16,plain,
( ~ 'has$ujob'(steve,X1)
| ~ 'has$ujob'(steve,X0)
| 'equal$ujobs'(X0,X1)
| 'equal$ujobs'(nurse,X1)
| 'equal$ujobs'(nurse,X0)
| male(thelma)
| male(roberta) ),
inference(resolution,[status(thm)],[d15,c52]) ).
cnf(d17,plain,
( male(thelma)
| male(roberta)
| ~ 'has$ujob'(steve,X0)
| 'equal$ujobs'(nurse,X0)
| 'equal$ujobs'(nurse,police)
| 'equal$ujobs'(X0,police) ),
inference(resolution,[status(thm)],[d16,d11]) ).
cnf(d18,plain,
( male(thelma)
| male(roberta)
| ~ 'has$ujob'(steve,X0)
| 'equal$ujobs'(nurse,X0)
| 'equal$ujobs'(X0,police) ),
inference(resolution,[status(thm)],[c24,d17]) ).
cnf(d19,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(pete,actor)
| 'has$ujob'(thelma,actor) ),
inference(resolution,[status(thm)],[c53,c39]) ).
cnf(d20,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(pete,actor) ),
inference(resolution,[status(thm)],[d19,c39]) ).
cnf(d21,plain,
( ~ husband(thelma,X0)
| 'has$ujob'(X0,operator)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d1,c50]) ).
cnf(d22,plain,
( husband(thelma,X0)
| ~ 'has$ujob'(X0,operator)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d1,c49]) ).
cnf(d23,plain,
( 'has$ujob'(steve,operator)
| 'has$ujob'(pete,operator)
| 'has$ujob'(thelma,operator)
| husband(thelma,roberta)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d22,c53]) ).
cnf(d24,plain,
( husband(thelma,thelma)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,operator)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d23,d22]) ).
cnf(d25,plain,
( female(pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,operator) ),
inference(resolution,[status(thm)],[d24,c40]) ).
cnf(d26,plain,
( husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,operator) ),
inference(resolution,[status(thm)],[d5,d25]) ).
cnf(d27,plain,
( husband(thelma,pete)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d26,d22]) ).
cnf(d28,plain,
( female(pete)
| husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d27,c40]) ).
cnf(d29,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d5,d28]) ).
cnf(d30,plain,
( female(steve)
| husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator) ),
inference(resolution,[status(thm)],[d29,c40]) ).
cnf(d31,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| 'has$ujob'(steve,operator) ),
inference(resolution,[status(thm)],[d10,d30]) ).
cnf(d32,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(nurse,operator)
| 'equal$ujobs'(operator,police)
| husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta) ),
inference(resolution,[status(thm)],[d31,d18]) ).
cnf(d33,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| male(thelma)
| male(roberta)
| 'equal$ujobs'(operator,police) ),
inference(resolution,[status(thm)],[c23,d32]) ).
cnf(d34,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| male(thelma)
| male(roberta) ),
inference(resolution,[status(thm)],[c28,d33]) ).
cnf(d35,plain,
( ~ female(roberta)
| husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| male(thelma) ),
inference(resolution,[status(thm)],[d34,c45]) ).
cnf(d36,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta)
| male(thelma) ),
inference(resolution,[status(thm)],[c61,d35]) ).
cnf(d37,plain,
( ~ female(thelma)
| husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta) ),
inference(resolution,[status(thm)],[d36,c45]) ).
cnf(d38,plain,
( husband(thelma,pete)
| husband(thelma,thelma)
| husband(thelma,roberta) ),
inference(resolution,[status(thm)],[c62,d37]) ).
cnf(d39,plain,
( male(roberta)
| husband(thelma,pete)
| husband(thelma,thelma) ),
inference(resolution,[status(thm)],[d38,c47]) ).
cnf(d40,plain,
( ~ female(roberta)
| husband(thelma,pete)
| husband(thelma,thelma) ),
inference(resolution,[status(thm)],[d39,c45]) ).
cnf(d41,plain,
( husband(thelma,pete)
| husband(thelma,thelma) ),
inference(resolution,[status(thm)],[c61,d40]) ).
cnf(d42,plain,
( male(thelma)
| husband(thelma,pete) ),
inference(resolution,[status(thm)],[d41,c47]) ).
cnf(d43,plain,
( ~ female(thelma)
| husband(thelma,pete) ),
inference(resolution,[status(thm)],[d42,c45]) ).
cnf(d44,plain,
husband(thelma,pete),
inference(resolution,[status(thm)],[c62,d43]) ).
cnf(d45,plain,
( 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| 'has$ujob'(pete,operator) ),
inference(resolution,[status(thm)],[d44,d21]) ).
cnf(d46,plain,
( female(pete)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,operator) ),
inference(resolution,[status(thm)],[d45,c40]) ).
cnf(d47,plain,
( 'has$ujob'(steve,chef)
| 'has$ujob'(pete,operator) ),
inference(resolution,[status(thm)],[d5,d46]) ).
cnf(d48,plain,
( ~ 'has$ujob'(pete,X1)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(X0,X1)
| 'equal$ujobs'(operator,X1)
| 'equal$ujobs'(operator,X0)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d47,c52]) ).
cnf(d49,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(operator,actor)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[d48,d20]) ).
cnf(d50,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[c29,d49]) ).
cnf(d51,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(thelma,boxer) ),
inference(resolution,[status(thm)],[c53,c57]) ).
cnf(d52,plain,
( ~ 'has$ujob'(thelma,X1)
| ~ 'has$ujob'(thelma,X0)
| 'equal$ujobs'(X0,X1)
| 'equal$ujobs'(chef,X1)
| 'equal$ujobs'(chef,X0)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d1,c52]) ).
cnf(d53,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| ~ 'has$ujob'(thelma,X0)
| 'equal$ujobs'(chef,X0)
| 'equal$ujobs'(chef,boxer)
| 'equal$ujobs'(X0,boxer) ),
inference(resolution,[status(thm)],[d52,d51]) ).
cnf(d54,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,chef)
| ~ 'has$ujob'(thelma,X0)
| 'equal$ujobs'(chef,X0)
| 'equal$ujobs'(X0,boxer) ),
inference(resolution,[status(thm)],[c15,d53]) ).
cnf(d55,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(pete,actor)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(chef,actor)
| 'equal$ujobs'(actor,boxer) ),
inference(resolution,[status(thm)],[d54,d19]) ).
cnf(d56,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(actor,boxer) ),
inference(resolution,[status(thm)],[c14,d55]) ).
cnf(d57,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[c35,d56]) ).
cnf(d58,plain,
( female(pete)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,actor) ),
inference(resolution,[status(thm)],[d57,c40]) ).
cnf(d59,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,actor) ),
inference(resolution,[status(thm)],[d5,d58]) ).
cnf(d60,plain,
( 'has$ujob'(steve,chef)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(operator,actor)
| 'equal$ujobs'(X0,actor)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[d59,d48]) ).
cnf(d61,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[c29,d60]) ).
cnf(d62,plain,
( male(roberta)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(chef,nurse)
| 'equal$ujobs'(nurse,boxer) ),
inference(resolution,[status(thm)],[d54,d12]) ).
cnf(d63,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(nurse,boxer) ),
inference(resolution,[status(thm)],[c11,d62]) ).
cnf(d64,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[c26,d63]) ).
cnf(d65,plain,
( female(pete)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,nurse) ),
inference(resolution,[status(thm)],[d64,c40]) ).
cnf(d66,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,nurse) ),
inference(resolution,[status(thm)],[d5,d65]) ).
cnf(d67,plain,
( educated(pete)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[d66,c41]) ).
cnf(d68,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[c55,d67]) ).
cnf(d69,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(pete,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| ~ 'has$ujob'(thelma,X0)
| 'equal$ujobs'(chef,X0)
| 'equal$ujobs'(chef,actor)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[d52,d19]) ).
cnf(d70,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,chef)
| ~ 'has$ujob'(thelma,X0)
| 'equal$ujobs'(chef,X0)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[c14,d69]) ).
cnf(d71,plain,
( male(roberta)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(pete,nurse)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(chef,nurse)
| 'equal$ujobs'(nurse,actor) ),
inference(resolution,[status(thm)],[d70,d12]) ).
cnf(d72,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(nurse,actor) ),
inference(resolution,[status(thm)],[c11,d71]) ).
cnf(d73,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,nurse)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[c25,d72]) ).
cnf(d74,plain,
( female(pete)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,nurse) ),
inference(resolution,[status(thm)],[d73,c40]) ).
cnf(d75,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor)
| 'has$ujob'(pete,nurse) ),
inference(resolution,[status(thm)],[d5,d74]) ).
cnf(d76,plain,
( educated(pete)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor) ),
inference(resolution,[status(thm)],[d75,c41]) ).
cnf(d77,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,actor) ),
inference(resolution,[status(thm)],[c55,d76]) ).
cnf(d78,plain,
( 'has$ujob'(steve,chef)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(operator,actor)
| 'equal$ujobs'(X0,actor)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d77,d48]) ).
cnf(d79,plain,
( male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| ~ 'has$ujob'(pete,X0)
| 'equal$ujobs'(operator,X0)
| 'equal$ujobs'(X0,actor) ),
inference(resolution,[status(thm)],[c29,d78]) ).
cnf(d80,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'equal$ujobs'(operator,boxer)
| 'equal$ujobs'(boxer,actor) ),
inference(resolution,[status(thm)],[d79,d68]) ).
cnf(d81,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef)
| 'equal$ujobs'(boxer,actor) ),
inference(resolution,[status(thm)],[c30,d80]) ).
cnf(d82,plain,
( 'equal$ujobs'(actor,boxer)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d81,c3]) ).
cnf(d83,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[c35,d82]) ).
cnf(d84,plain,
( female(steve)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse) ),
inference(resolution,[status(thm)],[d83,c40]) ).
cnf(d85,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,nurse) ),
inference(resolution,[status(thm)],[d10,d84]) ).
cnf(d86,plain,
( 'has$ujob'(steve,guard)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X6,boxer)
| ~ 'has$ujob'(X5,actor)
| ~ 'has$ujob'(X4,nurse)
| ~ 'has$ujob'(X3,chef)
| ~ 'has$ujob'(X2,teacher)
| ~ 'has$ujob'(X1,operator)
| ~ 'has$ujob'(X0,police) ),
inference(resolution,[status(thm)],[c63,c53]) ).
cnf(d87,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(steve,guard)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X5,police)
| ~ 'has$ujob'(X4,operator)
| ~ 'has$ujob'(X3,teacher)
| ~ 'has$ujob'(X2,chef)
| ~ 'has$ujob'(X1,nurse)
| ~ 'has$ujob'(X0,actor) ),
inference(resolution,[status(thm)],[d86,d51]) ).
cnf(d88,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,guard)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X4,actor)
| ~ 'has$ujob'(X3,nurse)
| ~ 'has$ujob'(X2,chef)
| ~ 'has$ujob'(X1,teacher)
| ~ 'has$ujob'(X0,operator) ),
inference(resolution,[status(thm)],[d87,d11]) ).
cnf(d89,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,guard)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X3,operator)
| ~ 'has$ujob'(X2,teacher)
| ~ 'has$ujob'(X1,chef)
| ~ 'has$ujob'(X0,nurse)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[d59,d88]) ).
cnf(d90,plain,
( 'has$ujob'(steve,chef)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X2,nurse)
| ~ 'has$ujob'(X1,chef)
| ~ 'has$ujob'(X0,teacher) ),
inference(resolution,[status(thm)],[d89,d47]) ).
cnf(d91,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X1,teacher)
| ~ 'has$ujob'(X0,chef) ),
inference(resolution,[status(thm)],[d90,d85]) ).
cnf(d92,plain,
( 'has$ujob'(steve,teacher)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(thelma,teacher)
| male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,guard)
| ~ 'has$ujob'(X0,chef) ),
inference(resolution,[status(thm)],[d91,c53]) ).
cnf(d93,plain,
( 'has$ujob'(steve,chef)
| 'has$ujob'(pete,chef)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(thelma,teacher)
| 'has$ujob'(thelma,guard) ),
inference(resolution,[status(thm)],[d92,d1]) ).
cnf(d94,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(chef,guard)
| 'equal$ujobs'(guard,boxer)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef)
| 'has$ujob'(thelma,teacher) ),
inference(resolution,[status(thm)],[d93,d54]) ).
cnf(d95,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef)
| 'has$ujob'(thelma,teacher)
| 'equal$ujobs'(guard,boxer) ),
inference(resolution,[status(thm)],[c10,d94]) ).
cnf(d96,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef)
| 'has$ujob'(thelma,teacher) ),
inference(resolution,[status(thm)],[c21,d95]) ).
cnf(d97,plain,
( 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(chef,teacher)
| 'equal$ujobs'(teacher,boxer)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d96,d54]) ).
cnf(d98,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef)
| 'equal$ujobs'(teacher,boxer) ),
inference(resolution,[status(thm)],[c16,d97]) ).
cnf(d99,plain,
( 'equal$ujobs'(boxer,teacher)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[d98,c3]) ).
cnf(d100,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard)
| 'has$ujob'(pete,chef) ),
inference(resolution,[status(thm)],[c37,d99]) ).
cnf(d101,plain,
( female(pete)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard) ),
inference(resolution,[status(thm)],[d100,c40]) ).
cnf(d102,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'has$ujob'(pete,guard) ),
inference(resolution,[status(thm)],[d5,d101]) ).
cnf(d103,plain,
( male(roberta)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,boxer)
| 'equal$ujobs'(operator,guard)
| 'equal$ujobs'(guard,actor)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[d102,d61]) ).
cnf(d104,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer)
| 'equal$ujobs'(operator,guard) ),
inference(resolution,[status(thm)],[c20,d103]) ).
cnf(d105,plain,
( 'equal$ujobs'(guard,operator)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[d104,c3]) ).
cnf(d106,plain,
( male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'has$ujob'(pete,boxer) ),
inference(resolution,[status(thm)],[c18,d105]) ).
cnf(d107,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,chef)
| 'equal$ujobs'(operator,boxer)
| 'equal$ujobs'(boxer,actor)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher) ),
inference(resolution,[status(thm)],[d106,d50]) ).
cnf(d108,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher)
| 'equal$ujobs'(boxer,actor) ),
inference(resolution,[status(thm)],[c30,d107]) ).
cnf(d109,plain,
( 'equal$ujobs'(actor,boxer)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher) ),
inference(resolution,[status(thm)],[d108,c3]) ).
cnf(d110,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef)
| 'has$ujob'(pete,teacher) ),
inference(resolution,[status(thm)],[c35,d109]) ).
cnf(d111,plain,
( educated(pete)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[d110,c42]) ).
cnf(d112,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard)
| 'has$ujob'(steve,chef) ),
inference(resolution,[status(thm)],[c55,d111]) ).
cnf(d113,plain,
( female(steve)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard) ),
inference(resolution,[status(thm)],[d112,c40]) ).
cnf(d114,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'has$ujob'(steve,guard) ),
inference(resolution,[status(thm)],[d10,d113]) ).
cnf(d115,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(nurse,guard)
| 'equal$ujobs'(guard,police)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor) ),
inference(resolution,[status(thm)],[d114,d18]) ).
cnf(d116,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor)
| 'equal$ujobs'(nurse,guard) ),
inference(resolution,[status(thm)],[c19,d115]) ).
cnf(d117,plain,
( 'equal$ujobs'(guard,nurse)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor) ),
inference(resolution,[status(thm)],[d116,c3]) ).
cnf(d118,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'has$ujob'(steve,actor) ),
inference(resolution,[status(thm)],[c17,d117]) ).
cnf(d119,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(nurse,actor)
| 'equal$ujobs'(actor,police)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer) ),
inference(resolution,[status(thm)],[d118,d18]) ).
cnf(d120,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer)
| 'equal$ujobs'(actor,police) ),
inference(resolution,[status(thm)],[c25,d119]) ).
cnf(d121,plain,
( 'equal$ujobs'(police,actor)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer) ),
inference(resolution,[status(thm)],[d120,c3]) ).
cnf(d122,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'has$ujob'(steve,boxer) ),
inference(resolution,[status(thm)],[c32,d121]) ).
cnf(d123,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(nurse,boxer)
| 'equal$ujobs'(boxer,police)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher) ),
inference(resolution,[status(thm)],[d122,d18]) ).
cnf(d124,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher)
| 'equal$ujobs'(boxer,police) ),
inference(resolution,[status(thm)],[c26,d123]) ).
cnf(d125,plain,
( 'equal$ujobs'(police,boxer)
| male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher) ),
inference(resolution,[status(thm)],[d124,c3]) ).
cnf(d126,plain,
( male(thelma)
| male(roberta)
| 'has$ujob'(steve,teacher) ),
inference(resolution,[status(thm)],[c33,d125]) ).
cnf(d127,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(nurse,teacher)
| 'equal$ujobs'(teacher,police)
| male(thelma)
| male(roberta) ),
inference(resolution,[status(thm)],[d126,d18]) ).
cnf(d128,plain,
( male(thelma)
| male(roberta)
| 'equal$ujobs'(teacher,police) ),
inference(resolution,[status(thm)],[c27,d127]) ).
cnf(d129,plain,
( 'equal$ujobs'(police,teacher)
| male(thelma)
| male(roberta) ),
inference(resolution,[status(thm)],[d128,c3]) ).
cnf(d130,plain,
( male(thelma)
| male(roberta) ),
inference(resolution,[status(thm)],[c34,d129]) ).
cnf(d131,plain,
( ~ female(roberta)
| male(thelma) ),
inference(resolution,[status(thm)],[d130,c45]) ).
cnf(d132,plain,
male(thelma),
inference(resolution,[status(thm)],[c61,d131]) ).
cnf(d133,plain,
~ female(thelma),
inference(resolution,[status(thm)],[d132,c45]) ).
cnf(d134,plain,
$false,
inference(resolution,[status(thm)],[c62,d133]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n008.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sat Sep 26 05:06:09 UTC 2026
% 0.13/0.57 % CPUTime :
% 0.13/0.57 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.37/5.89 % SZS status Unsatisfiable for theBenchmark.p
% 39.37/5.89 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------