%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:07 AM UTC 2026
% Result : Unsatisfiable 12.06s 1.93s
% Output : CNFRefutation 12.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 37
% Syntax : Number of clauses : 160 ( 6 unt; 111 nHn; 160 RR)
% Number of literals : 570 ( 0 equ; 194 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 11 ( 10 usr; 11 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(c1,hypothesis,
( 'mustard$ulang'
| 'mustard$ubarry'
| ~ 'salt$umill' ) ).
cnf(c3,hypothesis,
( 'mustard$ulang'
| 'salt$ubarry'
| ~ 'salt$umill' ) ).
cnf(c6,hypothesis,
( ~ 'salt$umill'
| ~ 'mustard$ucole'
| ~ 'mustard$ulang' ) ).
cnf(c7,hypothesis,
( ~ 'mustard$umill'
| ~ 'salt$ucole'
| ~ 'mustard$ulang' ) ).
cnf(c8,hypothesis,
( ~ 'salt$umill'
| ~ 'salt$ucole'
| ~ 'mustard$ulang' ) ).
cnf(c11,hypothesis,
( ~ 'mustard$umill'
| ~ 'salt$ulang'
| ~ 'mustard$udix' ) ).
cnf(c12,hypothesis,
( ~ 'salt$umill'
| ~ 'salt$ulang'
| ~ 'mustard$udix' ) ).
cnf(c14,hypothesis,
( 'salt$ucole'
| ~ 'mustard$ubarry'
| ~ 'salt$udix' ) ).
cnf(c15,hypothesis,
( 'mustard$ucole'
| ~ 'salt$ubarry'
| ~ 'salt$udix' ) ).
cnf(c17,hypothesis,
( 'mustard$ulang'
| 'mustard$udix'
| ~ 'mustard$ucole' ) ).
cnf(c20,hypothesis,
( 'salt$ulang'
| 'salt$udix'
| ~ 'mustard$ucole' ) ).
cnf(c26,hypothesis,
( 'mustard$umill'
| 'mustard$udix'
| ~ 'salt$udix' ) ).
cnf(c29,hypothesis,
( 'salt$umill'
| ~ 'mustard$ulang'
| ~ 'salt$ulang' ) ).
cnf(c30,hypothesis,
( 'salt$umill'
| ~ 'mustard$ubarry'
| ~ 'salt$ubarry' ) ).
cnf(c31,hypothesis,
( 'salt$ulang'
| ~ 'mustard$udix'
| 'salt$udix' ) ).
cnf(c34,hypothesis,
( 'salt$ulang'
| 'mustard$ubarry'
| ~ 'salt$ubarry' ) ).
cnf(c35,hypothesis,
( 'salt$udix'
| ~ 'mustard$ucole'
| ~ 'salt$ucole' ) ).
cnf(c36,hypothesis,
( 'mustard$ucole'
| ~ 'mustard$ulang'
| ~ 'salt$ulang' ) ).
cnf(c37,hypothesis,
( 'mustard$ucole'
| ~ 'mustard$udix'
| ~ 'salt$udix' ) ).
cnf(c39,hypothesis,
( 'salt$ucole'
| 'mustard$ubarry'
| ~ 'salt$ubarry' ) ).
cnf(c40,hypothesis,
( 'mustard$ubarry'
| ~ 'mustard$umill'
| ~ 'salt$umill' ) ).
cnf(c41,hypothesis,
( 'salt$ubarry'
| ~ 'mustard$ulang'
| 'salt$ulang' ) ).
cnf(c42,hypothesis,
( 'salt$ubarry'
| 'mustard$ulang'
| ~ 'salt$ulang' ) ).
cnf(c43,hypothesis,
( 'salt$ubarry'
| ~ 'mustard$ucole'
| 'salt$ucole' ) ).
cnf(c44,hypothesis,
( 'salt$ubarry'
| 'mustard$ucole'
| ~ 'salt$ucole' ) ).
cnf(c46,hypothesis,
( ~ 'salt$umill'
| ~ 'salt$ubarry'
| ~ 'mustard$ubarry'
| ~ 'salt$ucole' ) ).
cnf(c47,hypothesis,
( ~ 'mustard$umill'
| 'mustard$ubarry'
| 'salt$ubarry'
| ~ 'salt$ucole' ) ).
cnf(c49,hypothesis,
( ~ 'salt$udix'
| ~ 'mustard$udix'
| ~ 'salt$ucole'
| ~ 'mustard$ucole'
| ~ 'mustard$umill' ) ).
cnf(c50,hypothesis,
( 'mustard$udix'
| 'salt$udix'
| 'mustard$ucole'
| 'salt$ucole'
| ~ 'mustard$umill' ) ).
cnf(c52,hypothesis,
( 'mustard$udix'
| 'salt$udix'
| ~ 'salt$ubarry'
| ~ 'mustard$ubarry'
| ~ 'salt$ulang' ) ).
cnf(c53,hypothesis,
( ~ 'salt$udix'
| ~ 'mustard$udix'
| 'mustard$ubarry'
| 'salt$ubarry'
| ~ 'salt$ulang' ) ).
cnf(c56,hypothesis,
( 'mustard$ulang'
| 'mustard$umill'
| 'salt$umill' ) ).
cnf(c57,hypothesis,
( 'mustard$ulang'
| 'mustard$ucole'
| 'salt$ucole' ) ).
cnf(c59,hypothesis,
( 'mustard$udix'
| 'mustard$ulang'
| 'salt$ulang' ) ).
cnf(c60,hypothesis,
( 'salt$udix'
| 'mustard$ubarry'
| 'salt$ubarry' ) ).
cnf(c62,hypothesis,
( 'mustard$ubarry'
| 'mustard$udix'
| 'salt$udix' ) ).
cnf(prove_who_takes_what,negated_conjecture,
( 'mustard$umill'
| 'mustard$udix'
| 'salt$udix'
| 'mustard$ucole'
| 'salt$ucole'
| ~ 'mustard$ulang'
| ~ 'salt$umill'
| ~ 'salt$ubarry'
| ~ 'mustard$ubarry'
| 'salt$ulang' ) ).
cnf(c_0,plain,
( 'mustard$ulang'
| 'mustard$ubarry'
| ~ 'salt$umill' ),
inference(clausification,[status(esa)],[c1]) ).
cnf(c_2,plain,
( 'mustard$ulang'
| 'salt$ubarry'
| ~ 'salt$umill' ),
inference(clausification,[status(esa)],[c3]) ).
cnf(c_5,plain,
( ~ 'salt$umill'
| ~ 'mustard$ucole'
| ~ 'mustard$ulang' ),
inference(clausification,[status(esa)],[c6]) ).
cnf(c_6,plain,
( ~ 'mustard$umill'
| ~ 'salt$ucole'
| ~ 'mustard$ulang' ),
inference(clausification,[status(esa)],[c7]) ).
cnf(c_7,plain,
( ~ 'salt$umill'
| ~ 'salt$ucole'
| ~ 'mustard$ulang' ),
inference(clausification,[status(esa)],[c8]) ).
cnf(c_10,plain,
( ~ 'mustard$umill'
| ~ 'salt$ulang'
| ~ 'mustard$udix' ),
inference(clausification,[status(esa)],[c11]) ).
cnf(c_11,plain,
( ~ 'salt$umill'
| ~ 'salt$ulang'
| ~ 'mustard$udix' ),
inference(clausification,[status(esa)],[c12]) ).
cnf(c_13,plain,
( 'salt$ucole'
| ~ 'mustard$ubarry'
| ~ 'salt$udix' ),
inference(clausification,[status(esa)],[c14]) ).
cnf(c_14,plain,
( 'mustard$ucole'
| ~ 'salt$ubarry'
| ~ 'salt$udix' ),
inference(clausification,[status(esa)],[c15]) ).
cnf(c_16,plain,
( 'mustard$ulang'
| 'mustard$udix'
| ~ 'mustard$ucole' ),
inference(clausification,[status(esa)],[c17]) ).
cnf(c_19,plain,
( 'salt$ulang'
| 'salt$udix'
| ~ 'mustard$ucole' ),
inference(clausification,[status(esa)],[c20]) ).
cnf(c_25,plain,
( 'mustard$umill'
| 'mustard$udix'
| ~ 'salt$udix' ),
inference(clausification,[status(esa)],[c26]) ).
cnf(c_28,plain,
( 'salt$umill'
| ~ 'mustard$ulang'
| ~ 'salt$ulang' ),
inference(clausification,[status(esa)],[c29]) ).
cnf(c_29,plain,
( 'salt$umill'
| ~ 'mustard$ubarry'
| ~ 'salt$ubarry' ),
inference(clausification,[status(esa)],[c30]) ).
cnf(c_30,plain,
( 'salt$ulang'
| ~ 'mustard$udix'
| 'salt$udix' ),
inference(clausification,[status(esa)],[c31]) ).
cnf(c_33,plain,
( 'salt$ulang'
| 'mustard$ubarry'
| ~ 'salt$ubarry' ),
inference(clausification,[status(esa)],[c34]) ).
cnf(c_34,plain,
( 'salt$udix'
| ~ 'mustard$ucole'
| ~ 'salt$ucole' ),
inference(clausification,[status(esa)],[c35]) ).
cnf(c_35,plain,
( 'mustard$ucole'
| ~ 'mustard$ulang'
| ~ 'salt$ulang' ),
inference(clausification,[status(esa)],[c36]) ).
cnf(c_36,plain,
( 'mustard$ucole'
| ~ 'mustard$udix'
| ~ 'salt$udix' ),
inference(clausification,[status(esa)],[c37]) ).
cnf(c_38,plain,
( 'salt$ucole'
| 'mustard$ubarry'
| ~ 'salt$ubarry' ),
inference(clausification,[status(esa)],[c39]) ).
cnf(c_39,plain,
( 'mustard$ubarry'
| ~ 'mustard$umill'
| ~ 'salt$umill' ),
inference(clausification,[status(esa)],[c40]) ).
cnf(c_40,plain,
( 'salt$ubarry'
| ~ 'mustard$ulang'
| 'salt$ulang' ),
inference(clausification,[status(esa)],[c41]) ).
cnf(c_41,plain,
( 'salt$ubarry'
| 'mustard$ulang'
| ~ 'salt$ulang' ),
inference(clausification,[status(esa)],[c42]) ).
cnf(c_42,plain,
( 'salt$ubarry'
| ~ 'mustard$ucole'
| 'salt$ucole' ),
inference(clausification,[status(esa)],[c43]) ).
cnf(c_43,plain,
( 'salt$ubarry'
| 'mustard$ucole'
| ~ 'salt$ucole' ),
inference(clausification,[status(esa)],[c44]) ).
cnf(c_45,plain,
( ~ 'salt$umill'
| ~ 'salt$ubarry'
| ~ 'mustard$ubarry'
| ~ 'salt$ucole' ),
inference(clausification,[status(esa)],[c46]) ).
cnf(c_46,plain,
( ~ 'mustard$umill'
| 'mustard$ubarry'
| 'salt$ubarry'
| ~ 'salt$ucole' ),
inference(clausification,[status(esa)],[c47]) ).
cnf(c_48,plain,
( ~ 'mustard$udix'
| ~ 'salt$udix'
| ~ 'mustard$ucole'
| ~ 'salt$ucole'
| ~ 'mustard$umill' ),
inference(clausification,[status(esa)],[c49]) ).
cnf(c_49,plain,
( 'mustard$udix'
| 'salt$udix'
| 'salt$ucole'
| ~ 'mustard$umill'
| 'mustard$ucole' ),
inference(clausification,[status(esa)],[c50]) ).
cnf(c_51,plain,
( ~ 'mustard$ubarry'
| 'mustard$udix'
| ~ 'salt$ubarry'
| 'salt$udix'
| ~ 'salt$ulang' ),
inference(clausification,[status(esa)],[c52]) ).
cnf(c_52,plain,
( 'salt$ubarry'
| ~ 'mustard$udix'
| ~ 'salt$udix'
| 'mustard$ubarry'
| ~ 'salt$ulang' ),
inference(clausification,[status(esa)],[c53]) ).
cnf(c_55,plain,
( 'mustard$ulang'
| 'mustard$umill'
| 'salt$umill' ),
inference(clausification,[status(esa)],[c56]) ).
cnf(c_56,plain,
( 'mustard$ulang'
| 'mustard$ucole'
| 'salt$ucole' ),
inference(clausification,[status(esa)],[c57]) ).
cnf(c_58,plain,
( 'mustard$udix'
| 'mustard$ulang'
| 'salt$ulang' ),
inference(clausification,[status(esa)],[c59]) ).
cnf(c_59,plain,
( 'salt$udix'
| 'mustard$ubarry'
| 'salt$ubarry' ),
inference(clausification,[status(esa)],[c60]) ).
cnf(c_61,plain,
( 'mustard$ubarry'
| 'mustard$udix'
| 'salt$udix' ),
inference(clausification,[status(esa)],[c62]) ).
cnf(c_62,plain,
( ~ 'mustard$ubarry'
| 'mustard$umill'
| ~ 'mustard$ulang'
| ~ 'salt$umill'
| 'mustard$udix'
| ~ 'salt$ubarry'
| 'salt$ulang'
| 'salt$udix'
| 'salt$ucole'
| 'mustard$ucole' ),
inference(clausification,[status(esa)],[prove_who_takes_what]) ).
cnf(d0,plain,
( 'mustard$udix'
| 'mustard$umill'
| 'mustard$udix'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[c_61,c_25]) ).
cnf(d1,plain,
( 'mustard$ubarry'
| ~ 'salt$umill'
| 'mustard$udix'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d0,c_39]) ).
cnf(d2,plain,
( 'salt$ubarry'
| 'salt$ulang'
| 'mustard$udix'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[c_58,c_40]) ).
cnf(d3,plain,
( 'salt$ubarry'
| 'mustard$ulang'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d2,c_41]) ).
cnf(d4,plain,
( ~ 'mustard$ulang'
| 'salt$umill'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d2,c_28]) ).
cnf(d5,plain,
( 'mustard$udix'
| 'salt$ubarry'
| 'mustard$udix'
| 'salt$ubarry'
| 'salt$umill' ),
inference(resolution,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
( 'mustard$udix'
| 'mustard$ubarry'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d5,d1]) ).
cnf(d7,plain,
( 'salt$ubarry'
| 'mustard$ubarry'
| ~ 'mustard$udix'
| 'salt$ubarry'
| ~ 'salt$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[c_52,c_59]) ).
cnf(d8,plain,
( 'salt$ubarry'
| 'mustard$ubarry'
| 'salt$ubarry'
| ~ 'salt$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d7,d6]) ).
cnf(d9,plain,
( ~ 'mustard$udix'
| 'mustard$ucole'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[c_59,c_36]) ).
cnf(d10,plain,
( 'mustard$ucole'
| 'salt$ubarry'
| 'mustard$ubarry'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d6,d9]) ).
cnf(d11,plain,
( 'salt$ucole'
| 'salt$ubarry'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d10,c_42]) ).
cnf(d12,plain,
( ~ 'mustard$umill'
| 'salt$ubarry'
| 'mustard$ubarry'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d11,c_46]) ).
cnf(d13,plain,
( 'mustard$ulang'
| 'salt$umill'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d12,c_55]) ).
cnf(d14,plain,
( 'mustard$ulang'
| 'mustard$ubarry'
| 'salt$ubarry'
| 'mustard$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d13,c_0]) ).
cnf(d15,plain,
( 'salt$ubarry'
| 'salt$ulang'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d14,c_40]) ).
cnf(d16,plain,
( 'salt$ubarry'
| 'mustard$ubarry'
| 'salt$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d15,d8]) ).
cnf(d17,plain,
( 'salt$ulang'
| 'mustard$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d16,c_33]) ).
cnf(d18,plain,
( 'mustard$ucole'
| ~ 'salt$ubarry'
| 'mustard$udix'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[c_61,c_14]) ).
cnf(d19,plain,
( 'mustard$udix'
| 'mustard$ucole'
| 'mustard$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d16,d18]) ).
cnf(d20,plain,
( 'mustard$udix'
| 'mustard$ulang'
| 'mustard$udix'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d19,c_16]) ).
cnf(d21,plain,
( 'salt$ucole'
| 'mustard$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d16,c_38]) ).
cnf(d22,plain,
( ~ 'mustard$umill'
| ~ 'mustard$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d21,c_6]) ).
cnf(d23,plain,
( 'mustard$udix'
| 'mustard$ubarry'
| ~ 'mustard$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d22,d0]) ).
cnf(d24,plain,
( 'mustard$udix'
| 'mustard$ubarry'
| 'mustard$udix'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d23,d20]) ).
cnf(d25,plain,
( ~ 'salt$ulang'
| ~ 'salt$umill'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d24,c_11]) ).
cnf(d26,plain,
( 'mustard$ubarry'
| 'mustard$ubarry'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d25,d17]) ).
cnf(d27,plain,
( ~ 'mustard$ulang'
| 'salt$umill'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d17,c_28]) ).
cnf(d28,plain,
( ~ 'mustard$umill'
| ~ 'salt$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d24,c_10]) ).
cnf(d29,plain,
( 'mustard$ulang'
| 'salt$umill'
| ~ 'salt$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d28,c_55]) ).
cnf(d30,plain,
( 'mustard$ubarry'
| 'mustard$ulang'
| 'mustard$ubarry'
| 'salt$umill' ),
inference(resolution,[status(thm)],[d29,d17]) ).
cnf(d31,plain,
( 'mustard$ubarry'
| 'mustard$ulang'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d30,d26]) ).
cnf(d32,plain,
( 'mustard$ubarry'
| 'salt$umill'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d31,d27]) ).
cnf(d33,plain,
( 'mustard$ubarry'
| 'mustard$ubarry' ),
inference(resolution,[status(thm)],[d32,d26]) ).
cnf(d34,plain,
( ~ 'salt$udix'
| 'salt$ucole' ),
inference(resolution,[status(thm)],[d33,c_13]) ).
cnf(d35,plain,
( ~ 'salt$ucole'
| ~ 'salt$ubarry'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d33,c_45]) ).
cnf(d36,plain,
( 'salt$ubarry'
| 'salt$ulang'
| 'salt$ucole'
| 'mustard$ucole' ),
inference(resolution,[status(thm)],[c_56,c_40]) ).
cnf(d37,plain,
( 'salt$ucole'
| 'salt$ubarry'
| 'salt$ucole'
| 'salt$ubarry'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d36,c_42]) ).
cnf(d38,plain,
( 'mustard$ucole'
| ~ 'mustard$ulang'
| 'salt$ucole'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d37,c_35]) ).
cnf(d39,plain,
( 'salt$ucole'
| 'mustard$ucole'
| 'salt$ucole'
| 'mustard$ucole'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d38,c_56]) ).
cnf(d40,plain,
( 'salt$ucole'
| 'salt$ubarry'
| 'salt$ucole'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d39,c_42]) ).
cnf(d41,plain,
( ~ 'mustard$ulang'
| ~ 'salt$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d40,c_7]) ).
cnf(d42,plain,
( 'mustard$ucole'
| 'salt$ubarry'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d40,c_43]) ).
cnf(d43,plain,
( 'mustard$ucole'
| ~ 'mustard$ulang'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d2,c_35]) ).
cnf(d44,plain,
( 'mustard$udix'
| 'salt$ubarry'
| 'mustard$udix'
| 'mustard$ucole'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d43,d3]) ).
cnf(d45,plain,
( ~ 'mustard$ulang'
| ~ 'salt$umill'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d44,c_5]) ).
cnf(d46,plain,
( 'mustard$udix'
| 'salt$ubarry'
| 'mustard$udix'
| 'salt$ubarry'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d45,d3]) ).
cnf(d47,plain,
( 'mustard$udix'
| 'salt$ubarry'
| 'mustard$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d46,d5]) ).
cnf(d48,plain,
( 'salt$udix'
| ~ 'mustard$ucole'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d40,c_34]) ).
cnf(d49,plain,
( 'salt$ubarry'
| 'salt$udix'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d48,d42]) ).
cnf(d50,plain,
( ~ 'mustard$udix'
| ~ 'salt$ucole'
| ~ 'mustard$ucole'
| ~ 'mustard$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d49,c_48]) ).
cnf(d51,plain,
( 'salt$ubarry'
| ~ 'salt$ucole'
| ~ 'mustard$ucole'
| ~ 'mustard$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d50,d47]) ).
cnf(d52,plain,
( 'salt$ubarry'
| ~ 'mustard$ucole'
| ~ 'mustard$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d51,d40]) ).
cnf(d53,plain,
( 'salt$ubarry'
| ~ 'mustard$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d52,d42]) ).
cnf(d54,plain,
( 'mustard$ulang'
| 'salt$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d53,c_55]) ).
cnf(d55,plain,
( 'salt$ubarry'
| 'mustard$ulang'
| 'salt$ubarry'
| 'mustard$ulang' ),
inference(resolution,[status(thm)],[d54,c_2]) ).
cnf(d56,plain,
( 'salt$ubarry'
| ~ 'salt$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d55,d41]) ).
cnf(d57,plain,
( 'salt$ubarry'
| 'salt$ulang'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d55,c_40]) ).
cnf(d58,plain,
( ~ 'mustard$ulang'
| 'salt$umill'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d57,c_28]) ).
cnf(d59,plain,
( 'salt$ubarry'
| 'salt$ubarry'
| 'salt$umill' ),
inference(resolution,[status(thm)],[d58,d55]) ).
cnf(d60,plain,
( 'salt$ubarry'
| 'salt$ubarry' ),
inference(resolution,[status(thm)],[d59,d56]) ).
cnf(d61,plain,
( ~ 'salt$ucole'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d60,d35]) ).
cnf(d62,plain,
( ~ 'salt$ubarry'
| 'salt$umill' ),
inference(resolution,[status(thm)],[d33,c_29]) ).
cnf(d63,plain,
'salt$umill',
inference(resolution,[status(thm)],[d60,d62]) ).
cnf(d64,plain,
~ 'salt$ucole',
inference(resolution,[status(thm)],[d63,d61]) ).
cnf(d65,plain,
~ 'salt$udix',
inference(resolution,[status(thm)],[d64,d34]) ).
cnf(d66,plain,
( ~ 'mustard$udix'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d65,c_30]) ).
cnf(d67,plain,
( 'salt$udix'
| 'mustard$udix'
| ~ 'salt$ubarry'
| ~ 'salt$ulang' ),
inference(resolution,[status(thm)],[d33,c_51]) ).
cnf(d68,plain,
( 'salt$udix'
| 'mustard$udix'
| ~ 'salt$ulang' ),
inference(resolution,[status(thm)],[d60,d67]) ).
cnf(d69,plain,
( 'mustard$udix'
| ~ 'salt$ulang' ),
inference(resolution,[status(thm)],[d65,d68]) ).
cnf(d70,plain,
( ~ 'mustard$ucole'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d65,c_19]) ).
cnf(d71,plain,
( 'salt$udix'
| 'mustard$udix'
| 'salt$ucole'
| 'mustard$ucole'
| 'mustard$umill'
| ~ 'salt$ubarry'
| 'salt$ulang'
| ~ 'mustard$ulang'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d33,c_62]) ).
cnf(d72,plain,
( 'salt$udix'
| 'mustard$udix'
| 'salt$ucole'
| 'mustard$ucole'
| 'mustard$umill'
| 'salt$ulang'
| ~ 'mustard$ulang'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d60,d71]) ).
cnf(d73,plain,
( 'salt$ucole'
| 'mustard$ucole'
| 'salt$udix'
| 'mustard$udix'
| 'salt$ucole'
| 'mustard$ucole'
| 'mustard$umill'
| 'salt$ulang'
| ~ 'salt$umill' ),
inference(resolution,[status(thm)],[d72,c_56]) ).
cnf(d74,plain,
( 'salt$udix'
| 'mustard$udix'
| 'salt$ucole'
| 'mustard$ucole'
| 'mustard$umill'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d63,d73]) ).
cnf(d75,plain,
( 'salt$udix'
| 'mustard$udix'
| 'mustard$ucole'
| 'mustard$umill'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d64,d74]) ).
cnf(d76,plain,
( 'mustard$udix'
| 'mustard$ucole'
| 'mustard$umill'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d65,d75]) ).
cnf(d77,plain,
( 'salt$udix'
| 'mustard$udix'
| 'mustard$ucole'
| ~ 'mustard$umill' ),
inference(resolution,[status(thm)],[d64,c_49]) ).
cnf(d78,plain,
( 'mustard$udix'
| 'mustard$ucole'
| ~ 'mustard$umill' ),
inference(resolution,[status(thm)],[d65,d77]) ).
cnf(d79,plain,
( 'mustard$udix'
| 'mustard$ucole'
| 'salt$ulang'
| 'mustard$udix'
| 'mustard$ucole' ),
inference(resolution,[status(thm)],[d78,d76]) ).
cnf(d80,plain,
( 'salt$ulang'
| 'mustard$udix'
| 'salt$ulang' ),
inference(resolution,[status(thm)],[d79,d70]) ).
cnf(d81,plain,
( 'mustard$udix'
| 'mustard$udix' ),
inference(resolution,[status(thm)],[d80,d69]) ).
cnf(d82,plain,
'salt$ulang',
inference(resolution,[status(thm)],[d81,d66]) ).
cnf(d83,plain,
( ~ 'mustard$udix'
| ~ 'salt$ulang' ),
inference(resolution,[status(thm)],[d63,c_11]) ).
cnf(d84,plain,
~ 'salt$ulang',
inference(resolution,[status(thm)],[d81,d83]) ).
cnf(d85,plain,
$false,
inference(resolution,[status(thm)],[d84,d82]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 05:05:56 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.06/1.93 % SZS status Unsatisfiable for theBenchmark.p
% 12.06/1.93 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------