%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : PUZ030-1 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:23:12 AM UTC 2025
% Result : Unsatisfiable 0.18s 0.37s
% Output : Proof 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PUZ030-1 : TPTP v9.0.0. Released v1.0.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n010.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 02:42:11 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.18/0.37 % SZS status Unsatisfiable
% 0.18/0.37 % SZS output start Proof
% 0.18/0.37 tff(oneof_type, type, (
% 0.18/0.37 oneof: $i > $o)).
% 0.18/0.37 tff(mill_type, type, (
% 0.18/0.37 mill: $i)).
% 0.18/0.37 tff(mustard_type, type, (
% 0.18/0.37 mustard: $i > $o)).
% 0.18/0.37 tff(dix_type, type, (
% 0.18/0.37 dix: $i)).
% 0.18/0.37 tff(neither_type, type, (
% 0.18/0.37 neither: $i > $o)).
% 0.18/0.37 tff(barry_type, type, (
% 0.18/0.37 barry: $i)).
% 0.18/0.37 tff(both_type, type, (
% 0.18/0.37 both: $i > $o)).
% 0.18/0.37 tff(salt_type, type, (
% 0.18/0.37 salt: $i > $o)).
% 0.18/0.37 tff(lang_type, type, (
% 0.18/0.37 lang: $i)).
% 0.18/0.37 tff(cole_type, type, (
% 0.18/0.37 cole: $i)).
% 0.18/0.37 tff(1,assumption,(~oneof(mill)), introduced(assumption)).
% 0.18/0.37 tff(2,assumption,(~mustard(mill)), introduced(assumption)).
% 0.18/0.37 tff(3,plain,
% 0.18/0.37 (^[X: $i] : refl(((~both(X)) | mustard(X)) <=> ((~both(X)) | mustard(X)))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(4,plain,
% 0.18/0.37 (![X: $i] : ((~both(X)) | mustard(X)) <=> ![X: $i] : ((~both(X)) | mustard(X))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[3])).
% 0.18/0.37 tff(5,plain,
% 0.18/0.37 (![X: $i] : ((~both(X)) | mustard(X)) <=> ![X: $i] : ((~both(X)) | mustard(X))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(6,axiom,(![X: $i] : ((~both(X)) | mustard(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','both2')).
% 0.18/0.37 tff(7,plain,
% 0.18/0.37 (![X: $i] : ((~both(X)) | mustard(X))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.18/0.37 tff(8,plain,(
% 0.18/0.37 ![X: $i] : ((~both(X)) | mustard(X))),
% 0.18/0.37 inference(skolemize,[status(sab)],[7])).
% 0.18/0.37 tff(9,plain,
% 0.18/0.37 (![X: $i] : ((~both(X)) | mustard(X))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.18/0.37 tff(10,plain,
% 0.18/0.37 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(mill)) | mustard(mill))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(mill)) | mustard(mill))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(11,plain,
% 0.18/0.37 ((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(mill)) | mustard(mill))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(12,plain,
% 0.18/0.37 ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(mill)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[11, 10])).
% 0.18/0.37 tff(13,plain,
% 0.18/0.37 (~both(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[12, 9, 2])).
% 0.18/0.37 tff(14,plain,
% 0.18/0.37 (^[X: $i] : refl((both(X) | oneof(X) | neither(X)) <=> (both(X) | oneof(X) | neither(X)))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(15,plain,
% 0.18/0.37 (![X: $i] : (both(X) | oneof(X) | neither(X)) <=> ![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[14])).
% 0.18/0.37 tff(16,plain,
% 0.18/0.37 (![X: $i] : (both(X) | oneof(X) | neither(X)) <=> ![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(17,plain,
% 0.18/0.37 (^[X: $i] : rewrite(((both(X) | neither(X)) | oneof(X)) <=> (both(X) | oneof(X) | neither(X)))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(18,plain,
% 0.18/0.37 (![X: $i] : ((both(X) | neither(X)) | oneof(X)) <=> ![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[17])).
% 0.18/0.37 tff(19,axiom,(![X: $i] : ((both(X) | neither(X)) | oneof(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','one_condition_holds1')).
% 0.18/0.37 tff(20,plain,
% 0.18/0.37 (![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.18/0.37 tff(21,plain,
% 0.18/0.37 (![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.18/0.37 tff(22,plain,(
% 0.18/0.37 ![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(skolemize,[status(sab)],[21])).
% 0.18/0.37 tff(23,plain,
% 0.18/0.37 (![X: $i] : (both(X) | oneof(X) | neither(X))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[22, 15])).
% 0.18/0.37 tff(24,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(mill) | neither(mill) | oneof(mill))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | both(mill) | neither(mill) | oneof(mill))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(25,plain,
% 0.18/0.37 ((both(mill) | oneof(mill) | neither(mill)) <=> (both(mill) | neither(mill) | oneof(mill))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(26,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(mill) | oneof(mill) | neither(mill))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(mill) | neither(mill) | oneof(mill)))),
% 0.18/0.37 inference(monotonicity,[status(thm)],[25])).
% 0.18/0.37 tff(27,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(mill) | oneof(mill) | neither(mill))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | both(mill) | neither(mill) | oneof(mill))),
% 0.18/0.37 inference(transitivity,[status(thm)],[26, 24])).
% 0.18/0.37 tff(28,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(mill) | oneof(mill) | neither(mill))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(29,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | both(mill) | neither(mill) | oneof(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.18/0.37 tff(30,plain,
% 0.18/0.37 (both(mill) | neither(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[29, 23, 1])).
% 0.18/0.37 tff(31,plain,
% 0.18/0.37 (neither(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[30, 13])).
% 0.18/0.37 tff(32,plain,
% 0.18/0.37 (^[X: $i] : refl(((~neither(X)) | (~salt(X))) <=> ((~neither(X)) | (~salt(X))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(33,plain,
% 0.18/0.37 (![X: $i] : ((~neither(X)) | (~salt(X))) <=> ![X: $i] : ((~neither(X)) | (~salt(X)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[32])).
% 0.18/0.37 tff(34,plain,
% 0.18/0.37 (![X: $i] : ((~neither(X)) | (~salt(X))) <=> ![X: $i] : ((~neither(X)) | (~salt(X)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(35,axiom,(![X: $i] : ((~neither(X)) | (~salt(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neither2')).
% 0.18/0.37 tff(36,plain,
% 0.18/0.37 (![X: $i] : ((~neither(X)) | (~salt(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.18/0.37 tff(37,plain,(
% 0.18/0.37 ![X: $i] : ((~neither(X)) | (~salt(X)))),
% 0.18/0.37 inference(skolemize,[status(sab)],[36])).
% 0.18/0.37 tff(38,plain,
% 0.18/0.37 (![X: $i] : ((~neither(X)) | (~salt(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[37, 33])).
% 0.18/0.37 tff(39,plain,
% 0.18/0.37 (((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(mill)) | (~salt(mill)))) <=> ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(mill)) | (~salt(mill)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(40,plain,
% 0.18/0.37 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(mill)) | (~salt(mill)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(41,plain,
% 0.18/0.37 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(mill)) | (~salt(mill))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.18/0.37 tff(42,plain,
% 0.18/0.37 (~salt(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[41, 38, 31])).
% 0.18/0.37 tff(43,plain,
% 0.18/0.37 ((salt(mill) | (~both(barry))) <=> (salt(mill) | (~both(barry)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(44,plain,
% 0.18/0.37 (((~both(barry)) | salt(mill)) <=> (salt(mill) | (~both(barry)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(45,axiom,((~both(barry)) | salt(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule9_2')).
% 0.18/0.37 tff(46,plain,
% 0.18/0.37 (salt(mill) | (~both(barry))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.18/0.37 tff(47,plain,
% 0.18/0.37 (salt(mill) | (~both(barry))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[46, 43])).
% 0.18/0.37 tff(48,plain,
% 0.18/0.37 (~both(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[47, 42])).
% 0.18/0.37 tff(49,plain,
% 0.18/0.37 (((~neither(mill)) | mustard(lang)) <=> ((~neither(mill)) | mustard(lang))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(50,axiom,((~neither(mill)) | mustard(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule8_3')).
% 0.18/0.37 tff(51,plain,
% 0.18/0.37 ((~neither(mill)) | mustard(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.18/0.37 tff(52,plain,
% 0.18/0.37 ((~neither(mill)) | mustard(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[51, 49])).
% 0.18/0.37 tff(53,plain,
% 0.18/0.37 ((~neither(mill)) | mustard(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[52, 49])).
% 0.18/0.37 tff(54,plain,
% 0.18/0.37 ((~neither(mill)) | mustard(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[53, 49])).
% 0.18/0.37 tff(55,plain,
% 0.18/0.37 ((~neither(mill)) | mustard(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[54, 49])).
% 0.18/0.37 tff(56,plain,
% 0.18/0.37 (mustard(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[55, 31])).
% 0.18/0.37 tff(57,plain,
% 0.18/0.37 (((~both(lang)) | mustard(mill)) <=> ((~both(lang)) | mustard(mill))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(58,axiom,((~both(lang)) | mustard(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule9_3')).
% 0.18/0.37 tff(59,plain,
% 0.18/0.37 ((~both(lang)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.18/0.37 tff(60,plain,
% 0.18/0.37 ((~both(lang)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[59, 57])).
% 0.18/0.37 tff(61,plain,
% 0.18/0.37 ((~both(lang)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[60, 57])).
% 0.18/0.37 tff(62,plain,
% 0.18/0.37 ((~both(lang)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.18/0.37 tff(63,plain,
% 0.18/0.37 ((~both(lang)) | mustard(mill)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[62, 57])).
% 0.18/0.37 tff(64,plain,
% 0.18/0.37 (~both(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[63, 2])).
% 0.18/0.37 tff(65,plain,
% 0.18/0.37 (^[X: $i] : refl((both(X) | (~mustard(X)) | (~salt(X))) <=> (both(X) | (~mustard(X)) | (~salt(X))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(66,plain,
% 0.18/0.37 (![X: $i] : (both(X) | (~mustard(X)) | (~salt(X))) <=> ![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[65])).
% 0.18/0.37 tff(67,plain,
% 0.18/0.37 (![X: $i] : (both(X) | (~mustard(X)) | (~salt(X))) <=> ![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(68,plain,
% 0.18/0.37 (^[X: $i] : trans(monotonicity(rewrite(((~salt(X)) | (~mustard(X))) <=> ((~mustard(X)) | (~salt(X)))), ((((~salt(X)) | (~mustard(X))) | both(X)) <=> (((~mustard(X)) | (~salt(X))) | both(X)))), rewrite((((~mustard(X)) | (~salt(X))) | both(X)) <=> (both(X) | (~mustard(X)) | (~salt(X)))), ((((~salt(X)) | (~mustard(X))) | both(X)) <=> (both(X) | (~mustard(X)) | (~salt(X)))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(69,plain,
% 0.18/0.37 (![X: $i] : (((~salt(X)) | (~mustard(X))) | both(X)) <=> ![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[68])).
% 0.18/0.37 tff(70,axiom,(![X: $i] : (((~salt(X)) | (~mustard(X))) | both(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','both3')).
% 0.18/0.37 tff(71,plain,
% 0.18/0.37 (![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.18/0.37 tff(72,plain,
% 0.18/0.37 (![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[71, 67])).
% 0.18/0.37 tff(73,plain,(
% 0.18/0.37 ![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(skolemize,[status(sab)],[72])).
% 0.18/0.37 tff(74,plain,
% 0.18/0.37 (![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[73, 66])).
% 0.18/0.37 tff(75,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | (both(lang) | (~mustard(lang)) | (~salt(lang)))) <=> ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | both(lang) | (~mustard(lang)) | (~salt(lang)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(76,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | (both(lang) | (~mustard(lang)) | (~salt(lang)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(77,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | both(lang) | (~mustard(lang)) | (~salt(lang))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.18/0.37 tff(78,plain,
% 0.18/0.37 ((~mustard(lang)) | (~salt(lang))),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[77, 74, 64])).
% 0.18/0.37 tff(79,plain,
% 0.18/0.37 (~salt(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[78, 56])).
% 0.18/0.37 tff(80,plain,
% 0.18/0.37 (((~oneof(barry)) | salt(lang)) <=> ((~oneof(barry)) | salt(lang))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(81,axiom,((~oneof(barry)) | salt(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule7_2')).
% 0.18/0.37 tff(82,plain,
% 0.18/0.37 ((~oneof(barry)) | salt(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.18/0.37 tff(83,plain,
% 0.18/0.37 ((~oneof(barry)) | salt(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[82, 80])).
% 0.18/0.37 tff(84,plain,
% 0.18/0.37 ((~oneof(barry)) | salt(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[83, 80])).
% 0.18/0.37 tff(85,plain,
% 0.18/0.37 ((~oneof(barry)) | salt(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.18/0.37 tff(86,plain,
% 0.18/0.37 ((~oneof(barry)) | salt(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[85, 80])).
% 0.18/0.37 tff(87,plain,
% 0.18/0.37 (~oneof(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[86, 79])).
% 0.18/0.37 tff(88,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(barry) | neither(barry) | both(barry))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(barry) | neither(barry) | both(barry))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(89,plain,
% 0.18/0.37 ((both(barry) | oneof(barry) | neither(barry)) <=> (oneof(barry) | neither(barry) | both(barry))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(90,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(barry) | oneof(barry) | neither(barry))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(barry) | neither(barry) | both(barry)))),
% 0.18/0.37 inference(monotonicity,[status(thm)],[89])).
% 0.18/0.37 tff(91,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(barry) | oneof(barry) | neither(barry))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(barry) | neither(barry) | both(barry))),
% 0.18/0.37 inference(transitivity,[status(thm)],[90, 88])).
% 0.18/0.37 tff(92,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(barry) | oneof(barry) | neither(barry))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(93,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(barry) | neither(barry) | both(barry)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.18/0.37 tff(94,plain,
% 0.18/0.37 (neither(barry) | both(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[93, 23, 87])).
% 0.18/0.37 tff(95,plain,
% 0.18/0.37 (neither(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[94, 48])).
% 0.18/0.37 tff(96,plain,
% 0.18/0.37 (^[X: $i] : refl(((~mustard(X)) | (~neither(X))) <=> ((~mustard(X)) | (~neither(X))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(97,plain,
% 0.18/0.37 (![X: $i] : ((~mustard(X)) | (~neither(X))) <=> ![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[96])).
% 0.18/0.37 tff(98,plain,
% 0.18/0.37 (![X: $i] : ((~mustard(X)) | (~neither(X))) <=> ![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(99,plain,
% 0.18/0.37 (^[X: $i] : rewrite(((~neither(X)) | (~mustard(X))) <=> ((~mustard(X)) | (~neither(X))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(100,plain,
% 0.18/0.37 (![X: $i] : ((~neither(X)) | (~mustard(X))) <=> ![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[99])).
% 0.18/0.37 tff(101,axiom,(![X: $i] : ((~neither(X)) | (~mustard(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neither3')).
% 0.18/0.37 tff(102,plain,
% 0.18/0.37 (![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[101, 100])).
% 0.18/0.37 tff(103,plain,
% 0.18/0.37 (![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[102, 98])).
% 0.18/0.37 tff(104,plain,(
% 0.18/0.37 ![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(skolemize,[status(sab)],[103])).
% 0.18/0.37 tff(105,plain,
% 0.18/0.37 (![X: $i] : ((~mustard(X)) | (~neither(X)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[104, 97])).
% 0.18/0.37 tff(106,plain,
% 0.18/0.37 (((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(lang)) | (~neither(lang)))) <=> ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(lang)) | (~neither(lang)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(107,plain,
% 0.18/0.37 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(lang)) | (~neither(lang)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(108,plain,
% 0.18/0.37 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(lang)) | (~neither(lang))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.18/0.37 tff(109,plain,
% 0.18/0.37 (~neither(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[108, 105, 56])).
% 0.18/0.37 tff(110,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(lang) | both(lang) | neither(lang))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(lang) | both(lang) | neither(lang))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(111,plain,
% 0.18/0.37 ((both(lang) | oneof(lang) | neither(lang)) <=> (oneof(lang) | both(lang) | neither(lang))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(112,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(lang) | oneof(lang) | neither(lang))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(lang) | both(lang) | neither(lang)))),
% 0.18/0.37 inference(monotonicity,[status(thm)],[111])).
% 0.18/0.37 tff(113,plain,
% 0.18/0.37 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(lang) | oneof(lang) | neither(lang))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(lang) | both(lang) | neither(lang))),
% 0.18/0.37 inference(transitivity,[status(thm)],[112, 110])).
% 0.18/0.37 tff(114,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(lang) | oneof(lang) | neither(lang))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(115,plain,
% 0.18/0.37 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(lang) | both(lang) | neither(lang)),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[114, 113])).
% 0.18/0.37 tff(116,plain,
% 0.18/0.37 (oneof(lang) | neither(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[115, 23, 64])).
% 0.18/0.37 tff(117,plain,
% 0.18/0.37 (oneof(lang)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[116, 109])).
% 0.18/0.37 tff(118,plain,
% 0.18/0.37 ((salt(barry) | (~oneof(lang))) <=> (salt(barry) | (~oneof(lang)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(119,plain,
% 0.18/0.37 (((~oneof(lang)) | salt(barry)) <=> (salt(barry) | (~oneof(lang)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(120,axiom,((~oneof(lang)) | salt(barry)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule1_3')).
% 0.18/0.37 tff(121,plain,
% 0.18/0.37 (salt(barry) | (~oneof(lang))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[120, 119])).
% 0.18/0.37 tff(122,plain,
% 0.18/0.37 (salt(barry) | (~oneof(lang))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[121, 118])).
% 0.18/0.37 tff(123,plain,
% 0.18/0.37 (salt(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[122, 117])).
% 0.18/0.37 tff(124,plain,
% 0.18/0.37 (((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(barry)) | (~salt(barry)))) <=> ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(barry)) | (~salt(barry)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(125,plain,
% 0.18/0.37 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(barry)) | (~salt(barry)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(126,plain,
% 0.18/0.37 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(barry)) | (~salt(barry))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[125, 124])).
% 0.18/0.37 tff(127,plain,
% 0.18/0.37 ($false),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[126, 38, 123, 95])).
% 0.18/0.37 tff(128,plain,(mustard(mill) | oneof(mill)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.37 tff(129,plain,
% 0.18/0.37 (mustard(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[128, 1])).
% 0.18/0.37 tff(130,plain,
% 0.18/0.37 (((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(mill)) | (~neither(mill)))) <=> ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(mill)) | (~neither(mill)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(131,plain,
% 0.18/0.37 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(mill)) | (~neither(mill)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(132,plain,
% 0.18/0.37 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(mill)) | (~neither(mill))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.18/0.37 tff(133,plain,
% 0.18/0.37 (~neither(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[132, 105, 129])).
% 0.18/0.37 tff(134,plain,
% 0.18/0.37 (both(mill)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[30, 133])).
% 0.18/0.37 tff(135,plain,
% 0.18/0.37 ((mustard(barry) | (~both(mill))) <=> (mustard(barry) | (~both(mill)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(136,plain,
% 0.18/0.37 (((~both(mill)) | mustard(barry)) <=> (mustard(barry) | (~both(mill)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(137,axiom,((~both(mill)) | mustard(barry)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule2_3')).
% 0.18/0.37 tff(138,plain,
% 0.18/0.37 (mustard(barry) | (~both(mill))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.18/0.37 tff(139,plain,
% 0.18/0.37 (mustard(barry) | (~both(mill))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[138, 135])).
% 0.18/0.37 tff(140,plain,
% 0.18/0.37 (mustard(barry)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[139, 134])).
% 0.18/0.37 tff(141,plain,
% 0.18/0.37 (((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(barry)) | (~neither(barry)))) <=> ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(barry)) | (~neither(barry)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(142,plain,
% 0.18/0.37 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(barry)) | (~neither(barry)))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(143,plain,
% 0.18/0.38 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(barry)) | (~neither(barry))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.18/0.38 tff(144,plain,
% 0.18/0.38 (~neither(barry)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[143, 105, 140])).
% 0.18/0.38 tff(145,assumption,(mustard(mill)), introduced(assumption)).
% 0.18/0.38 tff(146,plain,
% 0.18/0.38 (~neither(mill)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[132, 105, 145])).
% 0.18/0.38 tff(147,assumption,(~salt(barry)), introduced(assumption)).
% 0.18/0.38 tff(148,plain,
% 0.18/0.38 ((salt(barry) | (~oneof(cole))) <=> (salt(barry) | (~oneof(cole)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(149,plain,
% 0.18/0.38 (((~oneof(cole)) | salt(barry)) <=> (salt(barry) | (~oneof(cole)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(150,axiom,((~oneof(cole)) | salt(barry)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule1_2')).
% 0.18/0.38 tff(151,plain,
% 0.18/0.38 (salt(barry) | (~oneof(cole))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[150, 149])).
% 0.18/0.38 tff(152,plain,
% 0.18/0.38 (salt(barry) | (~oneof(cole))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[151, 148])).
% 0.18/0.38 tff(153,plain,
% 0.18/0.38 (~oneof(cole)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[152, 147])).
% 0.18/0.38 tff(154,plain,
% 0.18/0.38 ((oneof(cole) | oneof(dix) | (~mustard(mill))) <=> (oneof(cole) | oneof(dix) | (~mustard(mill)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(155,plain,
% 0.18/0.38 (((oneof(cole) | (~mustard(mill))) | oneof(dix)) <=> (oneof(cole) | oneof(dix) | (~mustard(mill)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(156,plain,
% 0.18/0.38 (((~mustard(mill)) | oneof(cole)) <=> (oneof(cole) | (~mustard(mill)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(157,plain,
% 0.18/0.38 ((((~mustard(mill)) | oneof(cole)) | oneof(dix)) <=> ((oneof(cole) | (~mustard(mill))) | oneof(dix))),
% 0.18/0.38 inference(monotonicity,[status(thm)],[156])).
% 0.18/0.38 tff(158,plain,
% 0.18/0.38 ((((~mustard(mill)) | oneof(cole)) | oneof(dix)) <=> (oneof(cole) | oneof(dix) | (~mustard(mill)))),
% 0.18/0.38 inference(transitivity,[status(thm)],[157, 155])).
% 0.18/0.38 tff(159,axiom,(((~mustard(mill)) | oneof(cole)) | oneof(dix)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule10_1')).
% 0.18/0.38 tff(160,plain,
% 0.18/0.38 (oneof(cole) | oneof(dix) | (~mustard(mill))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.18/0.38 tff(161,plain,
% 0.18/0.38 (oneof(cole) | oneof(dix) | (~mustard(mill))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[160, 154])).
% 0.18/0.38 tff(162,plain,
% 0.18/0.38 (oneof(dix)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[161, 153, 145])).
% 0.18/0.38 tff(163,plain,
% 0.18/0.38 ((salt(lang) | (~oneof(dix))) <=> (salt(lang) | (~oneof(dix)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(164,plain,
% 0.18/0.38 (((~oneof(dix)) | salt(lang)) <=> (salt(lang) | (~oneof(dix)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(165,axiom,((~oneof(dix)) | salt(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule7_3')).
% 0.18/0.38 tff(166,plain,
% 0.18/0.38 (salt(lang) | (~oneof(dix))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[165, 164])).
% 0.18/0.38 tff(167,plain,
% 0.18/0.38 (salt(lang) | (~oneof(dix))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[166, 163])).
% 0.18/0.38 tff(168,plain,
% 0.18/0.38 (salt(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[167, 162])).
% 0.18/0.38 tff(169,plain,
% 0.18/0.38 (((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(lang)) | (~salt(lang)))) <=> ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(lang)) | (~salt(lang)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(170,plain,
% 0.18/0.38 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(lang)) | (~salt(lang)))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(171,plain,
% 0.18/0.38 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(lang)) | (~salt(lang))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.18/0.38 tff(172,plain,
% 0.18/0.38 (~neither(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[171, 38, 168])).
% 0.18/0.38 tff(173,plain,
% 0.18/0.38 (~oneof(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[122, 147])).
% 0.18/0.38 tff(174,plain,
% 0.18/0.38 (both(lang) | neither(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[115, 23, 173])).
% 0.18/0.38 tff(175,plain,
% 0.18/0.38 (both(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[174, 172])).
% 0.18/0.38 tff(176,plain,
% 0.18/0.38 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(lang)) | mustard(lang))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(lang)) | mustard(lang))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(177,plain,
% 0.18/0.38 ((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(lang)) | mustard(lang))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(178,plain,
% 0.18/0.38 ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(lang)) | mustard(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.18/0.38 tff(179,plain,
% 0.18/0.38 (mustard(lang)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[178, 9, 175])).
% 0.18/0.38 tff(180,assumption,(~neither(barry)), introduced(assumption)).
% 0.18/0.38 tff(181,plain,
% 0.18/0.38 ((neither(mill) | (~mustard(dix)) | neither(lang)) <=> (neither(mill) | (~mustard(dix)) | neither(lang))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(182,plain,
% 0.18/0.38 ((((~mustard(dix)) | neither(lang)) | neither(mill)) <=> (neither(mill) | (~mustard(dix)) | neither(lang))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(183,plain,
% 0.18/0.38 (((~mustard(dix)) | neither(lang)) <=> ((~mustard(dix)) | neither(lang))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(184,plain,
% 0.18/0.38 ((((~mustard(dix)) | neither(lang)) | neither(mill)) <=> (((~mustard(dix)) | neither(lang)) | neither(mill))),
% 0.18/0.38 inference(monotonicity,[status(thm)],[183])).
% 0.18/0.38 tff(185,plain,
% 0.18/0.38 ((((~mustard(dix)) | neither(lang)) | neither(mill)) <=> (neither(mill) | (~mustard(dix)) | neither(lang))),
% 0.18/0.38 inference(transitivity,[status(thm)],[184, 182])).
% 0.18/0.38 tff(186,axiom,(((~mustard(dix)) | neither(lang)) | neither(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule6_1')).
% 0.18/0.38 tff(187,plain,
% 0.18/0.38 (neither(mill) | (~mustard(dix)) | neither(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[186, 185])).
% 0.18/0.38 tff(188,plain,
% 0.18/0.38 (neither(mill) | (~mustard(dix)) | neither(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[187, 181])).
% 0.18/0.38 tff(189,plain,
% 0.18/0.38 (neither(mill) | (~mustard(dix)) | neither(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[188, 181])).
% 0.18/0.38 tff(190,plain,
% 0.18/0.38 (neither(mill) | (~mustard(dix)) | neither(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[189, 181])).
% 0.18/0.38 tff(191,plain,
% 0.18/0.38 (neither(mill) | (~mustard(dix)) | neither(lang)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[190, 181])).
% 0.18/0.38 tff(192,plain,
% 0.18/0.38 (~mustard(dix)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[191, 172, 146])).
% 0.18/0.38 tff(193,plain,
% 0.18/0.38 (^[X: $i] : refl((salt(X) | mustard(X) | (~oneof(X))) <=> (salt(X) | mustard(X) | (~oneof(X))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(194,plain,
% 0.18/0.38 (![X: $i] : (salt(X) | mustard(X) | (~oneof(X))) <=> ![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[193])).
% 0.18/0.38 tff(195,plain,
% 0.18/0.38 (![X: $i] : (salt(X) | mustard(X) | (~oneof(X))) <=> ![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(196,plain,
% 0.18/0.38 (^[X: $i] : trans(monotonicity(rewrite(((~oneof(X)) | salt(X)) <=> (salt(X) | (~oneof(X)))), ((((~oneof(X)) | salt(X)) | mustard(X)) <=> ((salt(X) | (~oneof(X))) | mustard(X)))), rewrite(((salt(X) | (~oneof(X))) | mustard(X)) <=> (salt(X) | mustard(X) | (~oneof(X)))), ((((~oneof(X)) | salt(X)) | mustard(X)) <=> (salt(X) | mustard(X) | (~oneof(X)))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(197,plain,
% 0.18/0.38 (![X: $i] : (((~oneof(X)) | salt(X)) | mustard(X)) <=> ![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[196])).
% 0.18/0.38 tff(198,axiom,(![X: $i] : (((~oneof(X)) | salt(X)) | mustard(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','oneof1')).
% 0.18/0.38 tff(199,plain,
% 0.18/0.38 (![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[198, 197])).
% 0.18/0.38 tff(200,plain,
% 0.18/0.38 (![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[199, 195])).
% 0.18/0.38 tff(201,plain,(
% 0.18/0.38 ![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(skolemize,[status(sab)],[200])).
% 0.18/0.38 tff(202,plain,
% 0.18/0.38 (![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[201, 194])).
% 0.18/0.38 tff(203,plain,
% 0.18/0.38 (((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | (salt(dix) | mustard(dix) | (~oneof(dix)))) <=> ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | salt(dix) | mustard(dix) | (~oneof(dix)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(204,plain,
% 0.18/0.38 ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | (salt(dix) | mustard(dix) | (~oneof(dix)))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(205,plain,
% 0.18/0.38 ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | salt(dix) | mustard(dix) | (~oneof(dix))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[204, 203])).
% 0.18/0.38 tff(206,plain,
% 0.18/0.38 (salt(dix) | mustard(dix)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[205, 202, 162])).
% 0.18/0.38 tff(207,plain,
% 0.18/0.38 (salt(dix)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[206, 192])).
% 0.18/0.38 tff(208,plain,
% 0.18/0.38 (((~salt(dix)) | neither(barry) | both(cole)) <=> ((~salt(dix)) | neither(barry) | both(cole))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(209,plain,
% 0.18/0.38 ((((~salt(dix)) | neither(barry)) | both(cole)) <=> ((~salt(dix)) | neither(barry) | both(cole))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(210,plain,
% 0.18/0.38 (((~salt(dix)) | neither(barry)) <=> ((~salt(dix)) | neither(barry))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(211,plain,
% 0.18/0.38 ((((~salt(dix)) | neither(barry)) | both(cole)) <=> (((~salt(dix)) | neither(barry)) | both(cole))),
% 0.18/0.38 inference(monotonicity,[status(thm)],[210])).
% 0.18/0.38 tff(212,plain,
% 0.18/0.38 ((((~salt(dix)) | neither(barry)) | both(cole)) <=> ((~salt(dix)) | neither(barry) | both(cole))),
% 0.18/0.38 inference(transitivity,[status(thm)],[211, 209])).
% 0.18/0.38 tff(213,axiom,(((~salt(dix)) | neither(barry)) | both(cole)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule5_1')).
% 0.18/0.38 tff(214,plain,
% 0.18/0.38 ((~salt(dix)) | neither(barry) | both(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[213, 212])).
% 0.18/0.38 tff(215,plain,
% 0.18/0.38 ((~salt(dix)) | neither(barry) | both(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[214, 208])).
% 0.18/0.38 tff(216,plain,
% 0.18/0.38 ((~salt(dix)) | neither(barry) | both(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[215, 208])).
% 0.18/0.38 tff(217,plain,
% 0.18/0.38 ((~salt(dix)) | neither(barry) | both(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[216, 208])).
% 0.18/0.38 tff(218,plain,
% 0.18/0.38 ((~salt(dix)) | neither(barry) | both(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[217, 208])).
% 0.18/0.38 tff(219,plain,
% 0.18/0.38 (both(cole)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[218, 207, 180])).
% 0.18/0.38 tff(220,plain,
% 0.18/0.38 (^[X: $i] : refl(((~both(X)) | (~neither(X))) <=> ((~both(X)) | (~neither(X))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(221,plain,
% 0.18/0.38 (![X: $i] : ((~both(X)) | (~neither(X))) <=> ![X: $i] : ((~both(X)) | (~neither(X)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[220])).
% 0.18/0.38 tff(222,plain,
% 0.18/0.38 (![X: $i] : ((~both(X)) | (~neither(X))) <=> ![X: $i] : ((~both(X)) | (~neither(X)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(223,axiom,(![X: $i] : ((~both(X)) | (~neither(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neither1')).
% 0.18/0.38 tff(224,plain,
% 0.18/0.38 (![X: $i] : ((~both(X)) | (~neither(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[223, 222])).
% 0.18/0.38 tff(225,plain,(
% 0.18/0.38 ![X: $i] : ((~both(X)) | (~neither(X)))),
% 0.18/0.38 inference(skolemize,[status(sab)],[224])).
% 0.18/0.38 tff(226,plain,
% 0.18/0.38 (![X: $i] : ((~both(X)) | (~neither(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[225, 221])).
% 0.18/0.38 tff(227,plain,
% 0.18/0.38 (((~![X: $i] : ((~both(X)) | (~neither(X)))) | ((~both(cole)) | (~neither(cole)))) <=> ((~![X: $i] : ((~both(X)) | (~neither(X)))) | (~both(cole)) | (~neither(cole)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(228,plain,
% 0.18/0.38 ((~![X: $i] : ((~both(X)) | (~neither(X)))) | ((~both(cole)) | (~neither(cole)))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(229,plain,
% 0.18/0.38 ((~![X: $i] : ((~both(X)) | (~neither(X)))) | (~both(cole)) | (~neither(cole))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[228, 227])).
% 0.18/0.38 tff(230,plain,
% 0.18/0.38 (~neither(cole)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[229, 226, 219])).
% 0.18/0.38 tff(231,plain,
% 0.18/0.38 ((neither(mill) | (~mustard(lang)) | neither(cole)) <=> (neither(mill) | (~mustard(lang)) | neither(cole))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(232,plain,
% 0.18/0.38 ((((~mustard(lang)) | neither(cole)) | neither(mill)) <=> (neither(mill) | (~mustard(lang)) | neither(cole))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(233,plain,
% 0.18/0.38 (((~mustard(lang)) | neither(cole)) <=> ((~mustard(lang)) | neither(cole))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(234,plain,
% 0.18/0.38 ((((~mustard(lang)) | neither(cole)) | neither(mill)) <=> (((~mustard(lang)) | neither(cole)) | neither(mill))),
% 0.18/0.38 inference(monotonicity,[status(thm)],[233])).
% 0.18/0.38 tff(235,plain,
% 0.18/0.38 ((((~mustard(lang)) | neither(cole)) | neither(mill)) <=> (neither(mill) | (~mustard(lang)) | neither(cole))),
% 0.18/0.38 inference(transitivity,[status(thm)],[234, 232])).
% 0.18/0.38 tff(236,axiom,(((~mustard(lang)) | neither(cole)) | neither(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule8_1')).
% 0.18/0.38 tff(237,plain,
% 0.18/0.38 (neither(mill) | (~mustard(lang)) | neither(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[236, 235])).
% 0.18/0.38 tff(238,plain,
% 0.18/0.38 (neither(mill) | (~mustard(lang)) | neither(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[237, 231])).
% 0.18/0.38 tff(239,plain,
% 0.18/0.38 (neither(mill) | (~mustard(lang)) | neither(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[238, 231])).
% 0.18/0.38 tff(240,plain,
% 0.18/0.38 (neither(mill) | (~mustard(lang)) | neither(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[239, 231])).
% 0.18/0.38 tff(241,plain,
% 0.18/0.38 (neither(mill) | (~mustard(lang)) | neither(cole)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[240, 231])).
% 0.18/0.38 tff(242,plain,
% 0.18/0.38 ($false),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[241, 230, 179, 146])).
% 0.18/0.38 tff(243,plain,(salt(barry) | neither(barry) | (~mustard(mill))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.38 tff(244,plain,
% 0.18/0.38 (salt(barry)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[243, 144, 129])).
% 0.18/0.38 tff(245,plain,
% 0.18/0.38 (^[X: $i] : refl(((~mustard(X)) | (~salt(X)) | (~oneof(X))) <=> ((~mustard(X)) | (~salt(X)) | (~oneof(X))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(246,plain,
% 0.18/0.38 (![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X))) <=> ![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[245])).
% 0.18/0.38 tff(247,plain,
% 0.18/0.38 (![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X))) <=> ![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(248,plain,
% 0.18/0.38 (^[X: $i] : rewrite((((~oneof(X)) | (~salt(X))) | (~mustard(X))) <=> ((~mustard(X)) | (~salt(X)) | (~oneof(X))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(249,plain,
% 0.18/0.38 (![X: $i] : (((~oneof(X)) | (~salt(X))) | (~mustard(X))) <=> ![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[248])).
% 0.18/0.38 tff(250,axiom,(![X: $i] : (((~oneof(X)) | (~salt(X))) | (~mustard(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','oneof4')).
% 0.18/0.38 tff(251,plain,
% 0.18/0.38 (![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[250, 249])).
% 0.18/0.38 tff(252,plain,
% 0.18/0.38 (![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[251, 247])).
% 0.18/0.38 tff(253,plain,(
% 0.18/0.38 ![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(skolemize,[status(sab)],[252])).
% 0.18/0.38 tff(254,plain,
% 0.18/0.38 (![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[253, 246])).
% 0.18/0.38 tff(255,plain,
% 0.18/0.38 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(barry)) | (~mustard(barry)) | (~oneof(barry)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(barry)) | (~mustard(barry)) | (~oneof(barry)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(256,plain,
% 0.18/0.38 (((~mustard(barry)) | (~salt(barry)) | (~oneof(barry))) <=> ((~salt(barry)) | (~mustard(barry)) | (~oneof(barry)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(257,plain,
% 0.18/0.38 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(barry)) | (~salt(barry)) | (~oneof(barry)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(barry)) | (~mustard(barry)) | (~oneof(barry))))),
% 0.18/0.38 inference(monotonicity,[status(thm)],[256])).
% 0.18/0.38 tff(258,plain,
% 0.18/0.39 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(barry)) | (~salt(barry)) | (~oneof(barry)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(barry)) | (~mustard(barry)) | (~oneof(barry)))),
% 0.18/0.39 inference(transitivity,[status(thm)],[257, 255])).
% 0.18/0.39 tff(259,plain,
% 0.18/0.39 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(barry)) | (~salt(barry)) | (~oneof(barry)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(260,plain,
% 0.18/0.39 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(barry)) | (~mustard(barry)) | (~oneof(barry))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[259, 258])).
% 0.18/0.39 tff(261,plain,
% 0.18/0.39 ((~salt(barry)) | (~oneof(barry))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[260, 254, 140])).
% 0.18/0.39 tff(262,plain,
% 0.18/0.39 (~oneof(barry)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[261, 244])).
% 0.18/0.39 tff(263,plain,
% 0.18/0.39 (((~salt(cole)) | oneof(barry) | neither(mill)) <=> ((~salt(cole)) | oneof(barry) | neither(mill))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(264,plain,
% 0.18/0.39 ((((~salt(cole)) | oneof(barry)) | neither(mill)) <=> ((~salt(cole)) | oneof(barry) | neither(mill))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(265,plain,
% 0.18/0.39 (((~salt(cole)) | oneof(barry)) <=> ((~salt(cole)) | oneof(barry))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(266,plain,
% 0.18/0.39 ((((~salt(cole)) | oneof(barry)) | neither(mill)) <=> (((~salt(cole)) | oneof(barry)) | neither(mill))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[265])).
% 0.18/0.39 tff(267,plain,
% 0.18/0.39 ((((~salt(cole)) | oneof(barry)) | neither(mill)) <=> ((~salt(cole)) | oneof(barry) | neither(mill))),
% 0.18/0.39 inference(transitivity,[status(thm)],[266, 264])).
% 0.18/0.39 tff(268,axiom,(((~salt(cole)) | oneof(barry)) | neither(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule3_1')).
% 0.18/0.39 tff(269,plain,
% 0.18/0.39 ((~salt(cole)) | oneof(barry) | neither(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[268, 267])).
% 0.18/0.39 tff(270,plain,
% 0.18/0.39 ((~salt(cole)) | oneof(barry) | neither(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[269, 263])).
% 0.18/0.39 tff(271,plain,
% 0.18/0.39 ((~salt(cole)) | oneof(barry) | neither(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[270, 263])).
% 0.18/0.39 tff(272,plain,
% 0.18/0.39 ((~salt(cole)) | oneof(barry) | neither(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[271, 263])).
% 0.18/0.39 tff(273,plain,
% 0.18/0.39 ((~salt(cole)) | oneof(barry) | neither(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[272, 263])).
% 0.18/0.39 tff(274,plain,
% 0.18/0.39 (~salt(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[273, 262, 133])).
% 0.18/0.39 tff(275,plain,
% 0.18/0.39 (^[X: $i] : refl((salt(X) | (~both(X))) <=> (salt(X) | (~both(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(276,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | (~both(X))) <=> ![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[275])).
% 0.18/0.39 tff(277,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | (~both(X))) <=> ![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(278,plain,
% 0.18/0.39 (^[X: $i] : rewrite(((~both(X)) | salt(X)) <=> (salt(X) | (~both(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(279,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | salt(X)) <=> ![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[278])).
% 0.18/0.39 tff(280,axiom,(![X: $i] : ((~both(X)) | salt(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','both1')).
% 0.18/0.39 tff(281,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[280, 279])).
% 0.18/0.39 tff(282,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[281, 277])).
% 0.18/0.39 tff(283,plain,(
% 0.18/0.39 ![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[282])).
% 0.18/0.39 tff(284,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | (~both(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[283, 276])).
% 0.18/0.39 tff(285,plain,
% 0.18/0.39 (((~![X: $i] : (salt(X) | (~both(X)))) | (salt(cole) | (~both(cole)))) <=> ((~![X: $i] : (salt(X) | (~both(X)))) | salt(cole) | (~both(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(286,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | (~both(X)))) | (salt(cole) | (~both(cole)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(287,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | (~both(X)))) | salt(cole) | (~both(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[286, 285])).
% 0.18/0.39 tff(288,plain,
% 0.18/0.39 (~both(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[287, 284, 274])).
% 0.18/0.39 tff(289,plain,
% 0.18/0.39 (~salt(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[218, 288, 144])).
% 0.18/0.39 tff(290,plain,
% 0.18/0.39 (((~![X: $i] : (salt(X) | (~both(X)))) | (salt(dix) | (~both(dix)))) <=> ((~![X: $i] : (salt(X) | (~both(X)))) | salt(dix) | (~both(dix)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(291,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | (~both(X)))) | (salt(dix) | (~both(dix)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(292,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | (~both(X)))) | salt(dix) | (~both(dix))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[291, 290])).
% 0.18/0.39 tff(293,plain,
% 0.18/0.39 (~both(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[292, 284, 289])).
% 0.18/0.39 tff(294,assumption,(~mustard(lang)), introduced(assumption)).
% 0.18/0.39 tff(295,assumption,(~both(dix)), introduced(assumption)).
% 0.18/0.39 tff(296,plain,
% 0.18/0.39 ((mustard(lang) | (~neither(cole))) <=> (mustard(lang) | (~neither(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(297,plain,
% 0.18/0.39 (((~neither(cole)) | mustard(lang)) <=> (mustard(lang) | (~neither(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(298,axiom,((~neither(cole)) | mustard(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule8_2')).
% 0.18/0.39 tff(299,plain,
% 0.18/0.39 (mustard(lang) | (~neither(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[298, 297])).
% 0.18/0.39 tff(300,plain,
% 0.18/0.39 (mustard(lang) | (~neither(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[299, 296])).
% 0.18/0.39 tff(301,plain,
% 0.18/0.39 (~neither(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[300, 294])).
% 0.18/0.39 tff(302,assumption,(~salt(cole)), introduced(assumption)).
% 0.18/0.39 tff(303,plain,
% 0.18/0.39 (^[X: $i] : refl((salt(X) | mustard(X) | neither(X)) <=> (salt(X) | mustard(X) | neither(X)))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(304,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | mustard(X) | neither(X)) <=> ![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[303])).
% 0.18/0.39 tff(305,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | mustard(X) | neither(X)) <=> ![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(306,plain,
% 0.18/0.39 (^[X: $i] : trans(monotonicity(rewrite((salt(X) | mustard(X)) <=> (salt(X) | mustard(X))), (((salt(X) | mustard(X)) | neither(X)) <=> ((salt(X) | mustard(X)) | neither(X)))), rewrite(((salt(X) | mustard(X)) | neither(X)) <=> (salt(X) | mustard(X) | neither(X))), (((salt(X) | mustard(X)) | neither(X)) <=> (salt(X) | mustard(X) | neither(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(307,plain,
% 0.18/0.39 (![X: $i] : ((salt(X) | mustard(X)) | neither(X)) <=> ![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[306])).
% 0.18/0.39 tff(308,axiom,(![X: $i] : ((salt(X) | mustard(X)) | neither(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neither4')).
% 0.18/0.39 tff(309,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[308, 307])).
% 0.18/0.39 tff(310,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[309, 305])).
% 0.18/0.39 tff(311,plain,(
% 0.18/0.39 ![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(skolemize,[status(sab)],[310])).
% 0.18/0.39 tff(312,plain,
% 0.18/0.39 (![X: $i] : (salt(X) | mustard(X) | neither(X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[311, 304])).
% 0.18/0.39 tff(313,plain,
% 0.18/0.39 (((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (salt(cole) | mustard(cole) | neither(cole))) <=> ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | salt(cole) | mustard(cole) | neither(cole))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(314,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (salt(cole) | mustard(cole) | neither(cole))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(315,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | salt(cole) | mustard(cole) | neither(cole)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[314, 313])).
% 0.18/0.39 tff(316,plain,
% 0.18/0.39 (mustard(cole) | neither(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[315, 312, 302])).
% 0.18/0.39 tff(317,plain,
% 0.18/0.39 (mustard(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[316, 301])).
% 0.18/0.39 tff(318,plain,
% 0.18/0.39 (((~mustard(cole)) | both(dix) | both(lang)) <=> ((~mustard(cole)) | both(dix) | both(lang))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(319,plain,
% 0.18/0.39 ((((~mustard(cole)) | both(dix)) | both(lang)) <=> ((~mustard(cole)) | both(dix) | both(lang))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(320,plain,
% 0.18/0.39 (((~mustard(cole)) | both(dix)) <=> ((~mustard(cole)) | both(dix))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(321,plain,
% 0.18/0.39 ((((~mustard(cole)) | both(dix)) | both(lang)) <=> (((~mustard(cole)) | both(dix)) | both(lang))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[320])).
% 0.18/0.39 tff(322,plain,
% 0.18/0.39 ((((~mustard(cole)) | both(dix)) | both(lang)) <=> ((~mustard(cole)) | both(dix) | both(lang))),
% 0.18/0.39 inference(transitivity,[status(thm)],[321, 319])).
% 0.18/0.39 tff(323,axiom,(((~mustard(cole)) | both(dix)) | both(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule4_1')).
% 0.18/0.39 tff(324,plain,
% 0.18/0.39 ((~mustard(cole)) | both(dix) | both(lang)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[323, 322])).
% 0.18/0.39 tff(325,plain,
% 0.18/0.39 ((~mustard(cole)) | both(dix) | both(lang)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[324, 318])).
% 0.18/0.39 tff(326,plain,
% 0.18/0.39 ((~mustard(cole)) | both(dix) | both(lang)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[325, 318])).
% 0.18/0.39 tff(327,plain,
% 0.18/0.39 ((~mustard(cole)) | both(dix) | both(lang)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[326, 318])).
% 0.18/0.39 tff(328,plain,
% 0.18/0.39 ((~mustard(cole)) | both(dix) | both(lang)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[327, 318])).
% 0.18/0.39 tff(329,plain,
% 0.18/0.39 (both(lang)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[328, 317, 295])).
% 0.18/0.39 tff(330,plain,
% 0.18/0.39 ($false),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[178, 9, 329, 294])).
% 0.18/0.39 tff(331,plain,(mustard(lang) | both(dix) | salt(cole)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.39 tff(332,plain,
% 0.18/0.39 (mustard(lang)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[331, 293, 274])).
% 0.18/0.39 tff(333,plain,
% 0.18/0.39 (~neither(lang)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[108, 105, 332])).
% 0.18/0.39 tff(334,plain,
% 0.18/0.39 (~mustard(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[191, 333, 133])).
% 0.18/0.39 tff(335,plain,
% 0.18/0.39 (neither(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[241, 332, 133])).
% 0.18/0.39 tff(336,plain,
% 0.18/0.39 (^[X: $i] : refl(((~oneof(X)) | (~neither(X))) <=> ((~oneof(X)) | (~neither(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(337,plain,
% 0.18/0.39 (![X: $i] : ((~oneof(X)) | (~neither(X))) <=> ![X: $i] : ((~oneof(X)) | (~neither(X)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[336])).
% 0.18/0.39 tff(338,plain,
% 0.18/0.39 (![X: $i] : ((~oneof(X)) | (~neither(X))) <=> ![X: $i] : ((~oneof(X)) | (~neither(X)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(339,axiom,(![X: $i] : ((~oneof(X)) | (~neither(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','oneof3')).
% 0.18/0.39 tff(340,plain,
% 0.18/0.39 (![X: $i] : ((~oneof(X)) | (~neither(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[339, 338])).
% 0.18/0.39 tff(341,plain,(
% 0.18/0.39 ![X: $i] : ((~oneof(X)) | (~neither(X)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[340])).
% 0.18/0.39 tff(342,plain,
% 0.18/0.39 (![X: $i] : ((~oneof(X)) | (~neither(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[341, 337])).
% 0.18/0.39 tff(343,plain,
% 0.18/0.39 (((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~oneof(cole)) | (~neither(cole)))) <=> ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | (~oneof(cole)) | (~neither(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(344,plain,
% 0.18/0.39 ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~oneof(cole)) | (~neither(cole)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(345,plain,
% 0.18/0.39 ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | (~oneof(cole)) | (~neither(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[344, 343])).
% 0.18/0.39 tff(346,plain,
% 0.18/0.39 (~oneof(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[345, 342, 335])).
% 0.18/0.39 tff(347,plain,
% 0.18/0.39 (oneof(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[161, 346, 129])).
% 0.18/0.39 tff(348,plain,
% 0.18/0.39 (mustard(dix) | (~oneof(dix))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[205, 202, 289])).
% 0.18/0.39 tff(349,plain,
% 0.18/0.39 ($false),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[348, 347, 334])).
% 0.18/0.39 tff(350,plain,(oneof(mill)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.39 tff(351,plain,
% 0.18/0.39 (((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~neither(mill)) | (~oneof(mill)))) <=> ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | (~neither(mill)) | (~oneof(mill)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(352,plain,
% 0.18/0.39 (((~oneof(mill)) | (~neither(mill))) <=> ((~neither(mill)) | (~oneof(mill)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(353,plain,
% 0.18/0.39 (((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~oneof(mill)) | (~neither(mill)))) <=> ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~neither(mill)) | (~oneof(mill))))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[352])).
% 0.18/0.39 tff(354,plain,
% 0.18/0.39 (((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~oneof(mill)) | (~neither(mill)))) <=> ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | (~neither(mill)) | (~oneof(mill)))),
% 0.18/0.39 inference(transitivity,[status(thm)],[353, 351])).
% 0.18/0.39 tff(355,plain,
% 0.18/0.39 ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | ((~oneof(mill)) | (~neither(mill)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(356,plain,
% 0.18/0.39 ((~![X: $i] : ((~oneof(X)) | (~neither(X)))) | (~neither(mill)) | (~oneof(mill))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[355, 354])).
% 0.18/0.39 tff(357,plain,
% 0.18/0.39 (~neither(mill)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[356, 342, 350])).
% 0.18/0.39 tff(358,plain,
% 0.18/0.39 (~both(lang)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[178, 9, 294])).
% 0.18/0.39 tff(359,plain,
% 0.18/0.39 (^[X: $i] : refl(((~both(X)) | (~oneof(X))) <=> ((~both(X)) | (~oneof(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(360,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | (~oneof(X))) <=> ![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[359])).
% 0.18/0.39 tff(361,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | (~oneof(X))) <=> ![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(362,plain,
% 0.18/0.39 (^[X: $i] : rewrite(((~oneof(X)) | (~both(X))) <=> ((~both(X)) | (~oneof(X))))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(363,plain,
% 0.18/0.39 (![X: $i] : ((~oneof(X)) | (~both(X))) <=> ![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[362])).
% 0.18/0.39 tff(364,axiom,(![X: $i] : ((~oneof(X)) | (~both(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','oneof2')).
% 0.18/0.39 tff(365,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[364, 363])).
% 0.18/0.39 tff(366,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[365, 361])).
% 0.18/0.39 tff(367,plain,(
% 0.18/0.39 ![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(skolemize,[status(sab)],[366])).
% 0.18/0.39 tff(368,plain,
% 0.18/0.39 (![X: $i] : ((~both(X)) | (~oneof(X)))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[367, 360])).
% 0.18/0.39 tff(369,plain,
% 0.18/0.39 (((~![X: $i] : ((~both(X)) | (~oneof(X)))) | ((~both(mill)) | (~oneof(mill)))) <=> ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | (~both(mill)) | (~oneof(mill)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(370,plain,
% 0.18/0.39 ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | ((~both(mill)) | (~oneof(mill)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(371,plain,
% 0.18/0.39 ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | (~both(mill)) | (~oneof(mill))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[370, 369])).
% 0.18/0.39 tff(372,plain,
% 0.18/0.39 (~both(mill)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[371, 368, 350])).
% 0.18/0.39 tff(373,plain,
% 0.18/0.39 (((~oneof(cole)) | mustard(mill)) <=> ((~oneof(cole)) | mustard(mill))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(374,axiom,((~oneof(cole)) | mustard(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule10_2')).
% 0.18/0.39 tff(375,plain,
% 0.18/0.39 ((~oneof(cole)) | mustard(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[374, 373])).
% 0.18/0.39 tff(376,plain,
% 0.18/0.39 ((~oneof(cole)) | mustard(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[375, 373])).
% 0.18/0.39 tff(377,plain,
% 0.18/0.39 ((~oneof(cole)) | mustard(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[376, 373])).
% 0.18/0.39 tff(378,plain,
% 0.18/0.39 ((~oneof(cole)) | mustard(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[377, 373])).
% 0.18/0.39 tff(379,plain,
% 0.18/0.39 ((~oneof(cole)) | mustard(mill)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[378, 373])).
% 0.18/0.39 tff(380,plain,
% 0.18/0.39 (~oneof(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[379, 2])).
% 0.18/0.39 tff(381,assumption,(~neither(cole)), introduced(assumption)).
% 0.18/0.39 tff(382,plain,
% 0.18/0.39 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(cole) | both(cole) | neither(cole))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(cole) | both(cole) | neither(cole))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(383,plain,
% 0.18/0.39 ((both(cole) | oneof(cole) | neither(cole)) <=> (oneof(cole) | both(cole) | neither(cole))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(384,plain,
% 0.18/0.39 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(cole) | oneof(cole) | neither(cole))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (oneof(cole) | both(cole) | neither(cole)))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[383])).
% 0.18/0.39 tff(385,plain,
% 0.18/0.39 (((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(cole) | oneof(cole) | neither(cole))) <=> ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(cole) | both(cole) | neither(cole))),
% 0.18/0.39 inference(transitivity,[status(thm)],[384, 382])).
% 0.18/0.39 tff(386,plain,
% 0.18/0.39 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | (both(cole) | oneof(cole) | neither(cole))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(387,plain,
% 0.18/0.39 ((~![X: $i] : (both(X) | oneof(X) | neither(X))) | oneof(cole) | both(cole) | neither(cole)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[386, 385])).
% 0.18/0.39 tff(388,plain,
% 0.18/0.39 (oneof(cole) | both(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[387, 23, 381])).
% 0.18/0.39 tff(389,plain,
% 0.18/0.39 (both(cole)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[388, 380])).
% 0.18/0.39 tff(390,plain,
% 0.18/0.39 ((salt(dix) | (~both(cole))) <=> (salt(dix) | (~both(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(391,plain,
% 0.18/0.39 (((~both(cole)) | salt(dix)) <=> (salt(dix) | (~both(cole)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(392,axiom,((~both(cole)) | salt(dix)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule5_3')).
% 0.18/0.39 tff(393,plain,
% 0.18/0.39 (salt(dix) | (~both(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[392, 391])).
% 0.18/0.39 tff(394,plain,
% 0.18/0.39 (salt(dix) | (~both(cole))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[393, 390])).
% 0.18/0.39 tff(395,plain,
% 0.18/0.39 (salt(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[394, 389])).
% 0.18/0.39 tff(396,plain,
% 0.18/0.39 (((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(dix)) | (~salt(dix)))) <=> ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(dix)) | (~salt(dix)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(397,plain,
% 0.18/0.39 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | ((~neither(dix)) | (~salt(dix)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(398,plain,
% 0.18/0.39 ((~![X: $i] : ((~neither(X)) | (~salt(X)))) | (~neither(dix)) | (~salt(dix))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[397, 396])).
% 0.18/0.39 tff(399,plain,
% 0.18/0.39 (~neither(dix)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[398, 38, 395])).
% 0.18/0.39 tff(400,assumption,(~both(lang)), introduced(assumption)).
% 0.18/0.39 tff(401,plain,
% 0.18/0.39 (((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | (salt(mill) | mustard(mill) | (~oneof(mill)))) <=> ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | salt(mill) | mustard(mill) | (~oneof(mill)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(402,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | (salt(mill) | mustard(mill) | (~oneof(mill)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(403,plain,
% 0.18/0.39 ((~![X: $i] : (salt(X) | mustard(X) | (~oneof(X)))) | salt(mill) | mustard(mill) | (~oneof(mill))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[402, 401])).
% 0.18/0.39 tff(404,plain,
% 0.18/0.39 (salt(mill) | mustard(mill)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[403, 202, 350])).
% 0.18/0.39 tff(405,plain,
% 0.18/0.39 (salt(mill)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[404, 2])).
% 0.18/0.39 tff(406,plain,
% 0.18/0.39 ((both(lang) | (~salt(mill)) | both(barry)) <=> (both(lang) | (~salt(mill)) | both(barry))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(407,plain,
% 0.18/0.40 ((((~salt(mill)) | both(barry)) | both(lang)) <=> (both(lang) | (~salt(mill)) | both(barry))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(408,plain,
% 0.18/0.40 (((~salt(mill)) | both(barry)) <=> ((~salt(mill)) | both(barry))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(409,plain,
% 0.18/0.40 ((((~salt(mill)) | both(barry)) | both(lang)) <=> (((~salt(mill)) | both(barry)) | both(lang))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[408])).
% 0.18/0.40 tff(410,plain,
% 0.18/0.40 ((((~salt(mill)) | both(barry)) | both(lang)) <=> (both(lang) | (~salt(mill)) | both(barry))),
% 0.18/0.40 inference(transitivity,[status(thm)],[409, 407])).
% 0.18/0.40 tff(411,axiom,(((~salt(mill)) | both(barry)) | both(lang)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule9_1')).
% 0.18/0.40 tff(412,plain,
% 0.18/0.40 (both(lang) | (~salt(mill)) | both(barry)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[411, 410])).
% 0.18/0.40 tff(413,plain,
% 0.18/0.40 (both(lang) | (~salt(mill)) | both(barry)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[412, 406])).
% 0.18/0.40 tff(414,plain,
% 0.18/0.40 (both(lang) | (~salt(mill)) | both(barry)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[413, 406])).
% 0.18/0.40 tff(415,plain,
% 0.18/0.40 (both(lang) | (~salt(mill)) | both(barry)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[414, 406])).
% 0.18/0.40 tff(416,plain,
% 0.18/0.40 (both(lang) | (~salt(mill)) | both(barry)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[415, 406])).
% 0.18/0.40 tff(417,plain,
% 0.18/0.40 (both(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[416, 405, 400])).
% 0.18/0.40 tff(418,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | (mustard(barry) | (~both(barry)))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(barry) | (~both(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(419,plain,
% 0.18/0.40 (((~both(barry)) | mustard(barry)) <=> (mustard(barry) | (~both(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(420,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(barry)) | mustard(barry))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | (mustard(barry) | (~both(barry))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[419])).
% 0.18/0.40 tff(421,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(barry)) | mustard(barry))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(barry) | (~both(barry)))),
% 0.18/0.40 inference(transitivity,[status(thm)],[420, 418])).
% 0.18/0.40 tff(422,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(barry)) | mustard(barry))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(423,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(barry) | (~both(barry))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[422, 421])).
% 0.18/0.40 tff(424,plain,
% 0.18/0.40 (mustard(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[423, 9, 417])).
% 0.18/0.40 tff(425,plain,
% 0.18/0.40 (((~mustard(barry)) | neither(dix) | both(mill)) <=> ((~mustard(barry)) | neither(dix) | both(mill))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(426,plain,
% 0.18/0.40 ((((~mustard(barry)) | neither(dix)) | both(mill)) <=> ((~mustard(barry)) | neither(dix) | both(mill))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(427,plain,
% 0.18/0.40 (((~mustard(barry)) | neither(dix)) <=> ((~mustard(barry)) | neither(dix))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(428,plain,
% 0.18/0.40 ((((~mustard(barry)) | neither(dix)) | both(mill)) <=> (((~mustard(barry)) | neither(dix)) | both(mill))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[427])).
% 0.18/0.40 tff(429,plain,
% 0.18/0.40 ((((~mustard(barry)) | neither(dix)) | both(mill)) <=> ((~mustard(barry)) | neither(dix) | both(mill))),
% 0.18/0.40 inference(transitivity,[status(thm)],[428, 426])).
% 0.18/0.40 tff(430,axiom,(((~mustard(barry)) | neither(dix)) | both(mill)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule2_1')).
% 0.18/0.40 tff(431,plain,
% 0.18/0.40 ((~mustard(barry)) | neither(dix) | both(mill)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[430, 429])).
% 0.18/0.40 tff(432,plain,
% 0.18/0.40 ((~mustard(barry)) | neither(dix) | both(mill)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[431, 425])).
% 0.18/0.40 tff(433,plain,
% 0.18/0.40 ((~mustard(barry)) | neither(dix) | both(mill)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[432, 425])).
% 0.18/0.40 tff(434,plain,
% 0.18/0.40 ((~mustard(barry)) | neither(dix) | both(mill)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[433, 425])).
% 0.18/0.40 tff(435,plain,
% 0.18/0.40 ((~mustard(barry)) | neither(dix) | both(mill)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[434, 425])).
% 0.18/0.40 tff(436,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[435, 424, 399, 372])).
% 0.18/0.40 tff(437,plain,(mustard(mill) | both(lang) | neither(cole)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(438,plain,
% 0.18/0.40 (mustard(mill)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[437, 358, 301])).
% 0.18/0.40 tff(439,assumption,(~salt(dix)), introduced(assumption)).
% 0.18/0.40 tff(440,plain,
% 0.18/0.40 ((salt(dix) | (~neither(barry))) <=> (salt(dix) | (~neither(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(441,plain,
% 0.18/0.40 (((~neither(barry)) | salt(dix)) <=> (salt(dix) | (~neither(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(442,axiom,((~neither(barry)) | salt(dix)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule5_2')).
% 0.18/0.40 tff(443,plain,
% 0.18/0.40 (salt(dix) | (~neither(barry))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[442, 441])).
% 0.18/0.40 tff(444,plain,
% 0.18/0.40 (salt(dix) | (~neither(barry))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[443, 440])).
% 0.18/0.40 tff(445,plain,
% 0.18/0.40 (~neither(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[444, 439])).
% 0.18/0.40 tff(446,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(mill)) | (~mustard(mill)) | (~oneof(mill)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(mill)) | (~mustard(mill)) | (~oneof(mill)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(447,plain,
% 0.18/0.40 (((~mustard(mill)) | (~salt(mill)) | (~oneof(mill))) <=> ((~salt(mill)) | (~mustard(mill)) | (~oneof(mill)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(448,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(mill)) | (~salt(mill)) | (~oneof(mill)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(mill)) | (~mustard(mill)) | (~oneof(mill))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[447])).
% 0.18/0.40 tff(449,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(mill)) | (~salt(mill)) | (~oneof(mill)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(mill)) | (~mustard(mill)) | (~oneof(mill)))),
% 0.18/0.40 inference(transitivity,[status(thm)],[448, 446])).
% 0.18/0.40 tff(450,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(mill)) | (~salt(mill)) | (~oneof(mill)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(451,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(mill)) | (~mustard(mill)) | (~oneof(mill))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[450, 449])).
% 0.18/0.40 tff(452,plain,
% 0.18/0.40 ((~salt(mill)) | (~mustard(mill))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[451, 254, 350])).
% 0.18/0.40 tff(453,plain,
% 0.18/0.40 (~salt(mill)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[452, 145])).
% 0.18/0.40 tff(454,plain,
% 0.18/0.40 (~both(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[47, 453])).
% 0.18/0.40 tff(455,plain,
% 0.18/0.40 (oneof(barry) | neither(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[93, 23, 454])).
% 0.18/0.40 tff(456,plain,
% 0.18/0.40 (oneof(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[455, 445])).
% 0.18/0.40 tff(457,plain,
% 0.18/0.40 (salt(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[86, 456])).
% 0.18/0.40 tff(458,plain,
% 0.18/0.40 (~neither(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[171, 38, 457])).
% 0.18/0.40 tff(459,plain,
% 0.18/0.40 (salt(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[243, 445, 145])).
% 0.18/0.40 tff(460,plain,
% 0.18/0.40 (((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | (both(barry) | (~mustard(barry)) | (~salt(barry)))) <=> ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | both(barry) | (~mustard(barry)) | (~salt(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(461,plain,
% 0.18/0.40 ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | (both(barry) | (~mustard(barry)) | (~salt(barry)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(462,plain,
% 0.18/0.40 ((~![X: $i] : (both(X) | (~mustard(X)) | (~salt(X)))) | both(barry) | (~mustard(barry)) | (~salt(barry))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[461, 460])).
% 0.18/0.40 tff(463,plain,
% 0.18/0.40 ((~mustard(barry)) | (~salt(barry))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[462, 74, 454])).
% 0.18/0.40 tff(464,plain,
% 0.18/0.40 (~mustard(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[463, 459])).
% 0.18/0.40 tff(465,plain,
% 0.18/0.40 ((mustard(barry) | (~neither(dix))) <=> (mustard(barry) | (~neither(dix)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(466,plain,
% 0.18/0.40 (((~neither(dix)) | mustard(barry)) <=> (mustard(barry) | (~neither(dix)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(467,axiom,((~neither(dix)) | mustard(barry)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule2_2')).
% 0.18/0.40 tff(468,plain,
% 0.18/0.40 (mustard(barry) | (~neither(dix))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[467, 466])).
% 0.18/0.40 tff(469,plain,
% 0.18/0.40 (mustard(barry) | (~neither(dix))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[468, 465])).
% 0.18/0.40 tff(470,plain,
% 0.18/0.40 (~neither(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[469, 464])).
% 0.18/0.40 tff(471,plain,
% 0.18/0.40 (((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (neither(dix) | salt(dix) | mustard(dix))) <=> ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | neither(dix) | salt(dix) | mustard(dix))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(472,plain,
% 0.18/0.40 ((salt(dix) | mustard(dix) | neither(dix)) <=> (neither(dix) | salt(dix) | mustard(dix))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(473,plain,
% 0.18/0.40 (((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (salt(dix) | mustard(dix) | neither(dix))) <=> ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (neither(dix) | salt(dix) | mustard(dix)))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[472])).
% 0.18/0.40 tff(474,plain,
% 0.18/0.40 (((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (salt(dix) | mustard(dix) | neither(dix))) <=> ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | neither(dix) | salt(dix) | mustard(dix))),
% 0.18/0.40 inference(transitivity,[status(thm)],[473, 471])).
% 0.18/0.40 tff(475,plain,
% 0.18/0.40 ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | (salt(dix) | mustard(dix) | neither(dix))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(476,plain,
% 0.18/0.40 ((~![X: $i] : (salt(X) | mustard(X) | neither(X))) | neither(dix) | salt(dix) | mustard(dix)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[475, 474])).
% 0.18/0.40 tff(477,plain,
% 0.18/0.40 (mustard(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[476, 312, 470, 439])).
% 0.18/0.40 tff(478,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[191, 477, 458, 357])).
% 0.18/0.40 tff(479,plain,(salt(dix) | (~mustard(mill))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(480,plain,
% 0.18/0.40 (salt(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[479, 438])).
% 0.18/0.40 tff(481,assumption,(salt(dix)), introduced(assumption)).
% 0.18/0.40 tff(482,assumption,(~neither(lang)), introduced(assumption)).
% 0.18/0.40 tff(483,plain,
% 0.18/0.40 (oneof(lang) | neither(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[115, 23, 400])).
% 0.18/0.40 tff(484,plain,
% 0.18/0.40 (oneof(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[483, 482])).
% 0.18/0.40 tff(485,plain,
% 0.18/0.40 (salt(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[122, 484])).
% 0.18/0.40 tff(486,plain,
% 0.18/0.40 (~neither(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[126, 38, 485])).
% 0.18/0.40 tff(487,plain,
% 0.18/0.40 (both(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[218, 486, 481])).
% 0.18/0.40 tff(488,plain,
% 0.18/0.40 (~mustard(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[191, 482, 357])).
% 0.18/0.40 tff(489,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(dix)) | mustard(dix))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(dix)) | mustard(dix))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(490,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(dix)) | mustard(dix))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(491,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | (~both(dix)) | mustard(dix)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[490, 489])).
% 0.18/0.40 tff(492,plain,
% 0.18/0.40 (~both(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[491, 9, 488])).
% 0.18/0.40 tff(493,plain,
% 0.18/0.40 (~mustard(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[328, 492, 400])).
% 0.18/0.40 tff(494,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | (mustard(cole) | (~both(cole)))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(cole) | (~both(cole)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(495,plain,
% 0.18/0.40 (((~both(cole)) | mustard(cole)) <=> (mustard(cole) | (~both(cole)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(496,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(cole)) | mustard(cole))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | (mustard(cole) | (~both(cole))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[495])).
% 0.18/0.40 tff(497,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(cole)) | mustard(cole))) <=> ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(cole) | (~both(cole)))),
% 0.18/0.40 inference(transitivity,[status(thm)],[496, 494])).
% 0.18/0.40 tff(498,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | ((~both(cole)) | mustard(cole))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(499,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | mustard(X))) | mustard(cole) | (~both(cole))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[498, 497])).
% 0.18/0.40 tff(500,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[499, 9, 493, 487])).
% 0.18/0.40 tff(501,plain,(neither(lang) | both(lang) | (~salt(dix))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(502,plain,
% 0.18/0.40 (neither(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[501, 358, 480])).
% 0.18/0.40 tff(503,plain,
% 0.18/0.40 ((mustard(dix) | (~neither(lang))) <=> (mustard(dix) | (~neither(lang)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(504,plain,
% 0.18/0.40 (((~neither(lang)) | mustard(dix)) <=> (mustard(dix) | (~neither(lang)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(505,axiom,((~neither(lang)) | mustard(dix)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule6_2')).
% 0.18/0.40 tff(506,plain,
% 0.18/0.40 (mustard(dix) | (~neither(lang))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[505, 504])).
% 0.18/0.40 tff(507,plain,
% 0.18/0.40 (mustard(dix) | (~neither(lang))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[506, 503])).
% 0.18/0.40 tff(508,plain,
% 0.18/0.40 (mustard(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[507, 502])).
% 0.18/0.40 tff(509,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(dix)) | (~mustard(dix)) | (~oneof(dix)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(dix)) | (~mustard(dix)) | (~oneof(dix)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(510,plain,
% 0.18/0.40 (((~mustard(dix)) | (~salt(dix)) | (~oneof(dix))) <=> ((~salt(dix)) | (~mustard(dix)) | (~oneof(dix)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(511,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(dix)) | (~salt(dix)) | (~oneof(dix)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~salt(dix)) | (~mustard(dix)) | (~oneof(dix))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[510])).
% 0.18/0.40 tff(512,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(dix)) | (~salt(dix)) | (~oneof(dix)))) <=> ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(dix)) | (~mustard(dix)) | (~oneof(dix)))),
% 0.18/0.40 inference(transitivity,[status(thm)],[511, 509])).
% 0.18/0.40 tff(513,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | ((~mustard(dix)) | (~salt(dix)) | (~oneof(dix)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(514,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~salt(X)) | (~oneof(X)))) | (~salt(dix)) | (~mustard(dix)) | (~oneof(dix))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[513, 512])).
% 0.18/0.40 tff(515,plain,
% 0.18/0.40 ((~mustard(dix)) | (~oneof(dix))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[514, 254, 480])).
% 0.18/0.40 tff(516,plain,
% 0.18/0.40 (~oneof(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[515, 508])).
% 0.18/0.40 tff(517,plain,
% 0.18/0.40 (oneof(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[161, 516, 438])).
% 0.18/0.40 tff(518,plain,
% 0.18/0.40 (((~![X: $i] : ((~both(X)) | (~oneof(X)))) | ((~both(cole)) | (~oneof(cole)))) <=> ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | (~both(cole)) | (~oneof(cole)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(519,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | ((~both(cole)) | (~oneof(cole)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(520,plain,
% 0.18/0.40 ((~![X: $i] : ((~both(X)) | (~oneof(X)))) | (~both(cole)) | (~oneof(cole))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[519, 518])).
% 0.18/0.40 tff(521,plain,
% 0.18/0.40 (~both(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[520, 368, 517])).
% 0.18/0.40 tff(522,plain,
% 0.18/0.40 (salt(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[152, 517])).
% 0.18/0.40 tff(523,plain,
% 0.18/0.40 (~neither(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[126, 38, 522])).
% 0.18/0.40 tff(524,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[218, 523, 521, 480])).
% 0.18/0.40 tff(525,plain,(mustard(lang)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(526,plain,
% 0.18/0.40 (neither(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[241, 525, 357])).
% 0.18/0.40 tff(527,plain,
% 0.18/0.40 (((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(cole)) | (~neither(cole)))) <=> ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(cole)) | (~neither(cole)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(528,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | ((~mustard(cole)) | (~neither(cole)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(529,plain,
% 0.18/0.40 ((~![X: $i] : ((~mustard(X)) | (~neither(X)))) | (~mustard(cole)) | (~neither(cole))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[528, 527])).
% 0.18/0.40 tff(530,plain,
% 0.18/0.40 (~mustard(cole)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[529, 105, 526])).
% 0.18/0.40 tff(531,plain,
% 0.18/0.40 ((mustard(cole) | (~both(lang))) <=> (mustard(cole) | (~both(lang)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(532,plain,
% 0.18/0.40 (((~both(lang)) | mustard(cole)) <=> (mustard(cole) | (~both(lang)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(533,axiom,((~both(lang)) | mustard(cole)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rule4_3')).
% 0.18/0.40 tff(534,plain,
% 0.18/0.40 (mustard(cole) | (~both(lang))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[533, 532])).
% 0.18/0.40 tff(535,plain,
% 0.18/0.40 (mustard(cole) | (~both(lang))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[534, 531])).
% 0.18/0.40 tff(536,plain,
% 0.18/0.40 (~both(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[535, 530])).
% 0.18/0.40 tff(537,plain,
% 0.18/0.40 (~neither(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[108, 105, 525])).
% 0.18/0.40 tff(538,plain,
% 0.18/0.40 (~salt(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[501, 536, 537])).
% 0.18/0.40 tff(539,plain,
% 0.18/0.40 (~mustard(mill)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[479, 538])).
% 0.18/0.40 tff(540,plain,
% 0.18/0.40 (salt(mill)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[404, 539])).
% 0.18/0.40 tff(541,plain,
% 0.18/0.40 (both(barry)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[416, 540, 536])).
% 0.18/0.40 tff(542,plain,
% 0.18/0.40 (oneof(lang)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[115, 23, 536, 537])).
% 0.18/0.40 tff(543,plain,
% 0.18/0.40 (~mustard(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[191, 537, 357])).
% 0.18/0.40 tff(544,plain,
% 0.18/0.40 (neither(dix)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[476, 312, 538, 543])).
% 0.18/0.40 tff(545,plain,
% 0.18/0.40 (((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))) <=> ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(546,plain,
% 0.18/0.40 ((((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry))) | (~oneof(mill))) <=> ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(547,plain,
% 0.18/0.40 ((((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~salt(mill)) | (~both(barry))) | (~mustard(lang))) <=> ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(548,plain,
% 0.18/0.40 ((((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~both(barry))) | (~salt(mill))) <=> ((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(549,plain,
% 0.18/0.40 ((((~neither(dix)) | (~neither(cole)) | (~both(barry))) | (~oneof(lang))) <=> ((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~both(barry)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(550,plain,
% 0.18/0.41 ((((~neither(cole)) | (~neither(dix))) | (~both(barry))) <=> ((~neither(dix)) | (~neither(cole)) | (~both(barry)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(551,plain,
% 0.18/0.41 (((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) <=> (((~neither(dix)) | (~neither(cole)) | (~both(barry))) | (~oneof(lang)))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[550])).
% 0.18/0.41 tff(552,plain,
% 0.18/0.41 (((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) <=> ((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~both(barry)))),
% 0.18/0.41 inference(transitivity,[status(thm)],[551, 549])).
% 0.18/0.41 tff(553,plain,
% 0.18/0.41 ((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) <=> (((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~both(barry))) | (~salt(mill)))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[552])).
% 0.18/0.41 tff(554,plain,
% 0.18/0.41 ((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) <=> ((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)))),
% 0.18/0.41 inference(transitivity,[status(thm)],[553, 548])).
% 0.18/0.41 tff(555,plain,
% 0.18/0.41 (((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) | (~mustard(lang))) <=> (((~oneof(lang)) | (~neither(dix)) | (~neither(cole)) | (~salt(mill)) | (~both(barry))) | (~mustard(lang)))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[554])).
% 0.18/0.41 tff(556,plain,
% 0.18/0.41 (((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) | (~mustard(lang))) <=> ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)))),
% 0.18/0.41 inference(transitivity,[status(thm)],[555, 547])).
% 0.18/0.41 tff(557,plain,
% 0.18/0.41 ((((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) | (~mustard(lang))) | (~oneof(mill))) <=> (((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry))) | (~oneof(mill)))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[556])).
% 0.18/0.41 tff(558,plain,
% 0.18/0.41 ((((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) | (~mustard(lang))) | (~oneof(mill))) <=> ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill)))),
% 0.18/0.41 inference(transitivity,[status(thm)],[557, 546])).
% 0.18/0.41 tff(559,axiom,(((((((~neither(cole)) | (~neither(dix))) | (~both(barry))) | (~oneof(lang))) | (~salt(mill))) | (~mustard(lang))) | (~oneof(mill))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_who_takes_what')).
% 0.18/0.41 tff(560,plain,
% 0.18/0.41 ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[559, 558])).
% 0.18/0.41 tff(561,plain,
% 0.18/0.41 ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[560, 545])).
% 0.18/0.41 tff(562,plain,
% 0.18/0.41 ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[561, 545])).
% 0.18/0.41 tff(563,plain,
% 0.18/0.41 ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[562, 545])).
% 0.18/0.41 tff(564,plain,
% 0.18/0.41 ((~oneof(lang)) | (~neither(dix)) | (~mustard(lang)) | (~neither(cole)) | (~salt(mill)) | (~both(barry)) | (~oneof(mill))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[563, 545])).
% 0.18/0.41 tff(565,plain,
% 0.18/0.41 ($false),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[564, 544, 542, 525, 526, 540, 541, 350])).
% 0.18/0.41 % SZS output end Proof
% 0.18/0.41 % E exiting
%------------------------------------------------------------------------------