# Entrants' Sample Solutions

## CVC4 1.2

Andrew Reynolds
University of Iowa, USA

### Sample solution for NLP042+1

% SZS CounterSatisfiable for NLP042+1
% SZS output start FiniteModel for NLP042+1
(model
(define-fun woman_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2)) false (ite (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2)) false (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2)))))) (define-fun female_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)) false (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)) false (not (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2))))))
(define-fun human_person_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2)) false (ite (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2)) false (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2)))))) (define-fun animate_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)) false (not (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)))))
(define-fun human_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2)))) (define-fun organism_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)) false (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)) false (not (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2))))))
(define-fun living_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2)))) (define-fun impartial_2 ((BOUND_VARIABLE_2482 $$unsorted) (BOUND_VARIABLE_2483$$unsorted)) Bool false) (define-fun entity_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)) false (not (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)))))
(define-fun mia_forename_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2))) (define-fun forename_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)))
(define-fun abstraction_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2))) (define-fun unisex_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)) true (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)) true (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)))))
(define-fun general_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2))) (define-fun nonhuman_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)))
(define-fun thing_2 ((BOUND_VARIABLE_2486 $$unsorted) (BOUND_VARIABLE_2487$$unsorted)) Bool false)
(define-fun relation_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_1 $x2))) (define-fun relname_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2)))
(define-fun object_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2))) (define-fun nonliving_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)))
(define-fun existent_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2)))) (define-fun specific_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (not (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_1$x2))))
(define-fun substance_matter_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2))) (define-fun food_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)))
(define-fun beverage_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_2 $x2))) (define-fun shake_beverage_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_2$x2)))
(define-fun order_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2))) (define-fun event_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)))
(define-fun eventuality_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2))) (define-fun nonexistent_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2)))
(define-fun singleton_2 ((BOUND_VARIABLE_2490 $$unsorted) (BOUND_VARIABLE_2491$$unsorted)) Bool false)
(define-fun act_2 (($x1 $$unsorted) (x2$$unsorted)) Bool (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2))) (define-fun of_3 (($x1 $$unsorted) (x2$$unsorted) ($x3 $$unsorted)) Bool true) (define-fun nonreflexive_2 ((x1$$unsorted) ($x2 $$unsorted)) Bool (and (= @uc___unsorted_0 x1) (= @uc___unsorted_3 x2))) (define-fun agent_3 ((x1$$unsorted) ($x2 $$unsorted) (x3$$unsorted)) Bool (ite (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2) (= @uc___unsorted_2$x3)) false (ite (and (= @uc___unsorted_0 $x1) (= @uc___unsorted_3$x2) (= @uc___unsorted_3 $x3)) false (not (and (= @uc___unsorted_0$x1) (= @uc___unsorted_3 $x2) (= @uc___unsorted_1$x3))))))
(define-fun patient_3 (($x1 $$unsorted) (x2$$unsorted) ($x3 $$unsorted)) Bool (not (and (= @uc___unsorted_0 x1) (= @uc___unsorted_3 x2) (= @uc___unsorted_0 x3)))) (define-fun actual_world_1 ((x1$$unsorted)) Bool true)
(define-fun past_2 (($x1 $$unsorted) (x2$$unsorted)) Bool true) ; cardinality of $$unsorted is 4 (declare-sort$$unsorted 0) ; rep: @uc___unsorted_0 ; rep: @uc___unsorted_1 ; rep: @uc___unsorted_2 ; rep: @uc___unsorted_3 ) % SZS output end FiniteModel for NLP042+1  ### Sample solution for SWV017+1 % SZS Satisfiable for SWV017+1 % SZS output start FiniteModel for SWV017+1 (model (define-fun at_0 () $$unsorted @uc___unsorted_0) (define-fun t_0 ()$$unsorted @uc___unsorted_0) (define-fun key_2 (($x1 $$unsorted) (x2$$unsorted)) $$unsorted @uc___unsorted_0) (define-fun a_holds_1 ((x1$$unsorted)) Bool true)
(define-fun a_0 () $$unsorted @uc___unsorted_0) (define-fun party_of_protocol_1 ((x1$$unsorted)) Bool true)
(define-fun b_0 () $$unsorted @uc___unsorted_0) (define-fun an_a_nonce_0 ()$$unsorted @uc___unsorted_0)
(define-fun pair_2 (($x1 $$unsorted) (x2$$unsorted)) $$unsorted @uc___unsorted_0) (define-fun sent_3 ((x1$$unsorted) ($x2 $$unsorted) (x3$$unsorted)) $$unsorted @uc___unsorted_0) (define-fun message_1 ((x1$$unsorted)) Bool true)
(define-fun a_stored_1 (($x1 $$unsorted)) Bool true) (define-fun quadruple_4 ((BOUND_VARIABLE_967$$unsorted) (BOUND_VARIABLE_968 $$unsorted) (BOUND_VARIABLE_969$$unsorted) (BOUND_VARIABLE_970 $$unsorted))$$unsorted @uc___unsorted_0) (define-fun encrypt_2 ((BOUND_VARIABLE_973 $$unsorted) (BOUND_VARIABLE_974$$unsorted)) $$unsorted @uc___unsorted_0) (define-fun triple_3 ((BOUND_VARIABLE_977$$unsorted) (BOUND_VARIABLE_978 $$unsorted) (BOUND_VARIABLE_979$$unsorted)) $$unsorted @uc___unsorted_0) (define-fun bt_0 ()$$unsorted @uc___unsorted_0) (define-fun b_holds_1 (($x1 $$unsorted)) Bool true) (define-fun fresh_to_b_1 ((x1$$unsorted)) Bool true)
(define-fun generate_b_nonce_1 ((BOUND_VARIABLE_982 $$unsorted))$$unsorted @uc___unsorted_0)
(define-fun generate_expiration_time_1 ((BOUND_VARIABLE_985 $$unsorted))$$unsorted @uc___unsorted_0)
(define-fun b_stored_1 ((BOUND_VARIABLE_988 $$unsorted)) Bool false) (define-fun a_key_1 ((x1$$unsorted)) Bool (= @uc___unsorted_1 $x1)) (define-fun t_holds_1 (($x1 $$unsorted)) Bool true) (define-fun a_nonce_1 ((x1$$unsorted)) Bool (not (= @uc___unsorted_1 $x1))) (define-fun generate_key_1 (($x1 $$unsorted))$$unsorted @uc___unsorted_1)
(define-fun intruder_message_1 ((BOUND_VARIABLE_991 $$unsorted)) Bool false) (define-fun intruder_holds_1 ((BOUND_VARIABLE_994$$unsorted)) Bool false)
(define-fun an_intruder_nonce_0 () $$unsorted @uc___unsorted_0) (define-fun fresh_intruder_nonce_1 ((x1$$unsorted)) Bool true)
(define-fun generate_intruder_nonce_1 ((BOUND_VARIABLE_997 $$unsorted))$$unsorted @uc___unsorted_0)
; cardinality of $$unsorted is 2 (declare-sort$$unsorted 0)
; rep: @uc___unsorted_0
; rep: @uc___unsorted_1
)
% SZS output end FiniteModel for SWV017+1


## E 1.8

Stephan Schulz
Technische Universität München, Germany

### Sample solution for SEU140+2

# SZS status Theorem
# SZS output start CNFRefutation.
fof(c_0_0, lemma, (![X1]:![X2]:(~((~(disjoint(X1,X2))&![X3]:~((in(X3,X1)&in(X3,X2)))))&~((?[X3]:(in(X3,X1)&in(X3,X2))&disjoint(X1,X2))))), file('/tmp/SystemOnTPTP1613/SEU140+2.tptp', t3_xboole_0)).
fof(c_0_1, conjecture, (![X1]:![X2]:![X3]:((subset(X1,X2)&disjoint(X2,X3))=>disjoint(X1,X3))), file('/tmp/SystemOnTPTP1613/SEU140+2.tptp', t63_xboole_1)).
fof(c_0_2, axiom, (![X1]:![X2]:(subset(X1,X2)<=>![X3]:(in(X3,X1)=>in(X3,X2)))), file('/tmp/SystemOnTPTP1613/SEU140+2.tptp', d3_tarski)).
fof(c_0_3, axiom, (![X1]:![X2]:(disjoint(X1,X2)=>disjoint(X2,X1))), file('/tmp/SystemOnTPTP1613/SEU140+2.tptp', symmetry_r1_xboole_0)).
fof(c_0_4, lemma, (![X1]:![X2]:(~((~disjoint(X1,X2)&![X3]:~((in(X3,X1)&in(X3,X2)))))&~((?[X3]:(in(X3,X1)&in(X3,X2))&disjoint(X1,X2))))), inference(fof_simplification,[status(thm)],[c_0_0])).
fof(c_0_5, negated_conjecture, (~(![X1]:![X2]:![X3]:((subset(X1,X2)&disjoint(X2,X3))=>disjoint(X1,X3)))), inference(assume_negation,[status(cth)],[c_0_1])).
fof(c_0_6, lemma, (![X4]:![X5]:![X7]:![X8]:![X9]:(((in(esk9_2(X4,X5),X4)|disjoint(X4,X5))&(in(esk9_2(X4,X5),X5)|disjoint(X4,X5)))&((~in(X9,X7)|~in(X9,X8))|~disjoint(X7,X8)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])])).
fof(c_0_7, negated_conjecture, (((subset(esk11_0,esk12_0)&disjoint(esk12_0,esk13_0))&~disjoint(esk11_0,esk13_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])).
fof(c_0_8, axiom, (![X1]:![X2]:(subset(X1,X2)<=>![X3]:(in(X3,X1)=>in(X3,X2)))), c_0_2).
cnf(c_0_9,lemma,(~disjoint(X1,X2)|~in(X3,X2)|~in(X3,X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
cnf(c_0_10,negated_conjecture,(disjoint(esk12_0,esk13_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
fof(c_0_11, plain, (![X4]:![X5]:![X6]:![X7]:![X8]:((~subset(X4,X5)|(~in(X6,X4)|in(X6,X5)))&((in(esk3_2(X7,X8),X7)|subset(X7,X8))&(~in(esk3_2(X7,X8),X8)|subset(X7,X8))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])])])).
fof(c_0_12, axiom, (![X1]:![X2]:(disjoint(X1,X2)=>disjoint(X2,X1))), c_0_3).
cnf(c_0_13,lemma,(~in(X3,X2)|~in(X3,X1)|~disjoint(X1,X2)), c_0_9).
cnf(c_0_14,negated_conjecture,(disjoint(esk12_0,esk13_0)), c_0_10).
cnf(c_0_15,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
cnf(c_0_16,plain,(in(X1,X2)|~in(X1,X3)|~subset(X3,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
cnf(c_0_17,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), inference(split_conjunct,[status(thm)],[c_0_6])).
fof(c_0_18, plain, (![X3]:![X4]:(~disjoint(X3,X4)|disjoint(X4,X3))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])).
cnf(c_0_19,lemma,(~disjoint(X1,X2)|~in(X3,X2)|~in(X3,X1)), c_0_13).
cnf(c_0_20,negated_conjecture,(disjoint(esk12_0,esk13_0)), c_0_14).
cnf(c_0_21,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), c_0_15).
cnf(c_0_22,plain,(in(X1,X2)|~in(X1,X3)|~subset(X3,X2)), c_0_16).
cnf(c_0_23,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), c_0_17).
cnf(c_0_24,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_18])).
cnf(c_0_25,lemma,(~disjoint(X1,X2)|~in(X3,X2)|~in(X3,X1)), c_0_19).
cnf(c_0_26,negated_conjecture,(disjoint(esk12_0,esk13_0)), c_0_20).
cnf(c_0_27,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), c_0_21).
cnf(c_0_28,plain,(in(X1,X2)|~subset(X3,X2)|~in(X1,X3)), c_0_22).
cnf(c_0_29,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), c_0_23).
cnf(c_0_30,negated_conjecture,(~disjoint(esk11_0,esk13_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
cnf(c_0_31,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), c_0_24).
cnf(c_0_32,negated_conjecture,(~in(X1,esk13_0)|~in(X1,esk12_0)), inference(spm,[status(thm)],[c_0_25, c_0_26, theory(equality)]])).
cnf(c_0_33,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), c_0_27).
cnf(c_0_34,plain,(in(X1,X2)|~subset(X3,X2)|~in(X1,X3)), c_0_28).
cnf(c_0_35,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), c_0_29).
cnf(c_0_36,negated_conjecture,(subset(esk11_0,esk12_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
cnf(c_0_37,negated_conjecture,(~disjoint(esk11_0,esk13_0)), c_0_30).
cnf(c_0_38,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), c_0_31).
cnf(c_0_39,negated_conjecture,(disjoint(esk13_0,X1)|~in(esk9_2(esk13_0,X1),esk12_0)), inference(spm,[status(thm)],[c_0_32, c_0_33, theory(equality)]])).
cnf(c_0_40,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X3)|~subset(X2,X3)), inference(spm,[status(thm)],[c_0_34, c_0_35, theory(equality)]])).
cnf(c_0_41,negated_conjecture,(subset(esk11_0,esk12_0)), c_0_36).
cnf(c_0_42,negated_conjecture,(~disjoint(esk11_0,esk13_0)), c_0_37).
cnf(c_0_43,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), c_0_38).
cnf(c_0_44,lemma,(disjoint(esk13_0,X1)|~subset(X1,esk12_0)), inference(spm,[status(thm)],[c_0_39, c_0_40, theory(equality)]])).
cnf(c_0_45,negated_conjecture,(subset(esk11_0,esk12_0)), c_0_41).
cnf(c_0_46,negated_conjecture,(~disjoint(esk11_0,esk13_0)), c_0_42).
cnf(c_0_47,lemma,(disjoint(X1,esk13_0)|~subset(X1,esk12_0)), inference(spm,[status(thm)],[c_0_43, c_0_44, theory(equality)]])).
cnf(c_0_48,negated_conjecture,(subset(esk11_0,esk12_0)), c_0_45).
cnf(1641,plain,($false),1640,['proof']). # SZS output end CNFRefutation  ## iProver 1.0 Konstantin Korovin, Christoph Sticksel University of Manchester, United Kingdom ### Sample solution for SEU140+2 % SZS output start CNFRefutation fof(f210,plain,( ~disjoint(sK10,sK12)), inference(cnf_transformation,[],[f134])). fof(f134,plain,( subset(sK10,sK11) & disjoint(sK11,sK12) & ~disjoint(sK10,sK12)), inference(skolemisation,[status(esa)],[f99])). fof(f99,plain,( ? [X0,X1,X2] : (subset(X0,X1) & disjoint(X1,X2) & ~disjoint(X0,X2))), inference(flattening,[],[f98])). fof(f98,plain,( ? [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) & ~disjoint(X0,X2))), inference(ennf_transformation,[],[f52])). fof(f52,negated_conjecture,( ~! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))), inference(negated_conjecture,[],[f51])). fof(f51,conjecture,( ! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))), file('/Users/korovin/TPTP-v5.4.0/Problems/SEU/SEU140+2.p',unknown)). fof(f209,plain,( disjoint(sK11,sK12)), inference(cnf_transformation,[],[f134])). fof(f208,plain,( subset(sK10,sK11)), inference(cnf_transformation,[],[f134])). fof(f198,plain,( ( ! [X0,X1] : (in(sK8(X1,X0),X1) | disjoint(X0,X1)) )), inference(cnf_transformation,[],[f132])). fof(f132,plain,( ! [X0,X1] : ((disjoint(X0,X1) | (in(sK8(X1,X0),X0) & in(sK8(X1,X0),X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))), inference(skolemisation,[status(esa)],[f93])). fof(f93,plain,( ! [X0,X1] : ((disjoint(X0,X1) | ? [X3] : (in(X3,X0) & in(X3,X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))), inference(ennf_transformation,[],[f71])). fof(f71,plain,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), inference(flattening,[],[f70])). fof(f70,plain,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), inference(rectify,[],[f43])). fof(f43,axiom,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X2] : ~(in(X2,X0) & in(X2,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SEU/SEU140+2.p',unknown)). fof(f197,plain,( ( ! [X0,X1] : (in(sK8(X1,X0),X0) | disjoint(X0,X1)) )), inference(cnf_transformation,[],[f132])). fof(f150,plain,( ( ! [X0,X3,X1] : (in(X3,X1) | ~in(X3,X0) | ~subset(X0,X1)) )), inference(cnf_transformation,[],[f116])). fof(f116,plain,( ! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & ((in(sK2(X1,X0),X0) & ~in(sK2(X1,X0),X1)) | subset(X0,X1)))), inference(skolemisation,[status(esa)],[f115])). fof(f115,plain,( ! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))), inference(rectify,[],[f114])). fof(f114,plain,( ! [X0,X1] : ((~subset(X0,X1) | ! [X2] : (~in(X2,X0) | in(X2,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))), inference(nnf_transformation,[],[f78])). fof(f78,plain,( ! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (~in(X2,X0) | in(X2,X1)))), inference(ennf_transformation,[],[f8])). fof(f8,axiom,( ! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (in(X2,X0) => in(X2,X1)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SEU/SEU140+2.p',unknown)). fof(f179,plain,( ( ! [X0,X1] : (disjoint(X1,X0) | ~disjoint(X0,X1)) )), inference(cnf_transformation,[],[f83])). fof(f83,plain,( ! [X0,X1] : (~disjoint(X0,X1) | disjoint(X1,X0))), inference(ennf_transformation,[],[f27])). fof(f27,axiom,( ! [X0,X1] : (disjoint(X0,X1) => disjoint(X1,X0))), file('/Users/korovin/TPTP-v5.4.0/Problems/SEU/SEU140+2.p',unknown)). fof(f199,plain,( ( ! [X2,X0,X1] : (~disjoint(X0,X1) | ~in(X2,X1) | ~in(X2,X0)) )), inference(cnf_transformation,[],[f132])). cnf(c_73,plain, ( ~ disjoint(sK10,sK12) ), inference(cnf_transformation,[],[f210]) ). cnf(c_83,plain, ( ~ disjoint(sK10,sK12) ), inference(subtyping,[status(esa)],[c_73]) ). cnf(c_74,plain, ( disjoint(sK11,sK12) ), inference(cnf_transformation,[],[f209]) ). cnf(c_82,plain, ( disjoint(sK11,sK12) ), inference(subtyping,[status(esa)],[c_74]) ). cnf(c_75,plain, ( subset(sK10,sK11) ), inference(cnf_transformation,[],[f208]) ). cnf(c_81,plain, ( subset(sK10,sK11) ), inference(subtyping,[status(esa)],[c_75]) ). cnf(c_63,plain, ( in(sK8(X0_$i,X1_$i),X0_$i) | disjoint(X1_$i,X0_$i) ),
inference(cnf_transformation,[],[f198]) ).

cnf(c_737,plain,
( in(sK8(X0_$i,X1_$i),X0_$i) | disjoint(X1_$i,X0_$i) ), inference(subtyping,[status(esa)],[c_63]) ). cnf(c_745,plain, ( in(sK8(sK12,sK10),sK12) | disjoint(sK10,sK12) ), inference(instantiation,[status(thm)],[c_737]) ). cnf(c_64,plain, ( in(sK8(X0_$i,X1_$i),X1_$i) | disjoint(X1_$i,X0_$i) ),
inference(cnf_transformation,[],[f197]) ).

cnf(c_738,plain,
( in(sK8(X0_$i,X1_$i),X1_$i) | disjoint(X1_$i,X0_$i) ), inference(subtyping,[status(esa)],[c_64]) ). cnf(c_746,plain, ( in(sK8(sK12,sK10),sK10) | disjoint(sK10,sK12) ), inference(instantiation,[status(thm)],[c_738]) ). cnf(c_17,plain, ( ~ in(X0_$i,X1_$i) | in(X0_$i,X2_$i) | ~ subset(X1_$i,X2_$i) ), inference(cnf_transformation,[],[f150]) ). cnf(c_664,plain, ( ~ in(X0_$i,X1_$i) | in(X0_$i,X2_$i) | ~ subset(X1_$i,X2_$i) ), inference(subtyping,[status(esa)],[c_17]) ). cnf(c_786,plain, ( ~ in(sK8(sK12,sK10),sK10) | in(sK8(sK12,sK10),X0_$i)
| ~ subset(sK10,X0_$i) ), inference(instantiation,[status(thm)],[c_664]) ). cnf(c_1093,plain, ( ~ in(sK8(sK12,sK10),sK10) | in(sK8(sK12,sK10),sK11) | ~ subset(sK10,sK11) ), inference(instantiation,[status(thm)],[c_786]) ). cnf(c_44,plain, ( ~ disjoint(X0_$i,X1_$i) | disjoint(X1_$i,X0_$i) ), inference(cnf_transformation,[],[f179]) ). cnf(c_735,plain, ( ~ disjoint(X0_$i,X1_$i) | disjoint(X1_$i,X0_$i) ), inference(subtyping,[status(esa)],[c_44]) ). cnf(c_1038,plain, ( disjoint(sK12,X0_$i) | ~ disjoint(X0_$i,sK12) ), inference(instantiation,[status(thm)],[c_735]) ). cnf(c_1888,plain, ( disjoint(sK12,sK11) | ~ disjoint(sK11,sK12) ), inference(instantiation,[status(thm)],[c_1038]) ). cnf(c_62,plain, ( ~ in(X0_$i,X1_$i) | ~ in(X0_$i,X2_$i) | ~ disjoint(X1_$i,X2_$i) ), inference(cnf_transformation,[],[f199]) ). cnf(c_736,plain, ( ~ in(X0_$i,X1_$i) | ~ in(X0_$i,X2_$i) | ~ disjoint(X1_$i,X2_$i) ), inference(subtyping,[status(esa)],[c_62]) ). cnf(c_775,plain, ( ~ in(sK8(sK12,sK10),sK12) | ~ in(sK8(sK12,sK10),X0_$i)
| ~ disjoint(sK12,X0_$i) ), inference(instantiation,[status(thm)],[c_736]) ). cnf(c_4288,plain, ( ~ in(sK8(sK12,sK10),sK12) | ~ in(sK8(sK12,sK10),sK11) | ~ disjoint(sK12,sK11) ), inference(instantiation,[status(thm)],[c_775]) ). cnf(contradiction,plain, ($false ),
inference(minisat,
[status(thm)],
[c_83,c_82,c_81,c_745,c_746,c_1093,c_1888,c_4288]) ).

% SZS output end CNFRefutation


### Sample solution for NLP042+1

% SZS output start Saturation

fof(f236,plain,(
( ! [Xxs0,X1] : (~general(X0,X1) | ~specific(X0,X1)) )),
inference(cnf_transformation,[],[f194])).

fof(f194,plain,(
! [X0,X1] : (~specific(X0,X1) | ~general(X0,X1))),
inference(ennf_transformation,[],[f51])).

fof(f51,plain,(
! [X0,X1] : (specific(X0,X1) => ~general(X0,X1))),
inference(flattening,[],[f41])).

fof(f41,axiom,(
! [X0,X1] : (specific(X0,X1) => ~general(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f219,plain,(
( ! [X0,X1] : (specific(X0,X1) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f177])).

fof(f177,plain,(
! [X0,X1] : (~entity(X0,X1) | specific(X0,X1))),
inference(ennf_transformation,[],[f21])).

fof(f21,axiom,(
! [X0,X1] : (entity(X0,X1) => specific(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f211,plain,(
( ! [X0,X1] : (general(X0,X1) | ~abstraction(X0,X1)) )),
inference(cnf_transformation,[],[f169])).

fof(f169,plain,(
! [X0,X1] : (~abstraction(X0,X1) | general(X0,X1))),
inference(ennf_transformation,[],[f11])).

fof(f11,axiom,(
! [X0,X1] : (abstraction(X0,X1) => general(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f213,plain,(
( ! [X0,X1] : (abstraction(X0,X1) | ~relation(X0,X1)) )),
inference(cnf_transformation,[],[f171])).

fof(f171,plain,(
! [X0,X1] : (~relation(X0,X1) | abstraction(X0,X1))),
inference(ennf_transformation,[],[f14])).

fof(f14,axiom,(
! [X0,X1] : (relation(X0,X1) => abstraction(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f214,plain,(
( ! [X0,X1] : (relation(X0,X1) | ~relname(X0,X1)) )),
inference(cnf_transformation,[],[f172])).

fof(f172,plain,(
! [X0,X1] : (~relname(X0,X1) | relation(X0,X1))),
inference(ennf_transformation,[],[f15])).

fof(f15,axiom,(
! [X0,X1] : (relname(X0,X1) => relation(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f215,plain,(
( ! [X0,X1] : (relname(X0,X1) | ~forename(X0,X1)) )),
inference(cnf_transformation,[],[f173])).

fof(f173,plain,(
! [X0,X1] : (~forename(X0,X1) | relname(X0,X1))),
inference(ennf_transformation,[],[f16])).

fof(f16,axiom,(
! [X0,X1] : (forename(X0,X1) => relname(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f243,plain,(
forename(sK5,sK7)),
inference(cnf_transformation,[],[f201])).

fof(f201,plain,(
of(sK5,sK7,sK6) & woman(sK5,sK6) & mia_forename(sK5,sK7) & forename(sK5,sK7) & shake_beverage(sK5,sK8) & event(sK5,sK9) & agent(sK5,sK9,sK6) & patient(sK5,sK9,sK8) & nonreflexive(sK5,sK9) & order(sK5,sK9)),
inference(skolemisation,[status(esa)],[f153])).
fof(f153,plain,(
? [X0,X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & nonreflexive(X0,X4) & order(X0,X4))),
inference(pure_predicate_removal,[],[f152])).

fof(f152,plain,(
? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(pure_predicate_removal,[],[f53])).

fof(f53,plain,(
? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(flattening,[],[f46])).

fof(f46,negated_conjecture,(
~~? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(negated_conjecture,[],[f45])).

fof(f45,conjecture,(
~? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f206,plain,(
( ! [X0,X1] : (entity(X0,X1) | ~organism(X0,X1)) )),
inference(cnf_transformation,[],[f164])).

fof(f164,plain,(
! [X0,X1] : (~organism(X0,X1) | entity(X0,X1))),
inference(ennf_transformation,[],[f6])).

fof(f6,axiom,(
! [X0,X1] : (organism(X0,X1) => entity(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f235,plain,(
( ! [X0,X1] : (~living(X0,X1) | ~nonliving(X0,X1)) )),
inference(cnf_transformation,[],[f193])).

fof(f193,plain,(
! [X0,X1] : (~nonliving(X0,X1) | ~living(X0,X1))),
inference(ennf_transformation,[],[f50])).

fof(f50,plain,(
! [X0,X1] : (nonliving(X0,X1) => ~living(X0,X1))),
inference(flattening,[],[f40])).

fof(f40,axiom,(
! [X0,X1] : (nonliving(X0,X1) => ~living(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f217,plain,(
( ! [X0,X1] : (nonliving(X0,X1) | ~object(X0,X1)) )),
inference(cnf_transformation,[],[f175])).

fof(f175,plain,(
! [X0,X1] : (~object(X0,X1) | nonliving(X0,X1))),
inference(ennf_transformation,[],[f19])).

fof(f19,axiom,(
! [X0,X1] : (object(X0,X1) => nonliving(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f221,plain,(
( ! [X0,X1] : (object(X0,X1) | ~substance_matter(X0,X1)) )),
inference(cnf_transformation,[],[f179])).

fof(f179,plain,(
! [X0,X1] : (~substance_matter(X0,X1) | object(X0,X1))),
inference(ennf_transformation,[],[f24])).

fof(f24,axiom,(
! [X0,X1] : (substance_matter(X0,X1) => object(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f222,plain,(
( ! [X0,X1] : (substance_matter(X0,X1) | ~food(X0,X1)) )),
inference(cnf_transformation,[],[f180])).

fof(f180,plain,(
! [X0,X1] : (~food(X0,X1) | substance_matter(X0,X1))),
inference(ennf_transformation,[],[f25])).

fof(f25,axiom,(
! [X0,X1] : (food(X0,X1) => substance_matter(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f223,plain,(
( ! [X0,X1] : (food(X0,X1) | ~beverage(X0,X1)) )),
inference(cnf_transformation,[],[f181])).

fof(f181,plain,(
! [X0,X1] : (~beverage(X0,X1) | food(X0,X1))),
inference(ennf_transformation,[],[f26])).

fof(f26,axiom,(
! [X0,X1] : (beverage(X0,X1) => food(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f224,plain,(
( ! [X0,X1] : (beverage(X0,X1) | ~shake_beverage(X0,X1)) )),
inference(cnf_transformation,[],[f182])).

fof(f182,plain,(
! [X0,X1] : (~shake_beverage(X0,X1) | beverage(X0,X1))),
inference(ennf_transformation,[],[f27])).

fof(f27,axiom,(
! [X0,X1] : (shake_beverage(X0,X1) => beverage(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f244,plain,(
shake_beverage(sK5,sK8)),
inference(cnf_transformation,[],[f201])).

fof(f205,plain,(
( ! [X0,X1] : (living(X0,X1) | ~organism(X0,X1)) )),
inference(cnf_transformation,[],[f163])).

fof(f163,plain,(
! [X0,X1] : (~organism(X0,X1) | living(X0,X1))),
inference(ennf_transformation,[],[f4])).

fof(f4,axiom,(
! [X0,X1] : (organism(X0,X1) => living(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f207,plain,(
( ! [X0,X1] : (organism(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f165])).

fof(f165,plain,(
! [X0,X1] : (~human_person(X0,X1) | organism(X0,X1))),
inference(ennf_transformation,[],[f7])).

fof(f7,axiom,(
! [X0,X1] : (human_person(X0,X1) => organism(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f234,plain,(
( ! [X0,X1] : (~human(X0,X1) | ~nonhuman(X0,X1)) )),
inference(cnf_transformation,[],[f192])).

fof(f192,plain,(
! [X0,X1] : (~nonhuman(X0,X1) | ~human(X0,X1))),
inference(ennf_transformation,[],[f49])).

fof(f49,plain,(
! [X0,X1] : (nonhuman(X0,X1) => ~human(X0,X1))),
inference(flattening,[],[f39])).

fof(f39,axiom,(
! [X0,X1] : (nonhuman(X0,X1) => ~human(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f212,plain,(
( ! [X0,X1] : (nonhuman(X0,X1) | ~abstraction(X0,X1)) )),
inference(cnf_transformation,[],[f170])).

fof(f170,plain,(
! [X0,X1] : (~abstraction(X0,X1) | nonhuman(X0,X1))),
inference(ennf_transformation,[],[f12])).

fof(f12,axiom,(
! [X0,X1] : (abstraction(X0,X1) => nonhuman(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f204,plain,(
( ! [X0,X1] : (human(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f162])).

fof(f162,plain,(
! [X0,X1] : (~human_person(X0,X1) | human(X0,X1))),
inference(ennf_transformation,[],[f3])).

fof(f3,axiom,(
! [X0,X1] : (human_person(X0,X1) => human(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f208,plain,(
( ! [X0,X1] : (human_person(X0,X1) | ~woman(X0,X1)) )),
inference(cnf_transformation,[],[f166])).

fof(f166,plain,(
! [X0,X1] : (~woman(X0,X1) | human_person(X0,X1))),
inference(ennf_transformation,[],[f8])).

fof(f8,axiom,(
! [X0,X1] : (woman(X0,X1) => human_person(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f233,plain,(
( ! [X0,X1] : (~nonexistent(X0,X1) | ~existent(X0,X1)) )),
inference(cnf_transformation,[],[f191])).

fof(f191,plain,(
! [X0,X1] : (~existent(X0,X1) | ~nonexistent(X0,X1))),
inference(ennf_transformation,[],[f48])).

fof(f48,plain,(
! [X0,X1] : (existent(X0,X1) => ~nonexistent(X0,X1))),
inference(flattening,[],[f38])).

fof(f38,axiom,(
! [X0,X1] : (existent(X0,X1) => ~nonexistent(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f227,plain,(
( ! [X0,X1] : (nonexistent(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f185])).

fof(f185,plain,(
! [X0,X1] : (~eventuality(X0,X1) | nonexistent(X0,X1))),
inference(ennf_transformation,[],[f30])).

fof(f30,axiom,(
! [X0,X1] : (eventuality(X0,X1) => nonexistent(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f229,plain,(
( ! [X0,X1] : (eventuality(X0,X1) | ~event(X0,X1)) )),
inference(cnf_transformation,[],[f187])).

fof(f187,plain,(
! [X0,X1] : (~event(X0,X1) | eventuality(X0,X1))),
inference(ennf_transformation,[],[f34])).

fof(f34,axiom,(
! [X0,X1] : (event(X0,X1) => eventuality(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f245,plain,(
event(sK5,sK9)),
inference(cnf_transformation,[],[f201])).

fof(f218,plain,(
( ! [X0,X1] : (existent(X0,X1) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f176])).

fof(f176,plain,(
! [X0,X1] : (~entity(X0,X1) | existent(X0,X1))),
inference(ennf_transformation,[],[f20])).

fof(f20,axiom,(
! [X0,X1] : (entity(X0,X1) => existent(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f232,plain,(
( ! [X0,X1] : (~nonliving(X0,X1) | ~animate(X0,X1)) )),
inference(cnf_transformation,[],[f190])).

fof(f190,plain,(
! [X0,X1] : (~animate(X0,X1) | ~nonliving(X0,X1))),
inference(ennf_transformation,[],[f47])).

fof(f47,plain,(
! [X0,X1] : (animate(X0,X1) => ~nonliving(X0,X1))),
inference(flattening,[],[f37])).

fof(f37,axiom,(
! [X0,X1] : (animate(X0,X1) => ~nonliving(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f203,plain,(
( ! [X0,X1] : (animate(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f161])).

fof(f161,plain,(
! [X0,X1] : (~human_person(X0,X1) | animate(X0,X1))),
inference(ennf_transformation,[],[f2])).

fof(f2,axiom,(
! [X0,X1] : (human_person(X0,X1) => animate(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f228,plain,(
( ! [X0,X1] : (specific(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f186])).

fof(f186,plain,(
! [X0,X1] : (~eventuality(X0,X1) | specific(X0,X1))),
inference(ennf_transformation,[],[f31])).

fof(f31,axiom,(
! [X0,X1] : (eventuality(X0,X1) => specific(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f237,plain,(
( ! [X0,X1] : (~female(X0,X1) | ~unisex(X0,X1)) )),
inference(cnf_transformation,[],[f195])).

fof(f195,plain,(
! [X0,X1] : (~unisex(X0,X1) | ~female(X0,X1))),
inference(ennf_transformation,[],[f52])).

fof(f52,plain,(
! [X0,X1] : (unisex(X0,X1) => ~female(X0,X1))),
inference(flattening,[],[f42])).

fof(f42,axiom,(
! [X0,X1] : (unisex(X0,X1) => ~female(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f210,plain,(
( ! [X0,X1] : (unisex(X0,X1) | ~abstraction(X0,X1)) )),
inference(cnf_transformation,[],[f168])).

fof(f168,plain,(
! [X0,X1] : (~abstraction(X0,X1) | unisex(X0,X1))),
inference(ennf_transformation,[],[f10])).

fof(f10,axiom,(
! [X0,X1] : (abstraction(X0,X1) => unisex(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f226,plain,(
( ! [X0,X1] : (unisex(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f184])).

fof(f184,plain,(
! [X0,X1] : (~eventuality(X0,X1) | unisex(X0,X1))),
inference(ennf_transformation,[],[f29])).

fof(f29,axiom,(
! [X0,X1] : (eventuality(X0,X1) => unisex(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f216,plain,(
( ! [X0,X1] : (unisex(X0,X1) | ~object(X0,X1)) )),
inference(cnf_transformation,[],[f174])).

fof(f174,plain,(
! [X0,X1] : (~object(X0,X1) | unisex(X0,X1))),
inference(ennf_transformation,[],[f17])).

fof(f17,axiom,(
! [X0,X1] : (object(X0,X1) => unisex(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f238,plain,(
( ! [X2,X0,X3,X1] : (~of(X0,X3,X1) | X2 = X3 | ~forename(X0,X3) | ~of(X0,X2,X1) | ~forename(X0,X2) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f197])).

fof(f197,plain,(
! [X0,X1,X2] : (~entity(X0,X1) | ~forename(X0,X2) | ~of(X0,X2,X1) | ! [X3] : (~forename(X0,X3) | X2 = X3 | ~of(X0,X3,X1)))),
inference(flattening,[],[f196])).

fof(f196,plain,(
! [X0,X1,X2] : ((~entity(X0,X1) | ~forename(X0,X2) | ~of(X0,X2,X1)) | ! [X3] : (~forename(X0,X3) | X2 = X3 | ~of(X0,X3,X1)))),
inference(ennf_transformation,[],[f43])).

fof(f43,axiom,(
! [X0,X1,X2] : ((entity(X0,X1) & forename(X0,X2) & of(X0,X2,X1)) => ~? [X3] : (forename(X0,X3) & X2 != X3 & of(X0,X3,X1)))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f240,plain,(
of(sK5,sK7,sK6)),
inference(cnf_transformation,[],[f201])).

fof(f220,plain,(
( ! [X0,X1] : (entity(X0,X1) | ~object(X0,X1)) )),
inference(cnf_transformation,[],[f178])).

fof(f178,plain,(
! [X0,X1] : (~object(X0,X1) | entity(X0,X1))),
inference(ennf_transformation,[],[f23])).

fof(f23,axiom,(
! [X0,X1] : (object(X0,X1) => entity(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f239,plain,(
( ! [X2,X0,X1] : (~nonreflexive(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X2)) )),
inference(cnf_transformation,[],[f200])).

fof(f200,plain,(
! [X0,X1,X2] : (~patient(X0,X1,X2) | ~agent(X0,X1,X2) | ~nonreflexive(X0,X1))),
inference(equality_propagation,[],[f199])).

fof(f199,plain,(
! [X0,X1,X2,X3] : (~nonreflexive(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3) | X2 != X3)),
inference(flattening,[],[f198])).

fof(f198,plain,(
! [X0,X1,X2,X3] : ((~nonreflexive(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3)) | X2 != X3)),
inference(ennf_transformation,[],[f44])).

fof(f44,axiom,(
! [X0,X1,X2,X3] : ((nonreflexive(X0,X1) & agent(X0,X1,X2) & patient(X0,X1,X3)) => X2 != X3)),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f247,plain,(
patient(sK5,sK9,sK8)),
inference(cnf_transformation,[],[f201])).

fof(f248,plain,(
nonreflexive(sK5,sK9)),
inference(cnf_transformation,[],[f201])).

fof(f202,plain,(
( ! [X0,X1] : (female(X0,X1) | ~woman(X0,X1)) )),
inference(cnf_transformation,[],[f160])).

fof(f160,plain,(
! [X0,X1] : (~woman(X0,X1) | female(X0,X1))),
inference(ennf_transformation,[],[f1])).

fof(f1,axiom,(
! [X0,X1] : (woman(X0,X1) => female(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f241,plain,(
woman(sK5,sK6)),
inference(cnf_transformation,[],[f201])).

fof(f242,plain,(
mia_forename(sK5,sK7)),
inference(cnf_transformation,[],[f201])).

fof(f246,plain,(
agent(sK5,sK9,sK6)),
inference(cnf_transformation,[],[f201])).

fof(f249,plain,(
order(sK5,sK9)),
inference(cnf_transformation,[],[f201])).

fof(f231,plain,(
( ! [X0,X1] : (act(X0,X1) | ~order(X0,X1)) )),
inference(cnf_transformation,[],[f189])).

fof(f189,plain,(
! [X0,X1] : (~order(X0,X1) | act(X0,X1))),
inference(ennf_transformation,[],[f36])).

fof(f36,axiom,(
! [X0,X1] : (order(X0,X1) => act(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f230,plain,(
( ! [X0,X1] : (event(X0,X1) | ~act(X0,X1)) )),
inference(cnf_transformation,[],[f188])).

fof(f188,plain,(
! [X0,X1] : (~act(X0,X1) | event(X0,X1))),
inference(ennf_transformation,[],[f35])).

fof(f35,axiom,(
! [X0,X1] : (act(X0,X1) => event(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f225,plain,(
( ! [X0,X1] : (event(X0,X1) | ~order(X0,X1)) )),
inference(cnf_transformation,[],[f183])).

fof(f183,plain,(
! [X0,X1] : (~order(X0,X1) | event(X0,X1))),
inference(ennf_transformation,[],[f28])).

fof(f28,axiom,(
! [X0,X1] : (order(X0,X1) => event(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f209,plain,(
( ! [X0,X1] : (forename(X0,X1) | ~mia_forename(X0,X1)) )),
inference(cnf_transformation,[],[f167])).

fof(f167,plain,(
! [X0,X1] : (~mia_forename(X0,X1) | forename(X0,X1))),
inference(ennf_transformation,[],[f9])).

fof(f9,axiom,(
! [X0,X1] : (mia_forename(X0,X1) => forename(X0,X1))),
file('/Users/korovin/TPTP-v5.4.0/Problems/NLP/NLP042+1.p',unknown)).

cnf(c_573,plain,
( specific(X0_$i,X1_$i)
| ~ specific(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_500,plain,( X0_$i = X0_$i ),theory(equality) ).

cnf(c_1761,plain,
( specific(X0_$i,X1_$i) | ~ specific(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_573,c_500]) ).

cnf(c_564,plain,
( organism(X0_$i,X1_$i)
| ~ organism(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1748,plain,
( organism(X0_$i,X1_$i) | ~ organism(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_564,c_500]) ).

cnf(c_562,plain,
( human_person(X0_$i,X1_$i)
| ~ human_person(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1736,plain,
( human_person(X0_$i,X1_$i)
| ~ human_person(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_562,c_500]) ).

cnf(c_557,plain,
( general(X0_$i,X1_$i)
| ~ general(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1724,plain,
( general(X0_$i,X1_$i) | ~ general(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_557,c_500]) ).

cnf(c_555,plain,
( abstraction(X0_$i,X1_$i)
| ~ abstraction(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1703,plain,
( abstraction(X0_$i,X1_$i)
| ~ abstraction(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_555,c_500]) ).

cnf(c_553,plain,
( relation(X0_$i,X1_$i)
| ~ relation(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1682,plain,
( relation(X0_$i,X1_$i) | ~ relation(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_553,c_500]) ).

cnf(c_551,plain,
( relname(X0_$i,X1_$i)
| ~ relname(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1661,plain,
( relname(X0_$i,X1_$i) | ~ relname(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_551,c_500]) ).

cnf(c_548,plain,
( unisex(X0_$i,X1_$i)
| ~ unisex(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1638,plain,
( unisex(X0_$i,X1_$i) | ~ unisex(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_548,c_500]) ).

cnf(c_546,plain,
( female(X0_$i,X1_$i)
| ~ female(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1569,plain,
( female(X0_$i,X1_$i) | ~ female(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_546,c_500]) ).

cnf(c_543,plain,
( nonhuman(X0_$i,X1_$i)
| ~ nonhuman(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1557,plain,
( nonhuman(X0_$i,X1_$i) | ~ nonhuman(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_543,c_500]) ).

cnf(c_541,plain,
( human(X0_$i,X1_$i)
| ~ human(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1545,plain,
( human(X0_$i,X1_$i) | ~ human(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_541,c_500]) ).

cnf(c_538,plain,
( entity(X0_$i,X1_$i)
| ~ entity(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1533,plain,
( entity(X0_$i,X1_$i) | ~ entity(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_538,c_500]) ).

cnf(c_536,plain,
( eventuality(X0_$i,X1_$i)
| ~ eventuality(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1520,plain,
( eventuality(X0_$i,X1_$i)
| ~ eventuality(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_536,c_500]) ).

cnf(c_528,plain,
( act(X0_$i,X1_$i)
| ~ act(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1508,plain,
( act(X0_$i,X1_$i) | ~ act(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_528,c_500]) ).

cnf(c_34,plain,
( ~ general(X0_$i,X1_$i) | ~ specific(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f236]) ).

cnf(c_574,plain,
( ~ general(X0_$i,X1_$i) | ~ specific(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_34]) ).

cnf(c_17,plain,
( ~ entity(X0_$i,X1_$i) | specific(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f219]) ).

cnf(c_558,plain,
( ~ entity(X0_$i,X1_$i) | specific(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_17]) ).

cnf(c_1166,plain,
( ~ entity(X0_$i,X1_$i) | ~ general(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_574,c_558]) ).

cnf(c_9,plain,
( ~ abstraction(X0_$i,X1_$i) | general(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f211]) ).

cnf(c_556,plain,
( ~ abstraction(X0_$i,X1_$i) | general(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_9]) ).

cnf(c_1325,plain,
( ~ entity(X0_$i,X1_$i) | ~ abstraction(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_1166,c_556]) ).

cnf(c_11,plain,
( abstraction(X0_$i,X1_$i) | ~ relation(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f213]) ).

cnf(c_554,plain,
( abstraction(X0_$i,X1_$i) | ~ relation(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_11]) ).

cnf(c_12,plain,
( relation(X0_$i,X1_$i) | ~ relname(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f214]) ).

cnf(c_552,plain,
( relation(X0_$i,X1_$i) | ~ relname(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_12]) ).

cnf(c_13,plain,
( ~ forename(X0_$i,X1_$i) | relname(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f215]) ).

cnf(c_550,plain,
( ~ forename(X0_$i,X1_$i) | relname(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_13]) ).

cnf(c_1054,plain,
( ~ forename(X0_$i,X1_$i) | relation(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_552,c_550]) ).

cnf(c_1065,plain,
( ~ forename(X0_$i,X1_$i) | abstraction(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_554,c_1054]) ).

cnf(c_1393,plain,
( ~ entity(X0_$i,X1_$i) | ~ forename(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_1325,c_1065]) ).

cnf(c_44,plain,
( forename(sK5,sK7) ),
inference(cnf_transformation,[],[f243]) ).

cnf(c_539,plain,
( forename(sK5,sK7) ),
inference(subtyping,[status(esa)],[c_44]) ).

cnf(c_1401,plain,
( ~ entity(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1393,c_539]) ).

cnf(c_4,plain,
( ~ organism(X0_$i,X1_$i) | entity(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f206]) ).

cnf(c_565,plain,
( ~ organism(X0_$i,X1_$i) | entity(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_4]) ).

cnf(c_1405,plain,
( ~ organism(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1401,c_565]) ).

cnf(c_524,plain,
( nonexistent(X0_$i,X1_$i)
| ~ nonexistent(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1385,plain,
( nonexistent(X0_$i,X1_$i)
| ~ nonexistent(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_524,c_500]) ).

cnf(c_522,plain,
( existent(X0_$i,X1_$i)
| ~ existent(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1373,plain,
( existent(X0_$i,X1_$i) | ~ existent(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_522,c_500]) ).

cnf(c_519,plain,
( substance_matter(X0_$i,X1_$i)
| ~ substance_matter(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1361,plain,
( substance_matter(X0_$i,X1_$i)
| ~ substance_matter(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_519,c_500]) ).

cnf(c_517,plain,
( food(X0_$i,X1_$i)
| ~ food(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1349,plain,
( food(X0_$i,X1_$i) | ~ food(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_517,c_500]) ).

cnf(c_515,plain,
( beverage(X0_$i,X1_$i)
| ~ beverage(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1337,plain,
( beverage(X0_$i,X1_$i) | ~ beverage(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_515,c_500]) ).

cnf(c_33,plain,
( ~ living(X0_$i,X1_$i) | ~ nonliving(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f235]) ).

cnf(c_509,plain,
( ~ living(X0_$i,X1_$i) | ~ nonliving(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_33]) ).

cnf(c_15,plain,
( ~ object(X0_$i,X1_$i) | nonliving(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f217]) ).

cnf(c_510,plain,
( ~ object(X0_$i,X1_$i) | nonliving(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_15]) ).

cnf(c_1157,plain,
( ~ living(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_509,c_510]) ).

cnf(c_19,plain,
( object(X0_$i,X1_$i) | ~ substance_matter(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f221]) ).

cnf(c_520,plain,
( object(X0_$i,X1_$i) | ~ substance_matter(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_19]) ).

cnf(c_20,plain,
( substance_matter(X0_$i,X1_$i) | ~ food(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f222]) ).

cnf(c_518,plain,
( substance_matter(X0_$i,X1_$i) | ~ food(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_20]) ).

cnf(c_21,plain,
( food(X0_$i,X1_$i) | ~ beverage(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f223]) ).

cnf(c_516,plain,
( food(X0_$i,X1_$i) | ~ beverage(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_21]) ).

cnf(c_22,plain,
( beverage(X0_$i,X1_$i) | ~ shake_beverage(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f224]) ).

cnf(c_514,plain,
( beverage(X0_$i,X1_$i) | ~ shake_beverage(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_22]) ).

cnf(c_43,plain,
( shake_beverage(sK5,sK8) ),
inference(cnf_transformation,[],[f244]) ).

cnf(c_512,plain,
( shake_beverage(sK5,sK8) ),
inference(subtyping,[status(esa)],[c_43]) ).

cnf(c_600,plain,
( beverage(sK5,sK8) ),
inference(resolution,[status(thm)],[c_514,c_512]) ).

cnf(c_765,plain,
( food(sK5,sK8) ),
inference(resolution,[status(thm)],[c_516,c_600]) ).

cnf(c_925,plain,
( substance_matter(sK5,sK8) ),
inference(resolution,[status(thm)],[c_518,c_765]) ).

cnf(c_1013,plain,
( object(sK5,sK8) ),
inference(resolution,[status(thm)],[c_520,c_925]) ).

cnf(c_1309,plain,
( ~ living(sK5,sK8) ),
inference(resolution,[status(thm)],[c_1157,c_1013]) ).

cnf(c_3,plain,
( living(X0_$i,X1_$i) | ~ organism(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f205]) ).

cnf(c_507,plain,
( living(X0_$i,X1_$i) | ~ organism(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_3]) ).

cnf(c_5,plain,
( ~ human_person(X0_$i,X1_$i) | organism(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f207]) ).

cnf(c_563,plain,
( ~ human_person(X0_$i,X1_$i) | organism(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_5]) ).

cnf(c_1092,plain,
( ~ human_person(X0_$i,X1_$i) | living(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_507,c_563]) ).

cnf(c_1313,plain,
( ~ human_person(sK5,sK8) ),
inference(resolution,[status(thm)],[c_1309,c_1092]) ).

cnf(c_32,plain,
( ~ human(X0_$i,X1_$i) | ~ nonhuman(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f234]) ).

cnf(c_542,plain,
( ~ human(X0_$i,X1_$i) | ~ nonhuman(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_32]) ).

cnf(c_10,plain,
( ~ abstraction(X0_$i,X1_$i) | nonhuman(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f212]) ).

cnf(c_544,plain,
( ~ abstraction(X0_$i,X1_$i) | nonhuman(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_10]) ).

cnf(c_1125,plain,
( ~ human(X0_$i,X1_$i) | ~ abstraction(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_542,c_544]) ).

cnf(c_1285,plain,
( ~ human(X0_$i,X1_$i) | ~ forename(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_1125,c_1065]) ).

cnf(c_1292,plain,
( ~ human(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1285,c_539]) ).

cnf(c_2,plain,
( ~ human_person(X0_$i,X1_$i) | human(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f204]) ).

cnf(c_540,plain,
( ~ human_person(X0_$i,X1_$i) | human(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_2]) ).

cnf(c_1296,plain,
( ~ human_person(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1292,c_540]) ).

cnf(c_6,plain,
( ~ woman(X0_$i,X1_$i) | human_person(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f208]) ).

cnf(c_561,plain,
( ~ woman(X0_$i,X1_$i) | human_person(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_6]) ).

cnf(c_1300,plain,
( ~ woman(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1296,c_561]) ).

cnf(c_31,plain,
( ~ existent(X0_$i,X1_$i) | ~ nonexistent(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f233]) ).

cnf(c_525,plain,
( ~ existent(X0_$i,X1_$i) | ~ nonexistent(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_31]) ).

cnf(c_25,plain,
( ~ eventuality(X0_$i,X1_$i) | nonexistent(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f227]) ).

cnf(c_523,plain,
( ~ eventuality(X0_$i,X1_$i) | nonexistent(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_25]) ).

cnf(c_1118,plain,
( ~ existent(X0_$i,X1_$i) | ~ eventuality(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_525,c_523]) ).

cnf(c_27,plain,
( ~ event(X0_$i,X1_$i) | eventuality(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f229]) ).

cnf(c_535,plain,
( ~ event(X0_$i,X1_$i) | eventuality(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_27]) ).

cnf(c_1196,plain,
( ~ existent(X0_$i,X1_$i) | ~ event(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_1118,c_535]) ).

cnf(c_42,plain,( event(sK5,sK9) ),inference(cnf_transformation,[],[f245]) ).

cnf(c_534,plain,
( event(sK5,sK9) ),
inference(subtyping,[status(esa)],[c_42]) ).

cnf(c_1260,plain,
( ~ existent(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1196,c_534]) ).

cnf(c_16,plain,
( ~ entity(X0_$i,X1_$i) | existent(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f218]) ).

cnf(c_521,plain,
( ~ entity(X0_$i,X1_$i) | existent(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_16]) ).

cnf(c_1264,plain,
( ~ entity(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1260,c_521]) ).

cnf(c_1268,plain,
( ~ organism(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1264,c_565]) ).

cnf(c_1272,plain,
( ~ human_person(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1268,c_563]) ).

cnf(c_1276,plain,
( ~ woman(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1272,c_561]) ).

cnf(c_511,plain,
( object(X0_$i,X1_$i)
| ~ object(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1253,plain,
( object(X0_$i,X1_$i) | ~ object(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_511,c_500]) ).

cnf(c_508,plain,
( living(X0_$i,X1_$i)
| ~ living(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1241,plain,
( living(X0_$i,X1_$i) | ~ living(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_508,c_500]) ).

cnf(c_506,plain,
( nonliving(X0_$i,X1_$i)
| ~ nonliving(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1229,plain,
( nonliving(X0_$i,X1_$i) | ~ nonliving(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_506,c_500]) ).

cnf(c_504,plain,
( animate(X0_$i,X1_$i)
| ~ animate(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_1217,plain,
( animate(X0_$i,X1_$i) | ~ animate(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_504,c_500]) ).

cnf(c_499,plain,
( X0_$i != X1_$i | X2_$i != X1_$i | X2_$i = X0_$i ),
theory(equality) ).

cnf(c_1205,plain,
( X0_$i != X1_$i | X1_$i = X0_$i ),
inference(resolution,[status(thm)],[c_499,c_500]) ).

cnf(c_30,plain,
( ~ animate(X0_$i,X1_$i) | ~ nonliving(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f232]) ).

cnf(c_505,plain,
( ~ animate(X0_$i,X1_$i) | ~ nonliving(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_30]) ).

cnf(c_1107,plain,
( ~ animate(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_505,c_510]) ).

cnf(c_1183,plain,
( ~ animate(sK5,sK8) ),
inference(resolution,[status(thm)],[c_1107,c_1013]) ).

cnf(c_1,plain,
( animate(X0_$i,X1_$i) | ~ human_person(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f203]) ).

cnf(c_503,plain,
( animate(X0_$i,X1_$i) | ~ human_person(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_1]) ).

cnf(c_755,plain,
( ~ woman(X0_$i,X1_$i) | animate(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_503,c_561]) ).

cnf(c_1187,plain,
( ~ woman(sK5,sK8) ),
inference(resolution,[status(thm)],[c_1183,c_755]) ).

cnf(c_26,plain,
( specific(X0_$i,X1_$i) | ~ eventuality(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f228]) ).

cnf(c_537,plain,
( specific(X0_$i,X1_$i) | ~ eventuality(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_26]) ).

cnf(c_946,plain,
( specific(X0_$i,X1_$i) | ~ event(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_537,c_535]) ).

cnf(c_962,plain,
( specific(sK5,sK9) ),
inference(resolution,[status(thm)],[c_946,c_534]) ).

cnf(c_1165,plain,
( ~ general(sK5,sK9) ),
inference(resolution,[status(thm)],[c_574,c_962]) ).

cnf(c_1170,plain,
( ~ abstraction(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1165,c_556]) ).

cnf(c_1174,plain,
( ~ forename(sK5,sK9) ),
inference(resolution,[status(thm)],[c_1170,c_1065]) ).

cnf(c_35,plain,
( ~ female(X0_$i,X1_$i) | ~ unisex(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f237]) ).

cnf(c_547,plain,
( ~ female(X0_$i,X1_$i) | ~ unisex(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_35]) ).

cnf(c_8,plain,
( unisex(X0_$i,X1_$i) | ~ abstraction(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f210]) ).

cnf(c_549,plain,
( unisex(X0_$i,X1_$i) | ~ abstraction(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_8]) ).

cnf(c_1071,plain,
( ~ forename(X0_$i,X1_$i) | unisex(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_549,c_1065]) ).

cnf(c_1136,plain,
( ~ female(X0_$i,X1_$i) | ~ forename(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_547,c_1071]) ).

cnf(c_1148,plain,
( ~ female(sK5,sK7) ),
inference(resolution,[status(thm)],[c_1136,c_539]) ).

cnf(c_24,plain,
( unisex(X0_$i,X1_$i) | ~ eventuality(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f226]) ).

cnf(c_526,plain,
( unisex(X0_$i,X1_$i) | ~ eventuality(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_24]) ).

cnf(c_940,plain,
( unisex(X0_$i,X1_$i) | ~ event(X0_$i,X1_$i) ),
inference(resolution,[status(thm)],[c_526,c_535]) ).

cnf(c_954,plain,
( unisex(sK5,sK9) ),
inference(resolution,[status(thm)],[c_940,c_534]) ).

cnf(c_1135,plain,
( ~ female(sK5,sK9) ),
inference(resolution,[status(thm)],[c_547,c_954]) ).

cnf(c_14,plain,
( unisex(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f216]) ).

cnf(c_501,plain,
( unisex(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_14]) ).

cnf(c_1016,plain,
( unisex(sK5,sK8) ),
inference(resolution,[status(thm)],[c_501,c_1013]) ).

cnf(c_1134,plain,
( ~ female(sK5,sK8) ),
inference(resolution,[status(thm)],[c_547,c_1016]) ).

cnf(c_36,plain,
( ~ entity(X0_$i,X1_$i)
| ~ forename(X0_$i,X2_$i)
| ~ forename(X0_$i,X3_$i)
| ~ of(X0_$i,X2_$i,X1_$i) | ~ of(X0_$i,X3_$i,X1_$i)
| X2_$i = X3_$i ),
inference(cnf_transformation,[],[f238]) ).

cnf(c_572,plain,
( ~ entity(X0_$i,X1_$i)
| ~ forename(X0_$i,X2_$i)
| ~ forename(X0_$i,X3_$i)
| ~ of(X0_$i,X2_$i,X1_$i) | ~ of(X0_$i,X3_$i,X1_$i)
| X2_$i = X3_$i ),
inference(subtyping,[status(esa)],[c_36]) ).

cnf(c_47,plain,( of(sK5,sK7,sK6) ),inference(cnf_transformation,[],[f240]) ).

cnf(c_570,plain,
( of(sK5,sK7,sK6) ),
inference(subtyping,[status(esa)],[c_47]) ).

cnf(c_1039,plain,
( ~ entity(sK5,sK6)
| ~ forename(sK5,sK7)
| ~ forename(sK5,X0_$i) | ~ of(sK5,X0_$i,sK6)
| X0_$i = sK7 ), inference(resolution,[status(thm)],[c_572,c_570]) ). cnf(c_51,plain, ( forename(sK5,sK7) ), inference(subtyping,[status(esa)],[c_44]) ). cnf(c_1040,plain, ( ~ entity(sK5,sK6) | ~ forename(sK5,X0_$i)
| ~ of(sK5,X0_$i,sK6) | X0_$i = sK7 ),
inference(global_propositional_subsumption,[status(thm)],[c_1039,c_51]) ).

cnf(c_18,plain,
( entity(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f220]) ).

cnf(c_502,plain,
( entity(X0_$i,X1_$i) | ~ object(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_18]) ).

cnf(c_1019,plain,
( entity(sK5,sK8) ),
inference(resolution,[status(thm)],[c_502,c_1013]) ).

cnf(c_571,plain,
( of(X0_$i,X1_$i,X2_$i) | ~ of(X3_$i,X4_$i,X5_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i
| X2_$i != X5_$i ),
theory(equality) ).

cnf(c_979,plain,
( of(X0_$i,X1_$i,X2_$i) | ~ of(X3_$i,X4_$i,X2_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i ),
inference(resolution,[status(thm)],[c_571,c_500]) ).

cnf(c_991,plain,
( of(X0_$i,X1_$i,X2_$i) | ~ of(X3_$i,X1_$i,X2_$i) | X0_$i != X3_$i ),
inference(resolution,[status(thm)],[c_979,c_500]) ).

cnf(c_497,plain,
( patient(X0_$i,X1_$i,X2_$i) | ~ patient(X3_$i,X4_$i,X5_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i
| X2_$i != X5_$i ),
theory(equality) ).

cnf(c_903,plain,
( patient(X0_$i,X1_$i,X2_$i) | ~ patient(X3_$i,X4_$i,X2_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i ),
inference(resolution,[status(thm)],[c_497,c_500]) ).

cnf(c_915,plain,
( patient(X0_$i,X1_$i,X2_$i) | ~ patient(X3_$i,X1_$i,X2_$i)
| X0_$i != X3_$i ),
inference(resolution,[status(thm)],[c_903,c_500]) ).

cnf(c_495,plain,
( agent(X0_$i,X1_$i,X2_$i) | ~ agent(X3_$i,X4_$i,X5_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i
| X2_$i != X5_$i ),
theory(equality) ).

cnf(c_867,plain,
( agent(X0_$i,X1_$i,X2_$i) | ~ agent(X3_$i,X4_$i,X2_$i)
| X0_$i != X3_$i
| X1_$i != X4_$i ),
inference(resolution,[status(thm)],[c_495,c_500]) ).

cnf(c_879,plain,
( agent(X0_$i,X1_$i,X2_$i) | ~ agent(X3_$i,X1_$i,X2_$i)
| X0_$i != X3_$i ),
inference(resolution,[status(thm)],[c_867,c_500]) ).

cnf(c_569,plain,
( forename(X0_$i,X1_$i)
| ~ forename(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_843,plain,
( forename(X0_$i,X1_$i) | ~ forename(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_569,c_500]) ).

cnf(c_567,plain,
( mia_forename(X0_$i,X1_$i)
| ~ mia_forename(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_822,plain,
( mia_forename(X0_$i,X1_$i)
| ~ mia_forename(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_567,c_500]) ).

cnf(c_560,plain,
( woman(X0_$i,X1_$i)
| ~ woman(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_801,plain,
( woman(X0_$i,X1_$i) | ~ woman(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_560,c_500]) ).

cnf(c_532,plain,
( order(X0_$i,X1_$i)
| ~ order(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_754,plain,
( order(X0_$i,X1_$i) | ~ order(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_532,c_500]) ).

cnf(c_530,plain,
( event(X0_$i,X1_$i)
| ~ event(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_733,plain,
( event(X0_$i,X1_$i) | ~ event(X2_$i,X1_$i) | X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_530,c_500]) ).

cnf(c_513,plain,
( shake_beverage(X0_$i,X1_$i)
| ~ shake_beverage(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_712,plain,
( shake_beverage(X0_$i,X1_$i)
| ~ shake_beverage(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_513,c_500]) ).

cnf(c_493,plain,
( nonreflexive(X0_$i,X1_$i)
| ~ nonreflexive(X2_$i,X3_$i)
| X0_$i != X2_$i
| X1_$i != X3_$i ),
theory(equality) ).

cnf(c_691,plain,
( nonreflexive(X0_$i,X1_$i)
| ~ nonreflexive(X2_$i,X1_$i)
| X0_$i != X2_$i ),
inference(resolution,[status(thm)],[c_493,c_500]) ).

cnf(c_37,plain,
( ~ nonreflexive(X0_$i,X1_$i)
| ~ agent(X0_$i,X1_$i,X2_$i) | ~ patient(X0_$i,X1_$i,X2_$i) ),
inference(cnf_transformation,[],[f239]) ).

cnf(c_498,plain,
( ~ nonreflexive(X0_$i,X1_$i)
| ~ agent(X0_$i,X1_$i,X2_$i) | ~ patient(X0_$i,X1_$i,X2_$i) ),
inference(subtyping,[status(esa)],[c_37]) ).

cnf(c_40,plain,
( patient(sK5,sK9,sK8) ),
inference(cnf_transformation,[],[f247]) ).

cnf(c_496,plain,
( patient(sK5,sK9,sK8) ),
inference(subtyping,[status(esa)],[c_40]) ).

cnf(c_676,plain,
( ~ nonreflexive(sK5,sK9) | ~ agent(sK5,sK9,sK8) ),
inference(resolution,[status(thm)],[c_498,c_496]) ).

cnf(c_39,plain,
( nonreflexive(sK5,sK9) ),
inference(cnf_transformation,[],[f248]) ).

cnf(c_56,plain,
( nonreflexive(sK5,sK9) ),
inference(subtyping,[status(esa)],[c_39]) ).

cnf(c_677,plain,
( ~ agent(sK5,sK9,sK8) ),
inference(global_propositional_subsumption,[status(thm)],[c_676,c_56]) ).

cnf(c_0,plain,
( female(X0_$i,X1_$i) | ~ woman(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f202]) ).

cnf(c_545,plain,
( female(X0_$i,X1_$i) | ~ woman(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_0]) ).

cnf(c_46,plain,( woman(sK5,sK6) ),inference(cnf_transformation,[],[f241]) ).

cnf(c_559,plain,
( woman(sK5,sK6) ),
inference(subtyping,[status(esa)],[c_46]) ).

cnf(c_648,plain,
( female(sK5,sK6) ),
inference(resolution,[status(thm)],[c_545,c_559]) ).

cnf(c_45,plain,
( mia_forename(sK5,sK7) ),
inference(cnf_transformation,[],[f242]) ).

cnf(c_566,plain,
( mia_forename(sK5,sK7) ),
inference(subtyping,[status(esa)],[c_45]) ).

cnf(c_41,plain,
( agent(sK5,sK9,sK6) ),
inference(cnf_transformation,[],[f246]) ).

cnf(c_494,plain,
( agent(sK5,sK9,sK6) ),
inference(subtyping,[status(esa)],[c_41]) ).

cnf(c_492,plain,
( nonreflexive(sK5,sK9) ),
inference(subtyping,[status(esa)],[c_39]) ).

cnf(c_38,plain,( order(sK5,sK9) ),inference(cnf_transformation,[],[f249]) ).

cnf(c_531,plain,
( order(sK5,sK9) ),
inference(subtyping,[status(esa)],[c_38]) ).

cnf(c_29,plain,
( ~ order(X0_$i,X1_$i) | act(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f231]) ).

cnf(c_527,plain,
( ~ order(X0_$i,X1_$i) | act(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_29]) ).

cnf(c_28,plain,
( event(X0_$i,X1_$i) | ~ act(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f230]) ).

cnf(c_529,plain,
( event(X0_$i,X1_$i) | ~ act(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_28]) ).

cnf(c_23,plain,
( event(X0_$i,X1_$i) | ~ order(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f225]) ).

cnf(c_533,plain,
( event(X0_$i,X1_$i) | ~ order(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_23]) ).

cnf(c_7,plain,
( forename(X0_$i,X1_$i) | ~ mia_forename(X0_$i,X1_$i) ),
inference(cnf_transformation,[],[f209]) ).

cnf(c_568,plain,
( forename(X0_$i,X1_$i) | ~ mia_forename(X0_$i,X1_$i) ),
inference(subtyping,[status(esa)],[c_7]) ).

% SZS output end Saturation


### Sample finite model for NLP042+1

%------ The model is defined over ground terms (initial term algebra).
%------ Predicates are defined as (\forall x_1,..,x_n  ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n))))
%------ where \phi is a formula over the term algebra.
%------ If we have equality in the problem then it is also defined as a predicate above,
%------ with "=" on the right-hand-side of the definition interpreted over the term algebra $$term_algebra_type %------ See help for --sat_out_model for different model outputs. %------ equality_sorted(X0,X1,X2) can be used in the place of usual "=" %------ where the first argument stands for the sort (i in the unsorted case) % SZS output start Model %------ Negative definition of$$equality_sorted
fof(lit_def,axiom,
(! [X0_$tType,X0_$i,X1_$i] : ( ~($$equality_sorted(X0_tType,X0_i,X1_i)) <=> ( ( ( X0_tType=i & X0_i=sK9 ) & ( X1_i!=sK9 ) ) | ( ( X0_tType=i & X0_i=sK8 ) & ( X1_i!=sK8 ) ) | ( ( X0_tType=i & X0_i=sK6 ) & ( X1_i!=sK6 ) ) | ( ( X0_tType=i & X0_i=sK7 ) & ( X1_i!=sK7 ) ) | ( ( X0_tType=i & X1_i=sK9 ) & ( X0_i!=sK9 ) ) | ( ( X0_tType=i & X1_i=sK8 ) & ( X0_i!=sK8 ) ) | ( ( X0_tType=i & X1_i=sK6 ) & ( X0_i!=sK6 ) ) | ( ( X0_tType=i & X1_i=sK7 ) & ( X0_i!=sK7 ) ) ) ) ) ). %------ Positive definition of female fof(lit_def,axiom, (! [X0_i,X1_i] : ( female(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of woman fof(lit_def,axiom, (! [X0_i,X1_i] : ( woman(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of animate fof(lit_def,axiom, (! [X0_i,X1_i] : ( animate(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of human_person fof(lit_def,axiom, (! [X0_i,X1_i] : ( human_person(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of human fof(lit_def,axiom, (! [X0_i,X1_i] : ( human(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of living fof(lit_def,axiom, (! [X0_i,X1_i] : ( living(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of organism fof(lit_def,axiom, (! [X0_i,X1_i] : ( organism(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of entity fof(lit_def,axiom, (! [X0_i,X1_i] : ( entity(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK8 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of forename fof(lit_def,axiom, (! [X0_i,X1_i] : ( forename(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of mia_forename fof(lit_def,axiom, (! [X0_i,X1_i] : ( mia_forename(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of unisex fof(lit_def,axiom, (! [X0_i,X1_i] : ( unisex(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK9 ) ) | ( ( X1_i=sK8 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of abstraction fof(lit_def,axiom, (! [X0_i,X1_i] : ( abstraction(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of general fof(lit_def,axiom, (! [X0_i,X1_i] : ( general(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of nonhuman fof(lit_def,axiom, (! [X0_i,X1_i] : ( nonhuman(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of relation fof(lit_def,axiom, (! [X0_i,X1_i] : ( relation(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of relname fof(lit_def,axiom, (! [X0_i,X1_i] : ( relname(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 ) ) | ( ( X1_i=sK7 ) ) ) ) ) ). %------ Positive definition of object fof(lit_def,axiom, (! [X0_i,X1_i] : ( object(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of nonliving fof(lit_def,axiom, (! [X0_i,X1_i] : ( nonliving(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of existent fof(lit_def,axiom, (! [X0_i,X1_i] : ( existent(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK8 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of specific fof(lit_def,axiom, (! [X0_i,X1_i] : ( specific(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X0_i=sK5 & X1_i=sK6 ) ) | ( ( X1_i=sK9 ) ) | ( ( X1_i=sK8 ) ) | ( ( X1_i=sK6 ) ) ) ) ) ). %------ Positive definition of substance_matter fof(lit_def,axiom, (! [X0_i,X1_i] : ( substance_matter(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of food fof(lit_def,axiom, (! [X0_i,X1_i] : ( food(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of beverage fof(lit_def,axiom, (! [X0_i,X1_i] : ( beverage(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of shake_beverage fof(lit_def,axiom, (! [X0_i,X1_i] : ( shake_beverage(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK8 ) ) | ( ( X1_i=sK8 ) ) ) ) ) ). %------ Positive definition of event fof(lit_def,axiom, (! [X0_i,X1_i] : ( event(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of order fof(lit_def,axiom, (! [X0_i,X1_i] : ( order(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of eventuality fof(lit_def,axiom, (! [X0_i,X1_i] : ( eventuality(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of nonexistent fof(lit_def,axiom, (! [X0_i,X1_i] : ( nonexistent(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of act fof(lit_def,axiom, (! [X0_i,X1_i] : ( act(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of of fof(lit_def,axiom, (! [X0_i,X1_i,X2_i] : ( of(X0_i,X1_i,X2_i) <=> ( ( ( X0_i=sK5 & X1_i=sK7 & X2_i=sK6 ) ) | ( ( X1_i=sK7 & X2_i=sK6 ) ) ) ) ) ). %------ Positive definition of nonreflexive fof(lit_def,axiom, (! [X0_i,X1_i] : ( nonreflexive(X0_i,X1_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 ) ) | ( ( X1_i=sK9 ) ) ) ) ) ). %------ Positive definition of agent fof(lit_def,axiom, (! [X0_i,X1_i,X2_i] : ( agent(X0_i,X1_i,X2_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 & X2_i=sK6 ) ) | ( ( X1_i=sK9 & X2_i=sK6 ) ) ) ) ) ). %------ Positive definition of patient fof(lit_def,axiom, (! [X0_i,X1_i,X2_i] : ( patient(X0_i,X1_i,X2_i) <=> ( ( ( X0_i=sK5 & X1_i=sK9 & X2_i=sK8 ) ) | ( ( X1_i=sK9 & X2_i=sK8 ) ) ) ) ) ). % SZS output end Model  ### Sample solution for SWV017+1 % SZS output start Saturation fof(f168,plain,( ( ! [X0] : (~a_nonce(generate_key(X0))) )), inference(cnf_transformation,[],[f36])). fof(f36,plain,( ! [X0] : ~a_nonce(generate_key(X0))), inference(flattening,[],[f27])). fof(f27,axiom,( ! [X0] : ~a_nonce(generate_key(X0))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f160,plain,( ( ! [X0,X1] : (intruder_message(pair(X0,X1)) | ~intruder_message(X1) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f123])). fof(f123,plain,( ! [X0,X1] : (~intruder_message(X0) | ~intruder_message(X1) | intruder_message(pair(X0,X1)))), inference(flattening,[],[f122])). fof(f122,plain,( ! [X0,X1] : ((~intruder_message(X0) | ~intruder_message(X1)) | intruder_message(pair(X0,X1)))), inference(ennf_transformation,[],[f19])). fof(f19,axiom,( ! [X0,X1] : ((intruder_message(X0) & intruder_message(X1)) => intruder_message(pair(X0,X1)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f176,plain,( ( ! [X0] : (intruder_message(X0) | ~fresh_intruder_nonce(X0)) )), inference(cnf_transformation,[],[f138])). fof(f138,plain,( ! [X0] : (~fresh_intruder_nonce(X0) | (fresh_to_b(X0) & intruder_message(X0)))), inference(ennf_transformation,[],[f33])). fof(f33,axiom,( ! [X0] : (fresh_intruder_nonce(X0) => (fresh_to_b(X0) & intruder_message(X0)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f163,plain,( ( ! [X2,X0,X1] : (intruder_message(X1) | ~party_of_protocol(X2) | ~intruder_holds(key(X1,X2)) | ~intruder_message(encrypt(X0,X1))) )), inference(cnf_transformation,[],[f129])). fof(f129,plain,( ! [X0,X1,X2] : (~intruder_message(encrypt(X0,X1)) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2) | intruder_message(X1))), inference(flattening,[],[f128])). fof(f128,plain,( ! [X0,X1,X2] : ((~intruder_message(encrypt(X0,X1)) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2)) | intruder_message(X1))), inference(ennf_transformation,[],[f22])). fof(f22,axiom,( ! [X0,X1,X2] : ((intruder_message(encrypt(X0,X1)) & intruder_holds(key(X1,X2)) & party_of_protocol(X2)) => intruder_message(X1))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f156,plain,( ( ! [X2,X0,X3,X1] : (intruder_message(X0) | ~intruder_message(quadruple(X0,X1,X2,X3))) )), inference(cnf_transformation,[],[f121])). fof(f121,plain,( ! [X0,X1,X2,X3] : (~intruder_message(quadruple(X0,X1,X2,X3)) | (intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)))), inference(ennf_transformation,[],[f18])). fof(f18,axiom,( ! [X0,X1,X2,X3] : (intruder_message(quadruple(X0,X1,X2,X3)) => (intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f157,plain,( ( ! [X2,X0,X3,X1] : (intruder_message(X1) | ~intruder_message(quadruple(X0,X1,X2,X3))) )), inference(cnf_transformation,[],[f121])). fof(f158,plain,( ( ! [X2,X0,X3,X1] : (intruder_message(X2) | ~intruder_message(quadruple(X0,X1,X2,X3))) )), inference(cnf_transformation,[],[f121])). fof(f159,plain,( ( ! [X2,X0,X3,X1] : (intruder_message(X3) | ~intruder_message(quadruple(X0,X1,X2,X3))) )), inference(cnf_transformation,[],[f121])). fof(f153,plain,( ( ! [X2,X0,X1] : (intruder_message(X0) | ~intruder_message(triple(X0,X1,X2))) )), inference(cnf_transformation,[],[f120])). fof(f120,plain,( ! [X0,X1,X2] : (~intruder_message(triple(X0,X1,X2)) | (intruder_message(X0) & intruder_message(X1) & intruder_message(X2)))), inference(ennf_transformation,[],[f17])). fof(f17,axiom,( ! [X0,X1,X2] : (intruder_message(triple(X0,X1,X2)) => (intruder_message(X0) & intruder_message(X1) & intruder_message(X2)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f154,plain,( ( ! [X2,X0,X1] : (intruder_message(X1) | ~intruder_message(triple(X0,X1,X2))) )), inference(cnf_transformation,[],[f120])). fof(f155,plain,( ( ! [X2,X0,X1] : (intruder_message(X2) | ~intruder_message(triple(X0,X1,X2))) )), inference(cnf_transformation,[],[f120])). fof(f151,plain,( ( ! [X0,X1] : (intruder_message(X0) | ~intruder_message(pair(X0,X1))) )), inference(cnf_transformation,[],[f119])). fof(f119,plain,( ! [X0,X1] : (~intruder_message(pair(X0,X1)) | (intruder_message(X0) & intruder_message(X1)))), inference(ennf_transformation,[],[f16])). fof(f16,axiom,( ! [X0,X1] : (intruder_message(pair(X0,X1)) => (intruder_message(X0) & intruder_message(X1)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f152,plain,( ( ! [X0,X1] : (intruder_message(X1) | ~intruder_message(pair(X0,X1))) )), inference(cnf_transformation,[],[f119])). fof(f150,plain,( ( ! [X2,X0,X1] : (intruder_message(X2) | ~message(sent(X0,X1,X2))) )), inference(cnf_transformation,[],[f118])). fof(f118,plain,( ! [X0,X1,X2] : (~message(sent(X0,X1,X2)) | intruder_message(X2))), inference(ennf_transformation,[],[f15])). fof(f15,axiom,( ! [X0,X1,X2] : (message(sent(X0,X1,X2)) => intruder_message(X2))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f161,plain,( ( ! [X2,X0,X1] : (intruder_message(triple(X0,X1,X2)) | ~intruder_message(X2) | ~intruder_message(X1) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f125])). fof(f125,plain,( ! [X0,X1,X2] : (~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | intruder_message(triple(X0,X1,X2)))), inference(flattening,[],[f124])). fof(f124,plain,( ! [X0,X1,X2] : ((~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2)) | intruder_message(triple(X0,X1,X2)))), inference(ennf_transformation,[],[f20])). fof(f20,axiom,( ! [X0,X1,X2] : ((intruder_message(X0) & intruder_message(X1) & intruder_message(X2)) => intruder_message(triple(X0,X1,X2)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f162,plain,( ( ! [X2,X0,X3,X1] : (intruder_message(quadruple(X0,X1,X2,X3)) | ~intruder_message(X3) | ~intruder_message(X2) | ~intruder_message(X1) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f127])). fof(f127,plain,( ! [X0,X1,X2,X3] : (~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | ~intruder_message(X3) | intruder_message(quadruple(X0,X1,X2,X3)))), inference(flattening,[],[f126])). fof(f126,plain,( ! [X0,X1,X2,X3] : ((~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | ~intruder_message(X3)) | intruder_message(quadruple(X0,X1,X2,X3)))), inference(ennf_transformation,[],[f21])). fof(f21,axiom,( ! [X0,X1,X2,X3] : ((intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)) => intruder_message(quadruple(X0,X1,X2,X3)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f166,plain,( ( ! [X2,X0,X1] : (intruder_message(encrypt(X0,X1)) | ~party_of_protocol(X2) | ~intruder_holds(key(X1,X2)) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f135])). fof(f135,plain,( ! [X0,X1,X2] : (~intruder_message(X0) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2) | intruder_message(encrypt(X0,X1)))), inference(flattening,[],[f134])). fof(f134,plain,( ! [X0,X1,X2] : ((~intruder_message(X0) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2)) | intruder_message(encrypt(X0,X1)))), inference(ennf_transformation,[],[f25])). fof(f25,axiom,( ! [X0,X1,X2] : ((intruder_message(X0) & intruder_holds(key(X1,X2)) & party_of_protocol(X2)) => intruder_message(encrypt(X0,X1)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f147,plain,( t_holds(key(bt,b))), inference(cnf_transformation,[],[f12])). fof(f12,axiom,( t_holds(key(bt,b))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f146,plain,( t_holds(key(at,a))), inference(cnf_transformation,[],[f11])). fof(f11,axiom,( t_holds(key(at,a))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f143,plain,( party_of_protocol(b)), inference(cnf_transformation,[],[f7])). fof(f7,axiom,( party_of_protocol(b)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f139,plain,( party_of_protocol(a)), inference(cnf_transformation,[],[f2])). fof(f2,axiom,( party_of_protocol(a)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f148,plain,( party_of_protocol(t)), inference(cnf_transformation,[],[f13])). fof(f13,axiom,( party_of_protocol(t)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f144,plain,( fresh_to_b(an_a_nonce)), inference(cnf_transformation,[],[f8])). fof(f8,axiom,( fresh_to_b(an_a_nonce)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f175,plain,( ( ! [X0] : (fresh_to_b(X0) | ~fresh_intruder_nonce(X0)) )), inference(cnf_transformation,[],[f138])). fof(f174,plain,( ( ! [X0] : (fresh_intruder_nonce(generate_intruder_nonce(X0)) | ~fresh_intruder_nonce(X0)) )), inference(cnf_transformation,[],[f137])). fof(f137,plain,( ! [X0] : (~fresh_intruder_nonce(X0) | fresh_intruder_nonce(generate_intruder_nonce(X0)))), inference(ennf_transformation,[],[f32])). fof(f32,axiom,( ! [X0] : (fresh_intruder_nonce(X0) => fresh_intruder_nonce(generate_intruder_nonce(X0)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f173,plain,( fresh_intruder_nonce(an_intruder_nonce)), inference(cnf_transformation,[],[f31])). fof(f31,axiom,( fresh_intruder_nonce(an_intruder_nonce)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f141,plain,( a_stored(pair(b,an_a_nonce))), inference(cnf_transformation,[],[f4])). fof(f4,axiom,( a_stored(pair(b,an_a_nonce))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f145,plain,( ( ! [X0,X1] : (message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))) | ~fresh_to_b(X1) | ~message(sent(X0,b,pair(X0,X1)))) )), inference(cnf_transformation,[],[f115])). fof(f115,plain,( ! [X0,X1] : (~message(sent(X0,b,pair(X0,X1))) | ~fresh_to_b(X1) | message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))), inference(flattening,[],[f114])). fof(f114,plain,( ! [X0,X1] : ((~message(sent(X0,b,pair(X0,X1))) | ~fresh_to_b(X1)) | message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))), inference(ennf_transformation,[],[f109])). fof(f109,plain,( ! [X0,X1] : ((message(sent(X0,b,pair(X0,X1))) & fresh_to_b(X1)) => message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))), inference(pure_predicate_removal,[],[f9])). fof(f9,axiom,( ! [X0,X1] : ((message(sent(X0,b,pair(X0,X1))) & fresh_to_b(X1)) => (message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))) & b_stored(pair(X0,X1))))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f164,plain,( ( ! [X2,X0,X1] : (message(sent(X1,X2,X0)) | ~party_of_protocol(X2) | ~party_of_protocol(X1) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f131])). fof(f131,plain,( ! [X0,X1,X2] : (~intruder_message(X0) | ~party_of_protocol(X1) | ~party_of_protocol(X2) | message(sent(X1,X2,X0)))), inference(flattening,[],[f130])). fof(f130,plain,( ! [X0,X1,X2] : ((~intruder_message(X0) | ~party_of_protocol(X1) | ~party_of_protocol(X2)) | message(sent(X1,X2,X0)))), inference(ennf_transformation,[],[f23])). fof(f23,axiom,( ! [X0,X1,X2] : ((intruder_message(X0) & party_of_protocol(X1) & party_of_protocol(X2)) => message(sent(X1,X2,X0)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f140,plain,( message(sent(a,b,pair(a,an_a_nonce)))), inference(cnf_transformation,[],[f3])). fof(f3,axiom,( message(sent(a,b,pair(a,an_a_nonce)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f142,plain,( ( ! [X4,X2,X0,X5,X3,X1] : (message(sent(a,X4,pair(X3,encrypt(X0,X2)))) | ~a_stored(pair(X4,X5)) | ~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0)))) )), inference(cnf_transformation,[],[f113])). fof(f113,plain,( ! [X0,X1,X2,X3,X4,X5] : (~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) | ~a_stored(pair(X4,X5)) | message(sent(a,X4,pair(X3,encrypt(X0,X2)))))), inference(flattening,[],[f112])). fof(f112,plain,( ! [X0,X1,X2,X3,X4,X5] : ((~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) | ~a_stored(pair(X4,X5))) | message(sent(a,X4,pair(X3,encrypt(X0,X2)))))), inference(ennf_transformation,[],[f110])). fof(f110,plain,( ! [X0,X1,X2,X3,X4,X5] : ((message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) & a_stored(pair(X4,X5))) => message(sent(a,X4,pair(X3,encrypt(X0,X2)))))), inference(pure_predicate_removal,[],[f5])). fof(f5,axiom,( ! [X0,X1,X2,X3,X4,X5] : ((message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) & a_stored(pair(X4,X5))) => (message(sent(a,X4,pair(X3,encrypt(X0,X2)))) & a_holds(key(X2,X4))))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f149,plain,( ( ! [X6,X4,X2,X0,X5,X3,X1] : (message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))) | ~a_nonce(X3) | ~t_holds(key(X6,X2)) | ~t_holds(key(X5,X0)) | ~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5))))) )), inference(cnf_transformation,[],[f117])). fof(f117,plain,( ! [X0,X1,X2,X3,X4,X5,X6] : (~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) | ~t_holds(key(X5,X0)) | ~t_holds(key(X6,X2)) | ~a_nonce(X3) | message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))), inference(flattening,[],[f116])). fof(f116,plain,( ! [X0,X1,X2,X3,X4,X5,X6] : ((~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) | ~t_holds(key(X5,X0)) | ~t_holds(key(X6,X2)) | ~a_nonce(X3)) | message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))), inference(ennf_transformation,[],[f14])). fof(f14,axiom,( ! [X0,X1,X2,X3,X4,X5,X6] : ((message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) & t_holds(key(X5,X0)) & t_holds(key(X6,X2)) & a_nonce(X3)) => message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f165,plain,( ( ! [X0,X1] : (intruder_holds(key(X0,X1)) | ~party_of_protocol(X1) | ~intruder_message(X0)) )), inference(cnf_transformation,[],[f133])). fof(f133,plain,( ! [X0,X1] : (~intruder_message(X0) | ~party_of_protocol(X1) | intruder_holds(key(X0,X1)))), inference(flattening,[],[f132])). fof(f132,plain,( ! [X0,X1] : ((~intruder_message(X0) | ~party_of_protocol(X1)) | intruder_holds(key(X0,X1)))), inference(ennf_transformation,[],[f35])). fof(f35,plain,( ! [X0,X1] : ((intruder_message(X0) & party_of_protocol(X1)) => intruder_holds(key(X0,X1)))), inference(rectify,[],[f24])). fof(f24,axiom,( ! [X1,X2] : ((intruder_message(X1) & party_of_protocol(X2)) => intruder_holds(key(X1,X2)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f171,plain,( ( ! [X0] : (~a_nonce(X0) | ~a_key(X0)) )), inference(cnf_transformation,[],[f136])). fof(f136,plain,( ! [X0] : (~a_key(X0) | ~a_nonce(X0))), inference(ennf_transformation,[],[f29])). fof(f29,axiom,( ! [X0] : ~(a_key(X0) & a_nonce(X0))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f172,plain,( ( ! [X0] : (a_key(generate_key(X0))) )), inference(cnf_transformation,[],[f30])). fof(f30,axiom,( ! [X0] : a_key(generate_key(X0))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f170,plain,( ( ! [X0] : (a_nonce(generate_b_nonce(X0))) )), inference(cnf_transformation,[],[f28])). fof(f28,axiom,( ! [X0] : (a_nonce(generate_expiration_time(X0)) & a_nonce(generate_b_nonce(X0)))), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). fof(f169,plain,( ( ! [X0] : (a_nonce(generate_expiration_time(X0))) )), inference(cnf_transformation,[],[f28])). fof(f167,plain,( a_nonce(an_a_nonce)), inference(cnf_transformation,[],[f26])). fof(f26,axiom,( a_nonce(an_a_nonce)), file('/Users/korovin/TPTP-v5.4.0/Problems/SWV/SWV017+1.p',unknown)). cnf(c_29,plain, ( ~ a_nonce(generate_key(X0_i)) ), inference(cnf_transformation,[],[f168]) ). cnf(c_291,plain, ( ~ a_nonce(generate_key(X0_$$iProver_key_$i_1)) ),
inference(subtyping,[status(esa)],[c_29]) ).

cnf(c_21,plain,
( intruder_message(pair(X0_$i,X1_$i))
| ~ intruder_message(X0_$i) | ~ intruder_message(X1_$i) ),
inference(cnf_transformation,[],[f160]) ).

cnf(c_298,plain,
( intruder_message(pair(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1)) | ~ intruder_message(X0_$$iProver_key_i_1) | ~ intruder_message(X1_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_21]) ).

cnf(c_36,plain,
( intruder_message(X0_$i) | ~ fresh_intruder_nonce(X0_$i) ),
inference(cnf_transformation,[],[f176]) ).

cnf(c_285,plain,
( intruder_message(X0_$$iProver_key_i_1) | ~ fresh_intruder_nonce(X0_$$iProver_key_$i_1) ), inference(subtyping,[status(esa)],[c_36]) ). cnf(c_24,plain, ( ~ party_of_protocol(X0_$i)
| ~ intruder_message(encrypt(X1_$i,X2_$i))
| intruder_message(X2_$i) | ~ intruder_holds(key(X2_$i,X0_$i)) ), inference(cnf_transformation,[],[f163]) ). cnf(c_295,plain, ( ~ party_of_protocol(X0_$$iProver_key_i_1) | ~ intruder_message(encrypt(X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | intruder_message(X2_$$iProver_key_$i_1) | ~ intruder_holds(key(X2_$$iProver_key_i_1,X0_$$iProver_key_$i_1)) ),
inference(subtyping,[status(esa)],[c_24]) ).

cnf(c_20,plain,
( ~ intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
| intruder_message(X0_$i) ), inference(cnf_transformation,[],[f156]) ). cnf(c_299,plain, ( ~ intruder_message(quadruple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1,X3_$$iProver_key_$i_1)) | intruder_message(X0_$$iProver_key_i_1) ), inference(subtyping,[status(esa)],[c_20]) ). cnf(c_19,plain, ( ~ intruder_message(quadruple(X0_i,X1_i,X2_i,X3_i)) | intruder_message(X1_i) ), inference(cnf_transformation,[],[f157]) ). cnf(c_300,plain, ( ~ intruder_message(quadruple(X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1,X2_$$iProver_key_$i_1,X3_$$iProver_key_i_1)) | intruder_message(X1_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_19]) ).

cnf(c_18,plain,
( ~ intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
| intruder_message(X2_$i) ), inference(cnf_transformation,[],[f158]) ). cnf(c_301,plain, ( ~ intruder_message(quadruple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1,X3_$$iProver_key_$i_1)) | intruder_message(X2_$$iProver_key_i_1) ), inference(subtyping,[status(esa)],[c_18]) ). cnf(c_17,plain, ( ~ intruder_message(quadruple(X0_i,X1_i,X2_i,X3_i)) | intruder_message(X3_i) ), inference(cnf_transformation,[],[f159]) ). cnf(c_302,plain, ( ~ intruder_message(quadruple(X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1,X2_$$iProver_key_$i_1,X3_$$iProver_key_i_1)) | intruder_message(X3_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_17]) ).

cnf(c_16,plain,
( ~ intruder_message(triple(X0_$i,X1_$i,X2_$i)) | intruder_message(X0_$i) ),
inference(cnf_transformation,[],[f153]) ).

cnf(c_303,plain,
( ~ intruder_message(triple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | intruder_message(X0_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_16]) ).

cnf(c_15,plain,
( ~ intruder_message(triple(X0_$i,X1_$i,X2_$i)) | intruder_message(X1_$i) ),
inference(cnf_transformation,[],[f154]) ).

cnf(c_304,plain,
( ~ intruder_message(triple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | intruder_message(X1_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_15]) ).

cnf(c_14,plain,
( ~ intruder_message(triple(X0_$i,X1_$i,X2_$i)) | intruder_message(X2_$i) ),
inference(cnf_transformation,[],[f155]) ).

cnf(c_305,plain,
( ~ intruder_message(triple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | intruder_message(X2_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_14]) ).

cnf(c_13,plain,
( ~ intruder_message(pair(X0_$i,X1_$i)) | intruder_message(X0_$i) ), inference(cnf_transformation,[],[f151]) ). cnf(c_306,plain, ( ~ intruder_message(pair(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1))
| intruder_message(X0_$$iProver_key_i_1) ), inference(subtyping,[status(esa)],[c_13]) ). cnf(c_12,plain, ( ~ intruder_message(pair(X0_i,X1_i)) | intruder_message(X1_i) ), inference(cnf_transformation,[],[f152]) ). cnf(c_307,plain, ( ~ intruder_message(pair(X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1)) | intruder_message(X1_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_12]) ).

cnf(c_11,plain,
( ~ message(sent(X0_$i,X1_$i,X2_$i)) | intruder_message(X2_$i) ),
inference(cnf_transformation,[],[f150]) ).

cnf(c_308,plain,
( ~ message(sent(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | intruder_message(X2_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_11]) ).

cnf(c_22,plain,
( intruder_message(triple(X0_$i,X1_$i,X2_$i)) | ~ intruder_message(X0_$i)
| ~ intruder_message(X1_$i) | ~ intruder_message(X2_$i) ),
inference(cnf_transformation,[],[f161]) ).

cnf(c_297,plain,
( intruder_message(triple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | ~ intruder_message(X0_$$iProver_key_$i_1)
| ~ intruder_message(X1_$$iProver_key_i_1) | ~ intruder_message(X2_$$iProver_key_$i_1) ), inference(subtyping,[status(esa)],[c_22]) ). cnf(c_23,plain, ( intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i)) | ~ intruder_message(X0_$i)
| ~ intruder_message(X1_$i) | ~ intruder_message(X2_$i)
| ~ intruder_message(X3_$i) ), inference(cnf_transformation,[],[f162]) ). cnf(c_296,plain, ( intruder_message(quadruple(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1,X3_$$iProver_key_$i_1)) | ~ intruder_message(X0_$$iProver_key_i_1) | ~ intruder_message(X1_$$iProver_key_$i_1)
| ~ intruder_message(X2_$$iProver_key_i_1) | ~ intruder_message(X3_$$iProver_key_$i_1) ), inference(subtyping,[status(esa)],[c_23]) ). cnf(c_27,plain, ( ~ party_of_protocol(X0_$i)
| intruder_message(encrypt(X1_$i,X2_$i))
| ~ intruder_message(X1_$i) | ~ intruder_holds(key(X2_$i,X0_$i)) ), inference(cnf_transformation,[],[f166]) ). cnf(c_292,plain, ( ~ party_of_protocol(X0_$$iProver_key_i_1) | intruder_message(encrypt(X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | ~ intruder_message(X1_$$iProver_key_$i_1) | ~ intruder_holds(key(X2_$$iProver_key_i_1,X0_$$iProver_key_$i_1)) ),
inference(subtyping,[status(esa)],[c_27]) ).

cnf(c_8,plain,
( t_holds(key(bt,b)) ),
inference(cnf_transformation,[],[f147]) ).

cnf(c_280,plain,
( t_holds(key(bt,b)) ),
inference(subtyping,[status(esa)],[c_8]) ).

cnf(c_7,plain,
( t_holds(key(at,a)) ),
inference(cnf_transformation,[],[f146]) ).

cnf(c_279,plain,
( t_holds(key(at,a)) ),
inference(subtyping,[status(esa)],[c_7]) ).

cnf(c_4,plain,
( party_of_protocol(b) ),
inference(cnf_transformation,[],[f143]) ).

cnf(c_277,plain,
( party_of_protocol(b) ),
inference(subtyping,[status(esa)],[c_4]) ).

cnf(c_0,plain,
( party_of_protocol(a) ),
inference(cnf_transformation,[],[f139]) ).

cnf(c_274,plain,
( party_of_protocol(a) ),
inference(subtyping,[status(esa)],[c_0]) ).

cnf(c_9,plain,
( party_of_protocol(t) ),
inference(cnf_transformation,[],[f148]) ).

cnf(c_281,plain,
( party_of_protocol(t) ),
inference(subtyping,[status(esa)],[c_9]) ).

cnf(c_5,plain,
( fresh_to_b(an_a_nonce) ),
inference(cnf_transformation,[],[f144]) ).

cnf(c_278,plain,
( fresh_to_b(an_a_nonce) ),
inference(subtyping,[status(esa)],[c_5]) ).

cnf(c_37,plain,
( fresh_to_b(X0_$i) | ~ fresh_intruder_nonce(X0_$i) ),
inference(cnf_transformation,[],[f175]) ).

cnf(c_284,plain,
( fresh_to_b(X0_$$iProver_key_i_1) | ~ fresh_intruder_nonce(X0_$$iProver_key_$i_1) ), inference(subtyping,[status(esa)],[c_37]) ). cnf(c_35,plain, ( fresh_intruder_nonce(generate_intruder_nonce(X0_$i))
| ~ fresh_intruder_nonce(X0_$i) ), inference(cnf_transformation,[],[f174]) ). cnf(c_286,plain, ( fresh_intruder_nonce(generate_intruder_nonce(X0_$$iProver_key_i_1)) | ~ fresh_intruder_nonce(X0_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_35]) ).

cnf(c_34,plain,
( fresh_intruder_nonce(an_intruder_nonce) ),
inference(cnf_transformation,[],[f173]) ).

cnf(c_283,plain,
( fresh_intruder_nonce(an_intruder_nonce) ),
inference(subtyping,[status(esa)],[c_34]) ).

cnf(c_2,plain,
( a_stored(pair(b,an_a_nonce)) ),
inference(cnf_transformation,[],[f141]) ).

cnf(c_276,plain,
( a_stored(pair(b,an_a_nonce)) ),
inference(subtyping,[status(esa)],[c_2]) ).

cnf(c_6,plain,
( message(sent(b,t,triple(b,generate_b_nonce(X0_$i),encrypt(triple(X1_$i,X0_$i,generate_expiration_time(X0_$i)),bt))))
| ~ message(sent(X1_$i,b,pair(X1_$i,X0_$i))) | ~ fresh_to_b(X0_$i) ),
inference(cnf_transformation,[],[f145]) ).

cnf(c_310,plain,
( message(sent(b,t,triple(b,generate_b_nonce(X0_$$iProver_key_i_1),encrypt(triple(X1_$$iProver_key_$i_1,X0_$$iProver_key_i_1,generate_expiration_time(X0_$$iProver_key_$i_1)),bt))))
| ~ message(sent(X1_$$iProver_key_i_1,b,pair(X1_$$iProver_key_$i_1,X0_$$iProver_key_i_1))) | ~ fresh_to_b(X0_$$iProver_key_$i_1) ),
inference(subtyping,[status(esa)],[c_6]) ).

cnf(c_25,plain,
( ~ party_of_protocol(X0_$i) | ~ party_of_protocol(X1_$i)
| message(sent(X0_$i,X1_$i,X2_$i)) | ~ intruder_message(X2_$i) ),
inference(cnf_transformation,[],[f164]) ).

cnf(c_294,plain,
( ~ party_of_protocol(X0_$$iProver_key_i_1) | ~ party_of_protocol(X1_$$iProver_key_$i_1) | message(sent(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1)) | ~ intruder_message(X2_$$iProver_key_$i_1) ), inference(subtyping,[status(esa)],[c_25]) ). cnf(c_1,plain, ( message(sent(a,b,pair(a,an_a_nonce))) ), inference(cnf_transformation,[],[f140]) ). cnf(c_275,plain, ( message(sent(a,b,pair(a,an_a_nonce))) ), inference(subtyping,[status(esa)],[c_1]) ). cnf(c_3,plain, ( message(sent(a,X0_$i,pair(X1_$i,encrypt(X2_$i,X3_$i)))) | ~ message(sent(t,a,triple(encrypt(quadruple(X0_$i,X4_$i,X3_$i,X5_$i),at),X1_$i,X2_$i))) | ~ a_stored(pair(X0_$i,X4_$i)) ), inference(cnf_transformation,[],[f142]) ). cnf(c_311,plain, ( message(sent(a,X0_$$iProver_key_i_1,pair(X1_$$iProver_key_$i_1,encrypt(X2_$$iProver_key_i_1,X3_$$iProver_key_$i_1)))) | ~ message(sent(t,a,triple(encrypt(quadruple(X0_$$iProver_key_i_1,X4_$$iProver_key_$i_1,X3_$$iProver_key_i_1,X5_$$iProver_key_$i_1),at),X1_$$iProver_key_i_1,X2_$$iProver_key_$i_1)))
| ~ a_stored(pair(X0_$$iProver_key_i_1,X4_$$iProver_key_$i_1)) ), inference(subtyping,[status(esa)],[c_3]) ). cnf(c_10,plain, ( message(sent(t,X0_$i,triple(encrypt(quadruple(X1_$i,X2_$i,generate_key(X2_$i),X3_$i),X4_$i),encrypt(triple(X0_$i,generate_key(X2_$i),X3_$i),X5_$i),X6_$i)))
| ~ message(sent(X1_$i,t,triple(X1_$i,X6_$i,encrypt(triple(X0_$i,X2_$i,X3_$i),X5_$i)))) | ~ t_holds(key(X5_$i,X1_$i)) | ~ t_holds(key(X4_$i,X0_$i)) | ~ a_nonce(X2_$i) ),
inference(cnf_transformation,[],[f149]) ).

cnf(c_309,plain,
( message(sent(t,X0_$$iProver_key_i_1,triple(encrypt(quadruple(X1_$$iProver_key_$i_1,X2_$$iProver_key_i_1,generate_key(X2_$$iProver_key_$i_1),X3_$$iProver_key_i_1),X4_$$iProver_key_$i_1),encrypt(triple(X0_$$iProver_key_i_1,generate_key(X2_$$iProver_key_$i_1),X3_$$iProver_key_i_1),X5_$$iProver_key_$i_1),X6_$$iProver_key_i_1))) | ~ message(sent(X1_$$iProver_key_$i_1,t,triple(X1_$$iProver_key_i_1,X6_$$iProver_key_$i_1,encrypt(triple(X0_$$iProver_key_i_1,X2_$$iProver_key_$i_1,X3_$$iProver_key_i_1),X5_$$iProver_key_$i_1)))) | ~ t_holds(key(X5_$$iProver_key_i_1,X1_$$iProver_key_$i_1))
| ~ t_holds(key(X4_$$iProver_key_i_1,X0_$$iProver_key_$i_1)) | ~ a_nonce(X2_$$iProver_key_i_1) ), inference(subtyping,[status(esa)],[c_10]) ). cnf(c_26,plain, ( ~ party_of_protocol(X0_i) | ~ intruder_message(X1_i) | intruder_holds(key(X1_i,X0_i)) ), inference(cnf_transformation,[],[f165]) ). cnf(c_293,plain, ( ~ party_of_protocol(X0_$$iProver_key_$i_1)
| ~ intruder_message(X1_$$iProver_key_i_1) | intruder_holds(key(X1_$$iProver_key_$i_1,X0_$$iProver_key_i_1)) ), inference(subtyping,[status(esa)],[c_26]) ). cnf(c_32,plain, ( ~ a_nonce(X0_i) | ~ a_key(X0_i) ), inference(cnf_transformation,[],[f171]) ). cnf(c_321,plain, ( ~ a_nonce(X0_$$iProver_key_$i_1) | ~ a_key(X0_$$iProver_key_i_1) ), inference(subtyping,[status(esa)],[c_32]) ). cnf(c_33,plain, ( a_key(generate_key(X0_i)) ), inference(cnf_transformation,[],[f172]) ). cnf(c_320,plain, ( a_key(generate_key(X0_$$iProver_key_$i_1)) ), inference(subtyping,[status(esa)],[c_33]) ). cnf(c_338,plain, ( ~ a_nonce(generate_key(X0_$$iProver_key_i_1)) ), inference(resolution,[status(thm)],[c_321,c_320]) ). cnf(c_30,plain, ( a_nonce(generate_b_nonce(X0_i)) ), inference(cnf_transformation,[],[f170]) ). cnf(c_319,plain, ( a_nonce(generate_b_nonce(X0_$$iProver_key_$i_1)) ),
inference(subtyping,[status(esa)],[c_30]) ).

cnf(c_31,plain,
( a_nonce(generate_expiration_time(X0_$i)) ), inference(cnf_transformation,[],[f169]) ). cnf(c_318,plain, ( a_nonce(generate_expiration_time(X0_$$iProver_key_i_1)) ), inference(subtyping,[status(esa)],[c_31]) ). cnf(c_28,plain, ( a_nonce(an_a_nonce) ), inference(cnf_transformation,[],[f167]) ). cnf(c_317,plain, ( a_nonce(an_a_nonce) ), inference(subtyping,[status(esa)],[c_28]) ). % SZS output end Saturation  ### Sample finite model for SWV017+1 %------ The model is defined over ground terms (initial term algebra). %------ Predicates are defined as (\forall x_1,..,x_n ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n)))) %------ where \phi is a formula over the term algebra. %------ If we have equality in the problem then it is also defined as a predicate above, %------ with "=" on the right-hand-side of the definition interpreted over the term algebra$$term_algebra_type %------ See help for --sat_out_model for different model outputs. %------ equality_sorted(X0,X1,X2) can be used in the place of usual "=" %------ where the first argument stands for the sort ($i in the unsorted case)

% SZS output start Model
%------ Negative definition of party_of_protocol
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1] : ( ~(party_of_protocol(X0_$$iProver_key_$i_1)) <=>$false
)
)
).

%------ Negative definition of message
fof(lit_def,axiom,
(! [X0_$$iProver_message_i_1] : ( ~(message(X0_$$iProver_message_$i_1)) <=>$false
)
)
).

%------ Negative definition of a_stored
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1] : ( ~(a_stored(X0_$$iProver_key_$i_1)) <=>$false
)
)
).

%------ Positive definition of fresh_to_b
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1] : ( fresh_to_b(X0_$$iProver_key_$i_1) <=>$true
)
)
).

%------ Negative definition of t_holds
fof(lit_def,axiom,
(! [X0_$$iProver_intruder_holds_i_1] : ( ~(t_holds(X0_$$iProver_intruder_holds_$i_1)) <=>$false
)
)
).

%------ Positive definition of a_nonce
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1] : ( a_nonce(X0_$$iProver_key_$i_1) <=> ( ( ( X0_$$iProver_key_i_1=$$iProver_Domain_$$iProver_key_i_1_1 ) ) ) ) ) ). %------ Positive definition of intruder_message fof(lit_def,axiom, (! [X0_$$iProver_key_$i_1] :
( intruder_message(X0_$$iProver_key_i_1) <=> true ) ) ). %------ Negative definition of intruder_holds fof(lit_def,axiom, (! [X0_$$iProver_intruder_holds_$i_1] : ( ~(intruder_holds(X0_$$iProver_intruder_holds_i_1)) <=> false ) ) ). %------ Positive definition of a_key fof(lit_def,axiom, (! [X0_$$iProver_key_$i_1] :
( a_key(X0_$$iProver_key_i_1) <=> ( ( ( X0_$$iProver_key_$i_1=$$iProver_Domain_$$iProver_key_$i_1_2 )
)

)
)
)
).

%------ Negative definition of fresh_intruder_nonce
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1] : ( ~(fresh_intruder_nonce(X0_$$iProver_key_$i_1)) <=>$false
)
)
).

%------ Positive definition of $$iProver_Flat_an_a_nonce fof(lit_def,axiom, (! [X0_$$iProver_key_$i_1] : ( $$iProver_Flat_an_a_nonce(X0_$$iProver_key_$i_1) <=>
(
(
( X0_$$iProver_key_i_1=$$iProver_Domain_$$iProver_key_i_1_1 ) ) ) ) ) ). %------ Positive definition of$$iProver_Flat_generate_b_nonce
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1] : ( $$iProver_Flat_generate_b_nonce(X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1) <=> ( ( ( X0_$$iProver_key_$i_1=$$iProver_Domain_$$iProver_key_$i_1_1 )
)

)
)
)
).

%------ Positive definition of $$iProver_Flat_generate_expiration_time fof(lit_def,axiom, (! [X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1] : ($$iProver_Flat_generate_expiration_time(X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1) <=>
(
(
( X0_$$iProver_key_i_1=$$iProver_Domain_$$iProver_key_i_1_1 ) ) ) ) ) ). %------ Positive definition of$$iProver_Flat_generate_key
fof(lit_def,axiom,
(! [X0_$$iProver_key_i_1,X1_$$iProver_key_$i_1] : ( $$iProver_Flat_generate_key(X0_$$iProver_key_$i_1,X1_$$iProver_key_i_1) <=> ( ( ( X0_$$iProver_key_$i_1=$$iProver_Domain_$$iProver_key_$i_1_2 )
)

)
)
)
).

% SZS output end Model


## MaLARea 0.5

Josef Urban
Radboud University Nijmegen, The Netherlands

### Sample solution for SEU140+2

# SZS status Theorem
# SZS output start CNFRefutation.
fof(c_0_0, axiom, (![X1]:![X2]:(disjoint(X1,X2)=>disjoint(X2,X1))), file('/Users/schulz/EPROVER/TPTP_5.4.0_FLAT/SEU140+2.p', symmetry_r1_xboole_0)).
fof(c_0_1, lemma, (![X1]:![X2]:(~((~(disjoint(X1,X2))&![X3]:~((in(X3,X1)&in(X3,X2)))))&~((?[X3]:(in(X3,X1)&in(X3,X2))&disjoint(X1,X2))))), file('/Users/schulz/EPROVER/TPTP_5.4.0_FLAT/SEU140+2.p', t3_xboole_0)).
fof(c_0_2, conjecture, (![X1]:![X2]:![X3]:((subset(X1,X2)&disjoint(X2,X3))=>disjoint(X1,X3))), file('/Users/schulz/EPROVER/TPTP_5.4.0_FLAT/SEU140+2.p', t63_xboole_1)).
fof(c_0_3, axiom, (![X1]:![X2]:(subset(X1,X2)<=>![X3]:(in(X3,X1)=>in(X3,X2)))), file('/Users/schulz/EPROVER/TPTP_5.4.0_FLAT/SEU140+2.p', d3_tarski)).
fof(c_0_4, axiom, (![X1]:![X2]:(disjoint(X1,X2)=>disjoint(X2,X1))), c_0_0).
fof(c_0_5, lemma, (![X1]:![X2]:(~((~disjoint(X1,X2)&![X3]:~((in(X3,X1)&in(X3,X2)))))&~((?[X3]:(in(X3,X1)&in(X3,X2))&disjoint(X1,X2))))), inference(fof_simplification,[status(thm)],[c_0_1])).
fof(c_0_6, negated_conjecture, (~(![X1]:![X2]:![X3]:((subset(X1,X2)&disjoint(X2,X3))=>disjoint(X1,X3)))), inference(assume_negation,[status(cth)],[c_0_2])).
fof(c_0_7, plain, (![X3]:![X4]:(~disjoint(X3,X4)|disjoint(X4,X3))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])).
fof(c_0_8, lemma, (![X4]:![X5]:![X7]:![X8]:![X9]:(((in(esk9_2(X4,X5),X4)|disjoint(X4,X5))&(in(esk9_2(X4,X5),X5)|disjoint(X4,X5)))&((~in(X9,X7)|~in(X9,X8))|~disjoint(X7,X8)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])])])).
fof(c_0_9, negated_conjecture, (((subset(esk11_0,esk12_0)&disjoint(esk12_0,esk13_0))&~disjoint(esk11_0,esk13_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])).
cnf(c_0_10,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), inference(split_conjunct,[status((null))],[c_0_7])).
cnf(c_0_11,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), inference(split_conjunct,[status((null))],[c_0_8])).
fof(c_0_12, axiom, (![X1]:![X2]:(subset(X1,X2)<=>![X3]:(in(X3,X1)=>in(X3,X2)))), c_0_3).
cnf(c_0_13,lemma,(~in(X3,X2)|~in(X3,X1)|~disjoint(X1,X2)), inference(split_conjunct,[status((null))],[c_0_8])).
cnf(c_0_14,negated_conjecture,(disjoint(esk12_0,esk13_0)), inference(split_conjunct,[status((null))],[c_0_9])).
cnf(c_0_15,negated_conjecture,(~disjoint(esk11_0,esk13_0)), inference(split_conjunct,[status((null))],[c_0_9])).
cnf(c_0_16,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), c_0_10).
cnf(c_0_17,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), c_0_11).
fof(c_0_18, plain, (![X4]:![X5]:![X6]:![X7]:![X8]:((~subset(X4,X5)|(~in(X6,X4)|in(X6,X5)))&((in(esk3_2(X7,X8),X7)|subset(X7,X8))&(~in(esk3_2(X7,X8),X8)|subset(X7,X8))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])])])])).
cnf(c_0_19,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), inference(split_conjunct,[status((null))],[c_0_8])).
cnf(c_0_20,lemma,(~disjoint(X1,X2)|~in(X3,X2)|~in(X3,X1)), c_0_13).
cnf(c_0_21,negated_conjecture,(disjoint(esk12_0,esk13_0)), c_0_14).
cnf(c_0_22,negated_conjecture,(~disjoint(esk11_0,esk13_0)), c_0_15).
cnf(c_0_23,plain,(disjoint(X1,X2)|~disjoint(X2,X1)), c_0_16).
cnf(c_0_24,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X1)), c_0_17).
cnf(c_0_25,plain,(in(X1,X2)|~in(X1,X3)|~subset(X3,X2)), inference(split_conjunct,[status((null))],[c_0_18])).
cnf(c_0_26,negated_conjecture,(subset(esk11_0,esk12_0)), inference(split_conjunct,[status((null))],[c_0_9])).
cnf(c_0_27,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), c_0_19).
cnf(c_0_28,lemma,(~disjoint(X1,X2)|~in(X3,X2)|~in(X3,X1)), c_0_20).
cnf(c_0_29,negated_conjecture,(disjoint(esk12_0,esk13_0)), c_0_21).
cnf(c_0_30,negated_conjecture,(~disjoint(esk11_0,esk13_0)), c_0_22).
cnf(c_0_31,lemma,(disjoint(X1,X2)|in(esk9_2(X2,X1),X2)), inference(spm,[status(thm)],[c_0_23, c_0_24, theory(equality)]])).
cnf(c_0_32,plain,(in(X1,X2)|~subset(X3,X2)|~in(X1,X3)), c_0_25).
cnf(c_0_33,negated_conjecture,(subset(esk11_0,esk12_0)), c_0_26).
cnf(c_0_34,lemma,(disjoint(X1,X2)|in(esk9_2(X1,X2),X2)), c_0_27).
cnf(c_0_35,negated_conjecture,(~in(X1,esk13_0)|~in(X1,esk12_0)), inference(spm,[status(thm)],[c_0_28, c_0_29, theory(equality)]])).
cnf(c_0_36,negated_conjecture,(in(esk9_2(esk13_0,esk11_0),esk13_0)), inference(spm,[status(thm)],[c_0_30, c_0_31, theory(equality)]])).
cnf(c_0_37,plain,(in(X1,X2)|~subset(X3,X2)|~in(X1,X3)), c_0_32).
cnf(c_0_38,negated_conjecture,(subset(esk11_0,esk12_0)), c_0_33).
cnf(c_0_39,lemma,(disjoint(X1,X2)|in(esk9_2(X2,X1),X1)), inference(spm,[status(thm)],[c_0_23, c_0_34, theory(equality)]])).
cnf(c_0_40,negated_conjecture,(~in(esk9_2(esk13_0,esk11_0),esk12_0)), inference(spm,[status(thm)],[c_0_35, c_0_36, theory(equality)]])).
cnf(c_0_41,negated_conjecture,(in(X1,esk12_0)|~in(X1,esk11_0)), inference(spm,[status(thm)],[c_0_37, c_0_38, theory(equality)]])).
cnf(c_0_42,negated_conjecture,(in(esk9_2(esk13_0,esk11_0),esk11_0)), inference(spm,[status(thm)],[c_0_30, c_0_39, theory(equality)]])).
cnf(c_0_43,negated_conjecture,($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41, theory(equality)]]), c_0_42, theory(equality)]]), theory(equality,[symmetry])]]), ['proof']). # SZS output end CNFRefutation.  ## Muscadet 4.3 Domonique Pastre University Paris Descartes, France ### Sample solution for SEU140+2 SZS status Theorem for SEU140+2.p SZS output start proof for SEU140+2.p * * * * * * * * * * * * * * * * * * * * * * * * in the following, N is the number of a (sub)theorem E is the current step or the step when a hypothesis or conclusion has been added or modified hyp(N,H,E) means that H is an hypothesis of (sub)theorem N concl(N,C,E) means that C is the conclusion of (sub)theorem N obj_ct(N,C) means that C is a created object or a given constant addhyp(N,H,E) means add H as a new hypothesis for N newconcl(N,C,E) means that the new conclusion of N is C (C replaces the precedent conclusion) a subtheorem N-i or N+i is a subtheorem of the (sub)theorem N N is proved if all N-i have been proved (&-node) or if one N+i have been proved (|-node) the initial theorem is numbered 0 * * * theorem to be proved ![A,B,C]: (subset(A,B)&disjoint(B,C)=>disjoint(A,C)) * * * proof : * * * * * * theoreme 0 * * * * * * *** newconcl(0,![A,B,C]: (subset(A,B)&disjoint(B,C)=>disjoint(A,C)),1) *** explanation : initial theorem ------------------------------------------------------- action ini create object(s) z3 z2 z1 *** newconcl(0,subset(z1,z2)&disjoint(z2,z3)=>disjoint(z1,z3),2) *** because concl((0,![A,B,C]: (subset(A,B)&disjoint(B,C)=>disjoint(A,C))),1) *** explanation : the universal variable(s) of the conclusion is(are) instantiated ------------------------------------------------------- rule ! *** addhyp(0,subset(z1,z2),3) *** addhyp(0,disjoint(z2,z3),3) *** newconcl(0,disjoint(z1,z3),3) *** because concl(0,subset(z1,z2)&disjoint(z2,z3)=>disjoint(z1,z3),2) *** explanation : to prove H=>C, assume H and prove C ------------------------------------------------------- rule => *** addhyp(0,set_intersection2(z2,z3)::empty_set,4) *** because hyp(0,disjoint(z2,z3),3) *** explanation : rule if hyp(A,disjoint(B,C),_)then addhyp(A,set_intersection2(B,C)::empty_set,_) built from the definition of disjoint (fof axiom:d7_xboole_0 ) ------------------------------------------------------- rule disjoint *** addhyp(0,set_difference(z1,z2)::empty_set,21) *** because hyp(0,subset(z1,z2),3),obj_ct(0,z1),obj_ct(0,z2) *** explanation : rule if (hyp(A,subset(B,C),_),obj_ct(A,B),obj_ct(A,C))then addhyp(A,set_difference(B,C)::empty_set,_) built from the axiom lemma:l32_xboole_1 ------------------------------------------------------- rule lemma:l32_xboole_1_1 *** newconcl(0,set_intersection2(z1,z3)::empty_set,109) *** because concl(0,disjoint(z1,z3),3) *** explanation : the conclusion disjoint(z1,z3) is replaced by its definition(fof axiom:d7_xboole_0 ) ------------------------------------------------------- rule def_concl_pred *** newconcl(0,seul(set_intersection2(z1,z3)::A,A=empty_set),110) *** because concl(0,set_intersection2(z1,z3)::empty_set,109) *** explanation : FX::Y is rewriten only(FX::Z, Z=Y) ------------------------------------------------------- rule concl2pts *** addhyp(0,set_intersection2(z1,z3)::z4,111),newconcl(0,z4=empty_set,111) *** because concl(0,seul(set_intersection2(z1,z3)::A,A=empty_set),110) *** explanation : creation of object z4 and of its definition ------------------------------------------------------- rule concl_only *** addhyp(0,set_intersection2(z3,z1)::z4,113) *** because hyp(0,set_intersection2(z1,z3)::z4,111),obj_ct(0,z1),obj_ct(0,z3) *** explanation : rule if (hyp(A,set_intersection2(B,C)::D,_),obj_ct(A,B),obj_ct(A,C))then addhyp(A,set_intersection2(C,B)::D,_) built from the axiom axiom:commutativity_k3_xboole_0 ------------------------------------------------------- rule axiom:commutativity_k3_xboole_0_1 *** newconcl(0,![A]: ~in(A,z4),114) *** because concl(0,z4=empty_set,111) *** explanation : sufficient condition (rule : axiom:d1_xboole_0_1 (fof axiom:d1_xboole_0 ) ------------------------------------------------------- rule axiom:d1_xboole_0_1_cs create object(s) z5 *** newconcl(0,~in(z5,z4),115) *** because concl((0,![A]: ~in(A,z4)),114) *** explanation : the universal variable(s) of the conclusion is(are) instantiated ------------------------------------------------------- rule ! *** addhyp(0,in(z5,z4),116),newconcl(0,false,116) *** because concl(0,~in(z5,z4),115) *** explanation : assume in(z5,z4) and search for a contradiction ------------------------------------------------------- rule concl_not *** addhyp(0,in(z5,z1),118) *** because hyp(0,set_intersection2(z1,z3)::z4,111),hyp(0,in(z5,z4),116),obj_ct(0,z5) *** explanation : rule if (hyp(A,set_intersection2(D,_)::B,_),hyp(A,in(C,B),_),obj_ct(A,C))then addhyp(A,in(C,D),_) built from the definition of set_intersection2 (fof axiom:d3_xboole_0 ) ------------------------------------------------------- rule set_intersection2_ *** addhyp(0,in(z5,z2),119) *** because hyp(0,subset(z1,z2),3),hyp(0,in(z5,z1),118),obj_ct(0,z5) *** explanation : rule if (hyp(A,subset(B,D),_),hyp(A,in(C,B),_),obj_ct(A,C))then addhyp(A,in(C,D),_) built from the definition of subset (fof axiom:d3_tarski ) ------------------------------------------------------- rule subset *** addhyp(0,in(z5,z3),120) *** because hyp(0,set_intersection2(z3,z1)::z4,113),hyp(0,in(z5,z4),116),obj_ct(0,z5) *** explanation : rule if (hyp(A,set_intersection2(D,_)::B,_),hyp(A,in(C,B),_),obj_ct(A,C))then addhyp(A,in(C,D),_) built from the definition of set_intersection2 (fof axiom:d3_xboole_0 ) ------------------------------------------------------- rule set_intersection2_ *** addhyp(0,in(z5,empty_set),121) *** because hyp(0,set_intersection2(z2,z3)::empty_set,4),hyp(0,in(z5,z2),119),hyp(0,in(z5,z3),120),obj_ct(0,z5) *** explanation : rule if (hyp(A,set_intersection2(B,D)::E,_),hyp(A,in(C,B),_),hyp(A,in(C,D),_),obj_ct(A,C))then addhyp(A,in(C,E),_) built from the definition of set_intersection2 (fof axiom:d3_xboole_0 ) ------------------------------------------------------- rule set_intersection2_2 *** addhyp(0,false,122) *** because hyp(0,set_difference(z1,z2)::empty_set,21),hyp(0,in(z5,empty_set),121),hyp(0,in(z5,z2),119),obj_ct(0,z5) *** explanation : rule if (hyp(A,set_difference(_,D)::B,_),hyp(A,in(C,B),_),hyp(A,in(C,D),_),obj_ct(A,C))then addhyp(A,false,_) built from the definition of set_difference (fof axiom:d4_xboole_0 ) ------------------------------------------------------- rule set_difference1 *** newconcl(0,true,123) *** because hyp(0,false,122),concl(0,false,116) *** explanation : the conclusion false to be proved is a hypothesis ------------------------------------------------------- rule stop_hyp_concl then the initial theorem is proved * * * * * * * * * * * * * * * * * * * * * * * * SZS output end proof for SEU140+2.p  ## Nitrox 2013 Jasmin C. Blanchette1, Emina Torlak2 1Technische Universität München, Germany, 2University of California, USA The domain elements of a model are of the form iN. Function mappings are provided for all tuples of domain elements. Predicate mappings are listed for the true cases. ### Sample solution for NLP042+1 % SZS status CounterSatisfiable % SZS output start FiniteModel Nitpick found a counterexample for card TPTP_Interpret.ind = 4: Skolem constants: U = i1 V = i2 W = i3 X = i4 Y = i1 Constants: bnd_abstraction = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_act = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_actual_world = (%x. _)(i1 := True, i2 := False, i3 := True, i4 := False) bnd_agent = (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i2 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i3 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i4 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False))) bnd_animate = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_beverage = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_entity = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_event = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_eventuality = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_existent = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_female = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_food = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_forename = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_general = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_human = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_human_person = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_impartial = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_living = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_mia_forename = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_nonexistent = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_nonhuman = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_nonliving = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_nonreflexive = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_object = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_of = (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i2 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i3 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i4 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False))) bnd_order = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_organism = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_past = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_patient = (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := True, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i2 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i3 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False)), i4 := (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _) (i1 := False, i2 := False, i3 := False, i4 := False))) bnd_relation = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_relname = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_shake_beverage = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_singleton = (%x. _) (i1 := (%x. _)(i1 := True, i2 := True, i3 := True, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_specific = (%x. _) (i1 := (%x. _)(i1 := True, i2 := True, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_substance_matter = (%x. _) (i1 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) bnd_thing = (%x. _) (i1 := (%x. _)(i1 := True, i2 := True, i3 := True, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_unisex = (%x. _) (i1 := (%x. _)(i1 := True, i2 := False, i3 := True, i4 := True), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := True, i4 := False)) bnd_woman = (%x. _) (i1 := (%x. _)(i1 := False, i2 := True, i3 := False, i4 := False), i2 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i3 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False), i4 := (%x. _)(i1 := False, i2 := False, i3 := False, i4 := False)) % SZS output end FiniteModel  ### Sample solution for SWV010+1 % SZS status Satisfiable % SZS output start FiniteModel Nitpick found a model for card TPTP_Interpret.ind = 2: Constants: bnd_a = i1 bnd_a_holds = (%x. _)(i1 := True, i2 := True) bnd_a_key = (%x. _)(i1 := True, i2 := False) bnd_a_nonce = (%x. _)(i1 := False, i2 := True) bnd_a_stored = (%x. _)(i1 := False, i2 := True) bnd_an_a_nonce = i2 bnd_an_intruder_nonce = i1 bnd_at = i1 bnd_b = i1 bnd_b_holds = (%x. _)(i1 := True, i2 := True) bnd_b_stored = (%x. _)(i1 := True, i2 := True) bnd_bt = i1 bnd_encrypt = (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1)) bnd_fresh_intruder_nonce = (%x. _)(i1 := True, i2 := False) bnd_fresh_to_b = (%x. _)(i1 := True, i2 := True) bnd_generate_b_nonce = (%x. _)(i1 := i2, i2 := i2) bnd_generate_expiration_time = (%x. _)(i1 := i2, i2 := i2) bnd_generate_intruder_nonce = (%x. _)(i1 := i1, i2 := i1) bnd_generate_key = (%x. _)(i1 := i1, i2 := i1) bnd_intruder_holds = (%x. _)(i1 := True, i2 := True) bnd_intruder_message = (%x. _)(i1 := True, i2 := True) bnd_key = (%x. _) (i1 := (%x. _)(i1 := i2, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1)) bnd_message = (%x. _)(i1 := True, i2 := True) bnd_pair = (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i2), i2 := (%x. _)(i1 := i1, i2 := i1)) bnd_party_of_protocol = (%x. _)(i1 := True, i2 := True) bnd_quadruple = (%x. _) (i1 := (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1)), i2 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1))), i2 := (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1)), i2 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i2)))) bnd_sent = (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1)), i2 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i1))) bnd_t = i1 bnd_t_holds = (%x. _)(i1 := False, i2 := True) bnd_triple = (%x. _) (i1 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i1, i2 := i2)), i2 := (%x. _) (i1 := (%x. _)(i1 := i1, i2 := i1), i2 := (%x. _)(i1 := i2, i2 := i1))) % SZS output end FiniteModel  ## Paradox 3.0 and 4.0 Koen Claessen Chalmers University of Technology, Sweden ### Sample solution for MGT019+2 % domain size is 1 disbanding_rate(!1,!1) = !1 efficient_producers = !1 environment(!1) <=>$true
first_movers = !1
founding_rate(!1,!1) = !1
greater(!1,!1) <=> $false greater_or_equal(!1,!1) <=>$true
growth_rate(!1,!1) = !1
in_environment(!1,!1) <=> $true stable(!1) <=>$true


## TEMPLAR::leanCoP 0.8

Mario Frank, Jens Otten
University of Potsdam, Germany

### Sample solution for SEU140+2

% SZS status Theorem for /home/eladrion/Daten/Uni/Projekte/ATP/TEMPLAR/build/SEU140+2.p
% SZS output start Proof for SEU140+2

% /tmp/TEMPLAR_SEU140+2.p.depth0 is a Theorem
% Start of proof for /tmp/TEMPLAR_SEU140+2.p.depth0
%-----------------------------------------------------
fof(t63_xboole_1,conjecture,![_G4877,_G4880,_G4883]: (subset(_G4877,_G4880)&disjoint(_G4880,_G4883)=>disjoint(_G4877,_G4883)),file('/tmp/TEMPLAR_SEU140+2.p.depth0',t63_xboole_1)).
fof(d3_tarski,axiom,![_G4952,_G4955]: (subset(_G4952,_G4955)<=>![_G4961]: (in(_G4961,_G4952)=>in(_G4961,_G4955))),file('/tmp/TEMPLAR_SEU140+2.p.depth0',d3_tarski)).
fof(t3_xboole_0,lemma,![_G5014,_G5017]: (~ (~disjoint(_G5014,_G5017)&![_G5025]: ~ (in(_G5025,_G5014)&in(_G5025,_G5017)))& ~ (?[_G5025]: (in(_G5025,_G5014)&in(_G5025,_G5017))&disjoint(_G5014,_G5017))),file('/tmp/TEMPLAR_SEU140+2.p.depth0',t3_xboole_0)).

cnf(1,plain,[-subset(4^[],5^[])],clausify(t63_xboole_1)).
cnf(2,plain,[-disjoint(5^[],6^[])],clausify(t63_xboole_1)).
cnf(3,plain,[disjoint(4^[],6^[])],clausify(t63_xboole_1)).
cnf(4,plain,[subset(_G180,_G181),in(_G185,_G180),-in(_G185,_G181)],clausify(d3_tarski)).
cnf(5,plain,[-disjoint(_G602,_G603),-in(3^[_G603,_G602],_G602)],clausify(t3_xboole_0)).
cnf(6,plain,[-disjoint(_G602,_G603),-in(3^[_G603,_G602],_G603)],clausify(t3_xboole_0)).
cnf(7,plain,[disjoint(_G602,_G603),in(_G607,_G602),in(_G607,_G603)],clausify(t3_xboole_0)).

cnf('1',plain,[disjoint(5^[],6^[]),in(3^[6^[],4^[]],5^[]),in(3^[6^[],4^[]],6^[])],start(7,bind([[_G602,_G607,_G603],[5^[],3^[6^[],4^[]],6^[]]]))).
cnf('1.1',plain,[-disjoint(5^[],6^[])],extension(2)).
cnf('1.2',plain,[-in(3^[6^[],4^[]],5^[]),subset(4^[],5^[]),in(3^[6^[],4^[]],4^[])],extension(4,bind([[_G181,_G185,_G180],[5^[],3^[6^[],4^[]],4^[]]]))).
cnf('1.2.1',plain,[-subset(4^[],5^[])],extension(1)).
cnf('1.2.2',plain,[-in(3^[6^[],4^[]],4^[]),-disjoint(4^[],6^[])],extension(5,bind([[_G602,_G603],[4^[],6^[]]]))).
cnf('1.2.2.1',plain,[disjoint(4^[],6^[])],extension(3)).
cnf('1.3',plain,[-in(3^[6^[],4^[]],6^[]),-disjoint(4^[],6^[])],extension(6,bind([[_G602,_G603],[4^[],6^[]]]))).
cnf('1.3.1',plain,[disjoint(4^[],6^[])],extension(3)).
%-----------------------------------------------------
% End of proof for /tmp/TEMPLAR_SEU140+2.p.depth0

% SZS output end Proof for SEU140+2


## Vampire 2.6

Krystof Hoder, Andrei Voronkov
University of Manchester, England

### Sample solution for SEU140+2

% SZS output start Proof for SEU140+2
fof(f1738,plain,(
$false), inference(subsumption_resolution,[],[f1737,f136])). fof(f136,plain,( ~disjoint(sK0,sK2)), inference(cnf_transformation,[],[f104])). fof(f104,plain,( subset(sK0,sK1) & disjoint(sK1,sK2) & ~disjoint(sK0,sK2)), inference(skolemisation,[status(esa)],[f76])). fof(f76,plain,( ? [X0,X1,X2] : (subset(X0,X1) & disjoint(X1,X2) & ~disjoint(X0,X2))), inference(flattening,[],[f75])). fof(f75,plain,( ? [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) & ~disjoint(X0,X2))), inference(ennf_transformation,[],[f52])). fof(f52,negated_conjecture,( ~! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))), inference(negated_conjecture,[],[f51])). fof(f51,conjecture,( ! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))), file('Problems/SEU/SEU140+2.p',t63_xboole_1)). fof(f1737,plain,( disjoint(sK0,sK2)), inference(duplicate_literal_removal,[],[f1736])). fof(f1736,plain,( disjoint(sK0,sK2) | disjoint(sK0,sK2)), inference(resolution,[],[f1707,f378])). fof(f378,plain,( ( ! [X1] : (~in(sK4(sK2,X1),sK1) | disjoint(X1,sK2)) )), inference(resolution,[],[f372,f148])). fof(f148,plain,( ( ! [X0,X1] : (in(sK4(X1,X0),X1) | disjoint(X0,X1)) )), inference(cnf_transformation,[],[f106])). fof(f106,plain,( ! [X0,X1] : ((disjoint(X0,X1) | (in(sK4(X1,X0),X0) & in(sK4(X1,X0),X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))), inference(skolemisation,[status(esa)],[f79])). fof(f79,plain,( ! [X0,X1] : ((disjoint(X0,X1) | ? [X3] : (in(X3,X0) & in(X3,X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))), inference(ennf_transformation,[],[f61])). fof(f61,plain,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), inference(flattening,[],[f60])). fof(f60,plain,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), inference(rectify,[],[f43])). fof(f43,axiom,( ! [X0,X1] : (~(~disjoint(X0,X1) & ! [X2] : ~(in(X2,X0) & in(X2,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))), file('Problems/SEU/SEU140+2.p',t3_xboole_0)). fof(f372,plain,( ( ! [X0] : (~in(X0,sK2) | ~in(X0,sK1)) )), inference(resolution,[],[f149,f135])). fof(f135,plain,( disjoint(sK1,sK2)), inference(cnf_transformation,[],[f104])). fof(f149,plain,( ( ! [X2,X0,X1] : (~disjoint(X0,X1) | ~in(X2,X1) | ~in(X2,X0)) )), inference(cnf_transformation,[],[f106])). fof(f1707,plain,( ( ! [X0] : (in(sK4(X0,sK0),sK1) | disjoint(sK0,X0)) )), inference(resolution,[],[f1706,f147])). fof(f147,plain,( ( ! [X0,X1] : (in(sK4(X1,X0),X0) | disjoint(X0,X1)) )), inference(cnf_transformation,[],[f106])). fof(f1706,plain,( ( ! [X78] : (~in(X78,sK0) | in(X78,sK1)) )), inference(resolution,[],[f1661,f134])). fof(f134,plain,( subset(sK0,sK1)), inference(cnf_transformation,[],[f104])). fof(f1661,plain,( ( ! [X6,X7,X5] : (~subset(X5,X6) | in(X7,X6) | ~in(X7,X5)) )), inference(superposition,[],[f236,f218])). fof(f218,plain,( ( ! [X0,X1] : (set_difference(X0,set_difference(X0,X1)) = X0 | ~subset(X0,X1)) )), inference(definition_unfolding,[],[f150,f144])). fof(f144,plain,( ( ! [X0,X1] : (set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))) )), inference(cnf_transformation,[],[f47])). fof(f47,axiom,( ! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))), file('Problems/SEU/SEU140+2.p',t48_xboole_1)). fof(f150,plain,( ( ! [X0,X1] : (set_intersection2(X0,X1) = X0 | ~subset(X0,X1)) )), inference(cnf_transformation,[],[f80])). fof(f80,plain,( ! [X0,X1] : (~subset(X0,X1) | set_intersection2(X0,X1) = X0)), inference(ennf_transformation,[],[f34])). fof(f34,axiom,( ! [X0,X1] : (subset(X0,X1) => set_intersection2(X0,X1) = X0)), file('Problems/SEU/SEU140+2.p',t28_xboole_1)). fof(f236,plain,( ( ! [X4,X0,X1] : (~in(X4,set_difference(X0,set_difference(X0,X1))) | in(X4,X1)) )), inference(equality_resolution,[],[f230])). fof(f230,plain,( ( ! [X4,X2,X0,X1] : (in(X4,X1) | ~in(X4,X2) | set_difference(X0,set_difference(X0,X1)) != X2) )), inference(definition_unfolding,[],[f196,f144])). fof(f196,plain,( ( ! [X4,X2,X0,X1] : (in(X4,X1) | ~in(X4,X2) | set_intersection2(X0,X1) != X2) )), inference(cnf_transformation,[],[f123])). fof(f123,plain,( ! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (((in(sK8(X2,X1,X0),X2) | (in(sK8(X2,X1,X0),X0) & in(sK8(X2,X1,X0),X1))) & (~in(sK8(X2,X1,X0),X2) | ~in(sK8(X2,X1,X0),X0) | ~in(sK8(X2,X1,X0),X1))) | set_intersection2(X0,X1) = X2))), inference(skolemisation,[status(esa)],[f122])). fof(f122,plain,( ! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))), inference(rectify,[],[f121])). fof(f121,plain,( ! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X0) | ~in(X3,X1) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))), inference(flattening,[],[f120])). fof(f120,plain,( ! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & ((~in(X3,X0) | ~in(X3,X1)) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | (~in(X3,X0) | ~in(X3,X1)))) | set_intersection2(X0,X1) = X2))), inference(nnf_transformation,[],[f9])). fof(f9,axiom,( ! [X0,X1,X2] : (set_intersection2(X0,X1) = X2 <=> ! [X3] : (in(X3,X2) <=> (in(X3,X0) & in(X3,X1))))), file('Problems/SEU/SEU140+2.p',d3_xboole_0)). % SZS output end Proof for SEU140+2  ## Vampire 3.0 Andrei Voronkov University of Manchester, England ### Sample solution for SEU140+2 % SZS output start Proof for SEU140+2 fof(f1738,plain,($false),
inference(subsumption_resolution,[],[f1737,f136])).
fof(f136,plain,(
~disjoint(sK0,sK2)),
inference(cnf_transformation,[],[f104])).
fof(f104,plain,(
subset(sK0,sK1) & disjoint(sK1,sK2) & ~disjoint(sK0,sK2)),
inference(skolemisation,[status(esa)],[f76])).
fof(f76,plain,(
? [X0,X1,X2] : (subset(X0,X1) & disjoint(X1,X2) & ~disjoint(X0,X2))),
inference(flattening,[],[f75])).
fof(f75,plain,(
? [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) & ~disjoint(X0,X2))),
inference(ennf_transformation,[],[f52])).
fof(f52,negated_conjecture,(
~! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
inference(negated_conjecture,[],[f51])).
fof(f51,conjecture,(
! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
file('Problems/SEU/SEU140+2.p',t63_xboole_1)).
fof(f1737,plain,(
disjoint(sK0,sK2)),
inference(duplicate_literal_removal,[],[f1736])).
fof(f1736,plain,(
disjoint(sK0,sK2) | disjoint(sK0,sK2)),
inference(resolution,[],[f1707,f378])).
fof(f378,plain,(
( ! [X1] : (~in(sK4(sK2,X1),sK1) | disjoint(X1,sK2)) )),
inference(resolution,[],[f372,f148])).
fof(f148,plain,(
( ! [X0,X1] : (in(sK4(X1,X0),X1) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f106])).
fof(f106,plain,(
! [X0,X1] : ((disjoint(X0,X1) | (in(sK4(X1,X0),X0) & in(sK4(X1,X0),X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(skolemisation,[status(esa)],[f79])).
fof(f79,plain,(
! [X0,X1] : ((disjoint(X0,X1) | ? [X3] : (in(X3,X0) & in(X3,X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(ennf_transformation,[],[f61])).
fof(f61,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(flattening,[],[f60])).
fof(f60,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(rectify,[],[f43])).
fof(f43,axiom,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X2] : ~(in(X2,X0) & in(X2,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
file('Problems/SEU/SEU140+2.p',t3_xboole_0)).
fof(f372,plain,(
( ! [X0] : (~in(X0,sK2) | ~in(X0,sK1)) )),
inference(resolution,[],[f149,f135])).
fof(f135,plain,(
disjoint(sK1,sK2)),
inference(cnf_transformation,[],[f104])).
fof(f149,plain,(
( ! [X2,X0,X1] : (~disjoint(X0,X1) | ~in(X2,X1) | ~in(X2,X0)) )),
inference(cnf_transformation,[],[f106])).
fof(f1707,plain,(
( ! [X0] : (in(sK4(X0,sK0),sK1) | disjoint(sK0,X0)) )),
inference(resolution,[],[f1706,f147])).
fof(f147,plain,(
( ! [X0,X1] : (in(sK4(X1,X0),X0) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f106])).
fof(f1706,plain,(
( ! [X78] : (~in(X78,sK0) | in(X78,sK1)) )),
inference(resolution,[],[f1661,f134])).
fof(f134,plain,(
subset(sK0,sK1)),
inference(cnf_transformation,[],[f104])).
fof(f1661,plain,(
( ! [X6,X7,X5] : (~subset(X5,X6) | in(X7,X6) | ~in(X7,X5)) )),
inference(superposition,[],[f236,f218])).
fof(f218,plain,(
( ! [X0,X1] : (set_difference(X0,set_difference(X0,X1)) = X0 | ~subset(X0,X1)) )),
inference(definition_unfolding,[],[f150,f144])).
fof(f144,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))) )),
inference(cnf_transformation,[],[f47])).
fof(f47,axiom,(
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))),
file('Problems/SEU/SEU140+2.p',t48_xboole_1)).
fof(f150,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = X0 | ~subset(X0,X1)) )),
inference(cnf_transformation,[],[f80])).
fof(f80,plain,(
! [X0,X1] : (~subset(X0,X1) | set_intersection2(X0,X1) = X0)),
inference(ennf_transformation,[],[f34])).
fof(f34,axiom,(
! [X0,X1] : (subset(X0,X1) => set_intersection2(X0,X1) = X0)),
file('Problems/SEU/SEU140+2.p',t28_xboole_1)).
fof(f236,plain,(
( ! [X4,X0,X1] : (~in(X4,set_difference(X0,set_difference(X0,X1))) | in(X4,X1)) )),
inference(equality_resolution,[],[f230])).
fof(f230,plain,(
( ! [X4,X2,X0,X1] : (in(X4,X1) | ~in(X4,X2) | set_difference(X0,set_difference(X0,X1)) != X2) )),
inference(definition_unfolding,[],[f196,f144])).
fof(f196,plain,(
( ! [X4,X2,X0,X1] : (in(X4,X1) | ~in(X4,X2) | set_intersection2(X0,X1) != X2) )),
inference(cnf_transformation,[],[f123])).
fof(f123,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (((in(sK8(X2,X1,X0),X2) | (in(sK8(X2,X1,X0),X0) & in(sK8(X2,X1,X0),X1))) & (~in(sK8(X2,X1,X0),X2) | ~in(sK8(X2,X1,X0),X0) | ~in(sK8(X2,X1,X0),X1))) | set_intersection2(X0,X1) = X2))),
inference(skolemisation,[status(esa)],[f122])).
fof(f122,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))),
inference(rectify,[],[f121])).
fof(f121,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X0) | ~in(X3,X1) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))),
inference(flattening,[],[f120])).
fof(f120,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & ((~in(X3,X0) | ~in(X3,X1)) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | (~in(X3,X0) | ~in(X3,X1)))) | set_intersection2(X0,X1) = X2))),
inference(nnf_transformation,[],[f9])).
fof(f9,axiom,(
! [X0,X1,X2] : (set_intersection2(X0,X1) = X2 <=> ! [X3] : (in(X3,X2) <=> (in(X3,X0) & in(X3,X1))))),
file('Problems/SEU/SEU140+2.p',d3_xboole_0)).
% SZS output end Proof for SEU140+2


### Sample solution for NLP042+1

% SZS output start FiniteModel for NLP042+1
fof(model1,interpretation_domain,
! [X] : ( X = "sK4" | X = "sK3" | X = "sK2" | X = "sK1" | X = "sK0" ) ).
fof(model2,interpretation_terms,
( sK0 = "sK0" & sK1 = "sK1" & sK2 = "sK2" & sK3 = "sK3" & sK4 = "sK4") ).
fof(model3,interpretation_atoms,
( ~woman("sK0","sK0") &
~woman("sK0","sK2") &
~woman("sK0","sK3") &
~woman("sK0","sK4") &
~woman("sK1","sK0") &
~woman("sK1","sK1") &
~woman("sK1","sK2") &
~woman("sK1","sK3") &
~woman("sK1","sK4") &
~woman("sK2","sK0") &
~woman("sK2","sK1") &
~woman("sK2","sK2") &
woman("sK0","sK1") &
~woman("sK4","sK4") &
~woman("sK4","sK3") &
~woman("sK4","sK2") &
~woman("sK4","sK1") &
~woman("sK4","sK0") &
~woman("sK3","sK4") &
~woman("sK3","sK3") &
~woman("sK3","sK2") &
~woman("sK3","sK1") &
~woman("sK3","sK0") &
~woman("sK2","sK4") &
~woman("sK2","sK3") &
~female("sK2","sK2") &
~female("sK2","sK1") &
~female("sK2","sK0") &
~female("sK1","sK4") &
~female("sK1","sK3") &
~female("sK1","sK2") &
~female("sK1","sK1") &
~female("sK1","sK0") &
~female("sK0","sK4") &
~female("sK0","sK3") &
~female("sK0","sK2") &
~female("sK0","sK0") &
female("sK0","sK1") &
~female("sK4","sK4") &
~female("sK4","sK3") &
~female("sK4","sK2") &
~female("sK4","sK1") &
~female("sK4","sK0") &
~female("sK3","sK4") &
~female("sK3","sK3") &
~female("sK3","sK2") &
~female("sK3","sK1") &
~female("sK3","sK0") &
~female("sK2","sK4") &
~female("sK2","sK3") &
~human_person("sK2","sK2") &
~human_person("sK2","sK1") &
~human_person("sK2","sK0") &
~human_person("sK1","sK4") &
~human_person("sK1","sK3") &
~human_person("sK1","sK2") &
~human_person("sK1","sK1") &
~human_person("sK1","sK0") &
~human_person("sK0","sK4") &
~human_person("sK0","sK3") &
~human_person("sK0","sK2") &
~human_person("sK0","sK0") &
human_person("sK0","sK1") &
~human_person("sK4","sK4") &
~human_person("sK4","sK3") &
~human_person("sK4","sK2") &
~human_person("sK4","sK1") &
~human_person("sK4","sK0") &
~human_person("sK3","sK4") &
~human_person("sK3","sK3") &
~human_person("sK3","sK2") &
~human_person("sK3","sK1") &
~human_person("sK3","sK0") &
~human_person("sK2","sK4") &
~human_person("sK2","sK3") &
~animate("sK2","sK2") &
~animate("sK2","sK1") &
~animate("sK2","sK0") &
~animate("sK1","sK4") &
~animate("sK1","sK3") &
~animate("sK1","sK2") &
~animate("sK1","sK1") &
~animate("sK1","sK0") &
~animate("sK0","sK4") &
~animate("sK0","sK3") &
~animate("sK0","sK2") &
~animate("sK0","sK0") &
animate("sK0","sK1") &
~animate("sK4","sK4") &
~animate("sK4","sK3") &
~animate("sK4","sK2") &
~animate("sK4","sK1") &
~animate("sK4","sK0") &
~animate("sK3","sK4") &
~animate("sK3","sK3") &
~animate("sK3","sK2") &
~animate("sK3","sK1") &
~animate("sK3","sK0") &
~animate("sK2","sK4") &
~animate("sK2","sK3") &
~human("sK3","sK4") &
~human("sK3","sK3") &
~human("sK3","sK1") &
~human("sK3","sK0") &
~human("sK2","sK4") &
~human("sK2","sK3") &
~human("sK2","sK1") &
~human("sK2","sK0") &
~human("sK1","sK4") &
~human("sK1","sK3") &
~human("sK1","sK1") &
~human("sK1","sK0") &
human("sK0","sK1") &
~human("sK0","sK2") &
~human("sK4","sK2") &
~human("sK3","sK2") &
~human("sK2","sK2") &
~human("sK1","sK2") &
~human("sK0","sK4") &
~human("sK0","sK3") &
~human("sK0","sK0") &
~human("sK4","sK4") &
~human("sK4","sK3") &
~human("sK4","sK1") &
~human("sK4","sK0") &
~organism("sK3","sK4") &
~organism("sK3","sK3") &
~organism("sK3","sK1") &
~organism("sK3","sK0") &
~organism("sK2","sK4") &
~organism("sK2","sK3") &
~organism("sK2","sK1") &
~organism("sK2","sK0") &
~organism("sK1","sK4") &
~organism("sK1","sK3") &
~organism("sK1","sK1") &
~organism("sK1","sK0") &
organism("sK0","sK1") &
~organism("sK0","sK2") &
~organism("sK0","sK4") &
~organism("sK4","sK2") &
~organism("sK3","sK2") &
~organism("sK2","sK2") &
~organism("sK1","sK2") &
~organism("sK0","sK3") &
~organism("sK0","sK0") &
~organism("sK4","sK4") &
~organism("sK4","sK3") &
~organism("sK4","sK1") &
~organism("sK4","sK0") &
~living("sK2","sK2") &
~living("sK2","sK1") &
~living("sK2","sK0") &
~living("sK1","sK4") &
~living("sK1","sK3") &
~living("sK1","sK2") &
~living("sK1","sK1") &
~living("sK1","sK0") &
~living("sK0","sK4") &
~living("sK0","sK3") &
~living("sK0","sK2") &
~living("sK0","sK0") &
living("sK0","sK1") &
~living("sK4","sK4") &
~living("sK4","sK3") &
~living("sK4","sK2") &
~living("sK4","sK1") &
~living("sK4","sK0") &
~living("sK3","sK4") &
~living("sK3","sK3") &
~living("sK3","sK2") &
~living("sK3","sK1") &
~living("sK3","sK0") &
~living("sK2","sK4") &
~living("sK2","sK3") &
impartial("sK2","sK2") &
impartial("sK2","sK1") &
impartial("sK2","sK0") &
impartial("sK1","sK4") &
impartial("sK1","sK3") &
impartial("sK1","sK2") &
impartial("sK1","sK1") &
impartial("sK1","sK0") &
impartial("sK0","sK4") &
impartial("sK0","sK3") &
impartial("sK0","sK2") &
impartial("sK0","sK0") &
impartial("sK0","sK1") &
impartial("sK4","sK4") &
impartial("sK4","sK3") &
impartial("sK4","sK2") &
impartial("sK4","sK1") &
impartial("sK4","sK0") &
impartial("sK3","sK4") &
impartial("sK3","sK3") &
impartial("sK3","sK2") &
impartial("sK3","sK1") &
impartial("sK3","sK0") &
impartial("sK2","sK4") &
impartial("sK2","sK3") &
entity("sK3","sK4") &
entity("sK3","sK3") &
entity("sK3","sK1") &
entity("sK3","sK0") &
entity("sK2","sK4") &
entity("sK2","sK3") &
entity("sK2","sK1") &
entity("sK2","sK0") &
entity("sK1","sK4") &
entity("sK1","sK3") &
entity("sK1","sK1") &
entity("sK1","sK0") &
entity("sK0","sK1") &
~entity("sK0","sK2") &
~entity("sK0","sK4") &
entity("sK0","sK3") &
~entity("sK0","sK0") &
~entity("sK4","sK2") &
~entity("sK3","sK2") &
~entity("sK2","sK2") &
~entity("sK1","sK2") &
entity("sK4","sK4") &
entity("sK4","sK3") &
entity("sK4","sK1") &
entity("sK4","sK0") &
~mia_forename("sK2","sK2") &
~mia_forename("sK2","sK1") &
~mia_forename("sK2","sK0") &
~mia_forename("sK1","sK4") &
~mia_forename("sK1","sK3") &
~mia_forename("sK1","sK2") &
~mia_forename("sK1","sK1") &
~mia_forename("sK1","sK0") &
~mia_forename("sK0","sK4") &
~mia_forename("sK0","sK3") &
~mia_forename("sK0","sK1") &
~mia_forename("sK0","sK0") &
mia_forename("sK0","sK2") &
~mia_forename("sK4","sK4") &
~mia_forename("sK4","sK3") &
~mia_forename("sK4","sK2") &
~mia_forename("sK4","sK1") &
~mia_forename("sK4","sK0") &
~mia_forename("sK3","sK4") &
~mia_forename("sK3","sK3") &
~mia_forename("sK3","sK2") &
~mia_forename("sK3","sK1") &
~mia_forename("sK3","sK0") &
~mia_forename("sK2","sK4") &
~mia_forename("sK2","sK3") &
~forename("sK3","sK3") &
~forename("sK2","sK3") &
~forename("sK1","sK3") &
~forename("sK0","sK0") &
~forename("sK4","sK0") &
~forename("sK3","sK0") &
~forename("sK2","sK0") &
~forename("sK1","sK0") &
~forename("sK4","sK1") &
~forename("sK3","sK1") &
~forename("sK2","sK1") &
~forename("sK1","sK1") &
~forename("sK0","sK3") &
forename("sK0","sK2") &
~forename("sK0","sK1") &
forename("sK4","sK2") &
forename("sK3","sK2") &
forename("sK2","sK2") &
forename("sK1","sK2") &
~forename("sK4","sK4") &
~forename("sK3","sK4") &
~forename("sK2","sK4") &
~forename("sK1","sK4") &
~forename("sK0","sK4") &
~forename("sK4","sK3") &
~abstraction("sK3","sK0") &
~abstraction("sK2","sK4") &
~abstraction("sK2","sK3") &
~abstraction("sK2","sK1") &
~abstraction("sK2","sK0") &
~abstraction("sK1","sK4") &
~abstraction("sK1","sK3") &
~abstraction("sK1","sK1") &
~abstraction("sK1","sK0") &
~abstraction("sK0","sK4") &
~abstraction("sK0","sK3") &
~abstraction("sK0","sK0") &
~abstraction("sK0","sK1") &
abstraction("sK0","sK2") &
abstraction("sK4","sK2") &
abstraction("sK3","sK2") &
abstraction("sK2","sK2") &
abstraction("sK1","sK2") &
~abstraction("sK4","sK4") &
~abstraction("sK4","sK3") &
~abstraction("sK4","sK1") &
~abstraction("sK4","sK0") &
~abstraction("sK3","sK4") &
~abstraction("sK3","sK3") &
~abstraction("sK3","sK1") &
unisex("sK3","sK4") &
unisex("sK3","sK3") &
unisex("sK3","sK1") &
unisex("sK3","sK0") &
unisex("sK2","sK4") &
unisex("sK2","sK3") &
unisex("sK2","sK1") &
unisex("sK2","sK0") &
unisex("sK1","sK4") &
unisex("sK1","sK3") &
unisex("sK1","sK1") &
unisex("sK1","sK0") &
~unisex("sK0","sK1") &
unisex("sK0","sK2") &
unisex("sK0","sK4") &
unisex("sK0","sK3") &
unisex("sK0","sK0") &
unisex("sK4","sK2") &
unisex("sK3","sK2") &
unisex("sK2","sK2") &
unisex("sK1","sK2") &
unisex("sK4","sK4") &
unisex("sK4","sK3") &
unisex("sK4","sK1") &
unisex("sK4","sK0") &
~general("sK2","sK4") &
~general("sK2","sK3") &
~general("sK2","sK1") &
~general("sK2","sK0") &
~general("sK1","sK4") &
~general("sK1","sK3") &
~general("sK1","sK1") &
~general("sK1","sK0") &
~general("sK0","sK4") &
~general("sK0","sK3") &
~general("sK0","sK1") &
~general("sK0","sK0") &
general("sK0","sK2") &
general("sK4","sK2") &
general("sK3","sK2") &
general("sK2","sK2") &
general("sK1","sK2") &
~general("sK4","sK4") &
~general("sK4","sK3") &
~general("sK4","sK1") &
~general("sK4","sK0") &
~general("sK3","sK4") &
~general("sK3","sK3") &
~general("sK3","sK1") &
~general("sK3","sK0") &
~nonhuman("sK3","sK4") &
~nonhuman("sK3","sK3") &
~nonhuman("sK3","sK1") &
~nonhuman("sK3","sK0") &
~nonhuman("sK2","sK4") &
~nonhuman("sK2","sK3") &
~nonhuman("sK2","sK1") &
~nonhuman("sK2","sK0") &
~nonhuman("sK1","sK4") &
~nonhuman("sK1","sK3") &
~nonhuman("sK1","sK1") &
~nonhuman("sK1","sK0") &
~nonhuman("sK0","sK1") &
nonhuman("sK0","sK2") &
nonhuman("sK0","sK4") &
nonhuman("sK0","sK3") &
nonhuman("sK0","sK0") &
nonhuman("sK4","sK2") &
nonhuman("sK3","sK2") &
nonhuman("sK2","sK2") &
nonhuman("sK1","sK2") &
~nonhuman("sK4","sK4") &
~nonhuman("sK4","sK3") &
~nonhuman("sK4","sK1") &
~nonhuman("sK4","sK0") &
thing("sK3","sK4") &
thing("sK3","sK3") &
thing("sK3","sK1") &
thing("sK3","sK0") &
thing("sK2","sK4") &
thing("sK2","sK3") &
thing("sK2","sK1") &
thing("sK2","sK0") &
thing("sK1","sK4") &
thing("sK1","sK3") &
thing("sK1","sK1") &
thing("sK1","sK0") &
thing("sK0","sK2") &
thing("sK0","sK4") &
thing("sK4","sK2") &
thing("sK3","sK2") &
thing("sK2","sK2") &
thing("sK1","sK2") &
thing("sK0","sK3") &
thing("sK0","sK1") &
thing("sK0","sK0") &
thing("sK4","sK4") &
thing("sK4","sK3") &
thing("sK4","sK1") &
thing("sK4","sK0") &
~relation("sK2","sK4") &
~relation("sK2","sK3") &
~relation("sK2","sK1") &
~relation("sK2","sK0") &
~relation("sK1","sK4") &
~relation("sK1","sK3") &
~relation("sK1","sK1") &
~relation("sK1","sK0") &
~relation("sK0","sK4") &
~relation("sK0","sK3") &
~relation("sK0","sK1") &
~relation("sK0","sK0") &
relation("sK0","sK2") &
relation("sK4","sK2") &
relation("sK3","sK2") &
relation("sK2","sK2") &
relation("sK1","sK2") &
~relation("sK4","sK4") &
~relation("sK4","sK3") &
~relation("sK4","sK1") &
~relation("sK4","sK0") &
~relation("sK3","sK4") &
~relation("sK3","sK3") &
~relation("sK3","sK1") &
~relation("sK3","sK0") &
~relname("sK2","sK4") &
~relname("sK2","sK3") &
~relname("sK2","sK1") &
~relname("sK2","sK0") &
~relname("sK1","sK4") &
~relname("sK1","sK3") &
~relname("sK1","sK1") &
~relname("sK1","sK0") &
~relname("sK0","sK4") &
~relname("sK0","sK3") &
~relname("sK0","sK1") &
~relname("sK0","sK0") &
relname("sK0","sK2") &
relname("sK4","sK2") &
relname("sK3","sK2") &
relname("sK2","sK2") &
relname("sK1","sK2") &
~relname("sK4","sK4") &
~relname("sK4","sK3") &
~relname("sK4","sK1") &
~relname("sK4","sK0") &
~relname("sK3","sK4") &
~relname("sK3","sK3") &
~relname("sK3","sK1") &
~relname("sK3","sK0") &
object("sK3","sK4") &
object("sK3","sK3") &
object("sK3","sK1") &
object("sK3","sK0") &
object("sK2","sK4") &
object("sK2","sK3") &
object("sK2","sK1") &
object("sK2","sK0") &
object("sK1","sK4") &
object("sK1","sK3") &
object("sK1","sK1") &
object("sK1","sK0") &
~object("sK0","sK1") &
object("sK0","sK3") &
~object("sK0","sK2") &
~object("sK0","sK4") &
~object("sK4","sK2") &
~object("sK3","sK2") &
~object("sK2","sK2") &
~object("sK1","sK2") &
~object("sK0","sK0") &
object("sK4","sK4") &
object("sK4","sK3") &
object("sK4","sK1") &
object("sK4","sK0") &
nonliving("sK2","sK2") &
nonliving("sK2","sK1") &
nonliving("sK2","sK0") &
nonliving("sK1","sK4") &
nonliving("sK1","sK3") &
nonliving("sK1","sK2") &
nonliving("sK1","sK1") &
nonliving("sK1","sK0") &
nonliving("sK0","sK4") &
nonliving("sK0","sK3") &
nonliving("sK0","sK2") &
nonliving("sK0","sK0") &
~nonliving("sK0","sK1") &
nonliving("sK4","sK4") &
nonliving("sK4","sK3") &
nonliving("sK4","sK2") &
nonliving("sK4","sK1") &
nonliving("sK4","sK0") &
nonliving("sK3","sK4") &
nonliving("sK3","sK3") &
nonliving("sK3","sK2") &
nonliving("sK3","sK1") &
nonliving("sK3","sK0") &
nonliving("sK2","sK4") &
nonliving("sK2","sK3") &
existent("sK3","sK1") &
existent("sK3","sK0") &
existent("sK2","sK4") &
existent("sK2","sK3") &
existent("sK2","sK2") &
existent("sK2","sK1") &
existent("sK2","sK0") &
existent("sK1","sK4") &
existent("sK1","sK3") &
existent("sK1","sK2") &
existent("sK1","sK1") &
existent("sK1","sK0") &
~existent("sK0","sK4") &
existent("sK0","sK3") &
existent("sK0","sK1") &
~existent("sK0","sK2") &
~existent("sK0","sK0") &
existent("sK4","sK4") &
existent("sK4","sK3") &
existent("sK4","sK2") &
existent("sK4","sK1") &
existent("sK4","sK0") &
existent("sK3","sK4") &
existent("sK3","sK3") &
existent("sK3","sK2") &
specific("sK3","sK4") &
specific("sK3","sK3") &
specific("sK3","sK1") &
specific("sK3","sK0") &
specific("sK2","sK4") &
specific("sK2","sK3") &
specific("sK2","sK1") &
specific("sK2","sK0") &
specific("sK1","sK4") &
specific("sK1","sK3") &
specific("sK1","sK1") &
specific("sK1","sK0") &
specific("sK0","sK4") &
~specific("sK0","sK2") &
~specific("sK4","sK2") &
~specific("sK3","sK2") &
~specific("sK2","sK2") &
~specific("sK1","sK2") &
specific("sK0","sK3") &
specific("sK0","sK1") &
specific("sK0","sK0") &
specific("sK4","sK4") &
specific("sK4","sK3") &
specific("sK4","sK1") &
specific("sK4","sK0") &
~substance_matter("sK3","sK4") &
~substance_matter("sK3","sK3") &
~substance_matter("sK3","sK1") &
~substance_matter("sK3","sK0") &
~substance_matter("sK2","sK4") &
~substance_matter("sK2","sK3") &
~substance_matter("sK2","sK1") &
~substance_matter("sK2","sK0") &
~substance_matter("sK1","sK4") &
~substance_matter("sK1","sK3") &
~substance_matter("sK1","sK1") &
~substance_matter("sK1","sK0") &
~substance_matter("sK0","sK2") &
substance_matter("sK0","sK3") &
~substance_matter("sK0","sK4") &
~substance_matter("sK0","sK1") &
~substance_matter("sK4","sK2") &
~substance_matter("sK3","sK2") &
~substance_matter("sK2","sK2") &
~substance_matter("sK1","sK2") &
~substance_matter("sK0","sK0") &
~substance_matter("sK4","sK4") &
~substance_matter("sK4","sK3") &
~substance_matter("sK4","sK1") &
~substance_matter("sK4","sK0") &
~food("sK2","sK2") &
~food("sK2","sK1") &
~food("sK2","sK0") &
~food("sK1","sK4") &
~food("sK1","sK3") &
~food("sK1","sK2") &
~food("sK1","sK1") &
~food("sK1","sK0") &
~food("sK0","sK4") &
~food("sK0","sK2") &
~food("sK0","sK1") &
~food("sK0","sK0") &
food("sK0","sK3") &
~food("sK4","sK4") &
~food("sK4","sK3") &
~food("sK4","sK2") &
~food("sK4","sK1") &
~food("sK4","sK0") &
~food("sK3","sK4") &
~food("sK3","sK3") &
~food("sK3","sK2") &
~food("sK3","sK1") &
~food("sK3","sK0") &
~food("sK2","sK4") &
~food("sK2","sK3") &
~beverage("sK2","sK2") &
~beverage("sK2","sK1") &
~beverage("sK2","sK0") &
~beverage("sK1","sK4") &
~beverage("sK1","sK3") &
~beverage("sK1","sK2") &
~beverage("sK1","sK1") &
~beverage("sK1","sK0") &
~beverage("sK0","sK4") &
~beverage("sK0","sK2") &
~beverage("sK0","sK1") &
~beverage("sK0","sK0") &
beverage("sK0","sK3") &
~beverage("sK4","sK4") &
~beverage("sK4","sK3") &
~beverage("sK4","sK2") &
~beverage("sK4","sK1") &
~beverage("sK4","sK0") &
~beverage("sK3","sK4") &
~beverage("sK3","sK3") &
~beverage("sK3","sK2") &
~beverage("sK3","sK1") &
~beverage("sK3","sK0") &
~beverage("sK2","sK4") &
~beverage("sK2","sK3") &
~shake_beverage("sK2","sK2") &
~shake_beverage("sK2","sK1") &
~shake_beverage("sK2","sK0") &
~shake_beverage("sK1","sK4") &
~shake_beverage("sK1","sK3") &
~shake_beverage("sK1","sK2") &
~shake_beverage("sK1","sK1") &
~shake_beverage("sK1","sK0") &
~shake_beverage("sK0","sK4") &
~shake_beverage("sK0","sK2") &
~shake_beverage("sK0","sK1") &
~shake_beverage("sK0","sK0") &
shake_beverage("sK0","sK3") &
~shake_beverage("sK4","sK4") &
~shake_beverage("sK4","sK3") &
~shake_beverage("sK4","sK2") &
~shake_beverage("sK4","sK1") &
~shake_beverage("sK4","sK0") &
~shake_beverage("sK3","sK4") &
~shake_beverage("sK3","sK3") &
~shake_beverage("sK3","sK2") &
~shake_beverage("sK3","sK1") &
~shake_beverage("sK3","sK0") &
~shake_beverage("sK2","sK4") &
~shake_beverage("sK2","sK3") &
~order("sK3","sK1") &
~order("sK3","sK0") &
~order("sK2","sK4") &
~order("sK2","sK3") &
~order("sK2","sK2") &
~order("sK2","sK1") &
~order("sK2","sK0") &
~order("sK1","sK4") &
~order("sK1","sK3") &
~order("sK1","sK2") &
~order("sK1","sK1") &
~order("sK1","sK0") &
order("sK0","sK4") &
~order("sK0","sK2") &
~order("sK0","sK1") &
~order("sK0","sK3") &
order("sK0","sK0") &
~order("sK4","sK4") &
~order("sK4","sK3") &
~order("sK4","sK2") &
~order("sK4","sK1") &
~order("sK4","sK0") &
~order("sK3","sK4") &
~order("sK3","sK3") &
~order("sK3","sK2") &
~event("sK3","sK1") &
~event("sK3","sK0") &
~event("sK2","sK4") &
~event("sK2","sK3") &
~event("sK2","sK2") &
~event("sK2","sK1") &
~event("sK2","sK0") &
~event("sK1","sK4") &
~event("sK1","sK3") &
~event("sK1","sK2") &
~event("sK1","sK1") &
~event("sK1","sK0") &
event("sK0","sK4") &
~event("sK0","sK2") &
~event("sK0","sK3") &
~event("sK0","sK1") &
event("sK0","sK0") &
~event("sK4","sK4") &
~event("sK4","sK3") &
~event("sK4","sK2") &
~event("sK4","sK1") &
~event("sK4","sK0") &
~event("sK3","sK4") &
~event("sK3","sK3") &
~event("sK3","sK2") &
~eventuality("sK3","sK4") &
~eventuality("sK3","sK3") &
~eventuality("sK3","sK1") &
~eventuality("sK3","sK0") &
~eventuality("sK2","sK4") &
~eventuality("sK2","sK3") &
~eventuality("sK2","sK1") &
~eventuality("sK2","sK0") &
~eventuality("sK1","sK4") &
~eventuality("sK1","sK3") &
~eventuality("sK1","sK1") &
~eventuality("sK1","sK0") &
~eventuality("sK0","sK2") &
~eventuality("sK0","sK3") &
~eventuality("sK0","sK1") &
eventuality("sK0","sK4") &
eventuality("sK0","sK0") &
~eventuality("sK4","sK2") &
~eventuality("sK3","sK2") &
~eventuality("sK2","sK2") &
~eventuality("sK1","sK2") &
~eventuality("sK4","sK4") &
~eventuality("sK4","sK3") &
~eventuality("sK4","sK1") &
~eventuality("sK4","sK0") &
~nonexistent("sK3","sK1") &
~nonexistent("sK3","sK0") &
~nonexistent("sK2","sK4") &
~nonexistent("sK2","sK3") &
~nonexistent("sK2","sK2") &
~nonexistent("sK2","sK1") &
~nonexistent("sK2","sK0") &
~nonexistent("sK1","sK4") &
~nonexistent("sK1","sK3") &
~nonexistent("sK1","sK2") &
~nonexistent("sK1","sK1") &
~nonexistent("sK1","sK0") &
~nonexistent("sK0","sK3") &
~nonexistent("sK0","sK1") &
nonexistent("sK0","sK4") &
nonexistent("sK0","sK2") &
nonexistent("sK0","sK0") &
~nonexistent("sK4","sK4") &
~nonexistent("sK4","sK3") &
~nonexistent("sK4","sK2") &
~nonexistent("sK4","sK1") &
~nonexistent("sK4","sK0") &
~nonexistent("sK3","sK4") &
~nonexistent("sK3","sK3") &
~nonexistent("sK3","sK2") &
singleton("sK2","sK1") &
singleton("sK2","sK0") &
singleton("sK1","sK4") &
singleton("sK1","sK3") &
singleton("sK1","sK2") &
singleton("sK1","sK1") &
singleton("sK1","sK0") &
singleton("sK0","sK4") &
singleton("sK0","sK3") &
singleton("sK0","sK2") &
singleton("sK0","sK1") &
singleton("sK0","sK0") &
singleton("sK4","sK4") &
singleton("sK4","sK3") &
singleton("sK4","sK2") &
singleton("sK4","sK1") &
singleton("sK4","sK0") &
singleton("sK3","sK4") &
singleton("sK3","sK3") &
singleton("sK3","sK2") &
singleton("sK3","sK1") &
singleton("sK3","sK0") &
singleton("sK2","sK4") &
singleton("sK2","sK3") &
singleton("sK2","sK2") &
~act("sK3","sK1") &
~act("sK3","sK0") &
~act("sK2","sK4") &
~act("sK2","sK3") &
~act("sK2","sK2") &
~act("sK2","sK1") &
~act("sK2","sK0") &
~act("sK1","sK4") &
~act("sK1","sK3") &
~act("sK1","sK2") &
~act("sK1","sK1") &
~act("sK1","sK0") &
~act("sK0","sK3") &
act("sK0","sK4") &
~act("sK0","sK2") &
~act("sK0","sK1") &
act("sK0","sK0") &
~act("sK4","sK4") &
~act("sK4","sK3") &
~act("sK4","sK2") &
~act("sK4","sK1") &
~act("sK4","sK0") &
~act("sK3","sK4") &
~act("sK3","sK3") &
~act("sK3","sK2") &
of("sK3","sK2","sK0") &
of("sK3","sK0","sK4") &
of("sK3","sK0","sK3") &
of("sK3","sK0","sK2") &
of("sK3","sK0","sK1") &
of("sK3","sK0","sK0") &
of("sK2","sK4","sK4") &
of("sK2","sK4","sK3") &
of("sK2","sK4","sK2") &
of("sK2","sK4","sK1") &
of("sK2","sK4","sK0") &
of("sK2","sK3","sK4") &
of("sK2","sK3","sK3") &
of("sK2","sK3","sK2") &
of("sK2","sK3","sK1") &
of("sK3","sK2","sK1") &
of("sK3","sK2","sK2") &
of("sK3","sK2","sK3") &
of("sK3","sK2","sK4") &
of("sK3","sK3","sK0") &
of("sK3","sK3","sK1") &
of("sK3","sK3","sK2") &
of("sK3","sK3","sK3") &
of("sK3","sK3","sK4") &
of("sK3","sK4","sK0") &
of("sK3","sK4","sK1") &
of("sK3","sK4","sK2") &
of("sK3","sK4","sK3") &
of("sK3","sK4","sK4") &
of("sK4","sK0","sK0") &
of("sK4","sK0","sK1") &
of("sK1","sK0","sK0") &
of("sK1","sK0","sK1") &
of("sK1","sK0","sK2") &
of("sK1","sK0","sK3") &
of("sK1","sK0","sK4") &
of("sK1","sK2","sK0") &
of("sK1","sK2","sK1") &
of("sK1","sK2","sK2") &
of("sK1","sK2","sK3") &
of("sK1","sK2","sK4") &
of("sK1","sK3","sK0") &
of("sK1","sK3","sK1") &
of("sK1","sK3","sK2") &
of("sK1","sK3","sK3") &
of("sK1","sK3","sK4") &
of("sK1","sK4","sK0") &
of("sK1","sK4","sK1") &
of("sK1","sK4","sK2") &
of("sK1","sK4","sK3") &
of("sK1","sK4","sK4") &
of("sK2","sK0","sK0") &
of("sK2","sK0","sK1") &
of("sK2","sK0","sK2") &
of("sK2","sK0","sK3") &
of("sK2","sK0","sK4") &
of("sK2","sK2","sK0") &
of("sK2","sK2","sK1") &
of("sK2","sK2","sK2") &
of("sK2","sK2","sK3") &
of("sK2","sK2","sK4") &
of("sK2","sK3","sK0") &
~of("sK3","sK1","sK4") &
~of("sK4","sK1","sK0") &
~of("sK4","sK1","sK1") &
~of("sK4","sK1","sK2") &
~of("sK4","sK1","sK3") &
~of("sK4","sK1","sK4") &
~of("sK0","sK1","sK0") &
~of("sK0","sK1","sK2") &
~of("sK0","sK1","sK3") &
~of("sK0","sK1","sK4") &
~of("sK0","sK3","sK0") &
~of("sK0","sK3","sK2") &
~of("sK0","sK3","sK3") &
~of("sK0","sK3","sK4") &
~of("sK0","sK4","sK0") &
~of("sK0","sK4","sK2") &
~of("sK0","sK4","sK3") &
~of("sK0","sK4","sK4") &
of("sK0","sK2","sK0") &
of("sK0","sK2","sK2") &
of("sK0","sK2","sK4") &
~of("sK0","sK0","sK0") &
~of("sK0","sK0","sK2") &
~of("sK0","sK0","sK3") &
~of("sK0","sK0","sK4") &
~of("sK0","sK1","sK1") &
~of("sK0","sK3","sK1") &
~of("sK0","sK4","sK1") &
~of("sK0","sK2","sK3") &
~of("sK0","sK0","sK1") &
of("sK0","sK2","sK1") &
of("sK4","sK0","sK2") &
of("sK4","sK0","sK3") &
of("sK4","sK0","sK4") &
of("sK4","sK2","sK0") &
of("sK4","sK2","sK1") &
of("sK4","sK2","sK2") &
of("sK4","sK2","sK3") &
of("sK4","sK2","sK4") &
of("sK4","sK3","sK0") &
of("sK4","sK3","sK1") &
of("sK4","sK3","sK2") &
of("sK4","sK3","sK3") &
of("sK4","sK3","sK4") &
of("sK4","sK4","sK0") &
of("sK4","sK4","sK1") &
of("sK4","sK4","sK2") &
~of("sK3","sK1","sK3") &
~of("sK3","sK1","sK2") &
~of("sK3","sK1","sK1") &
~of("sK3","sK1","sK0") &
~of("sK2","sK1","sK4") &
~of("sK2","sK1","sK3") &
~of("sK2","sK1","sK2") &
~of("sK2","sK1","sK1") &
~of("sK2","sK1","sK0") &
~of("sK1","sK1","sK4") &
~of("sK1","sK1","sK3") &
~of("sK1","sK1","sK2") &
~of("sK1","sK1","sK1") &
~of("sK1","sK1","sK0") &
of("sK4","sK4","sK4") &
of("sK4","sK4","sK3") &
nonreflexive("sK2","sK2") &
nonreflexive("sK2","sK1") &
nonreflexive("sK2","sK0") &
nonreflexive("sK1","sK4") &
nonreflexive("sK1","sK3") &
nonreflexive("sK1","sK2") &
nonreflexive("sK1","sK1") &
nonreflexive("sK1","sK0") &
nonreflexive("sK0","sK3") &
nonreflexive("sK0","sK2") &
nonreflexive("sK0","sK1") &
nonreflexive("sK0","sK0") &
nonreflexive("sK0","sK4") &
nonreflexive("sK4","sK4") &
nonreflexive("sK4","sK3") &
nonreflexive("sK4","sK2") &
nonreflexive("sK4","sK1") &
nonreflexive("sK4","sK0") &
nonreflexive("sK3","sK4") &
nonreflexive("sK3","sK3") &
nonreflexive("sK3","sK2") &
nonreflexive("sK3","sK1") &
nonreflexive("sK3","sK0") &
nonreflexive("sK2","sK4") &
nonreflexive("sK2","sK3") &
agent("sK2","sK4","sK0") &
agent("sK2","sK3","sK4") &
agent("sK2","sK3","sK3") &
agent("sK2","sK3","sK2") &
agent("sK2","sK3","sK1") &
agent("sK2","sK3","sK0") &
agent("sK2","sK2","sK4") &
agent("sK2","sK2","sK3") &
agent("sK2","sK2","sK2") &
agent("sK2","sK2","sK1") &
agent("sK2","sK2","sK0") &
agent("sK2","sK1","sK4") &
agent("sK2","sK1","sK3") &
agent("sK2","sK1","sK2") &
agent("sK2","sK1","sK1") &
agent("sK2","sK4","sK1") &
agent("sK2","sK4","sK2") &
agent("sK2","sK4","sK3") &
agent("sK2","sK4","sK4") &
agent("sK3","sK0","sK0") &
agent("sK3","sK0","sK1") &
agent("sK3","sK0","sK2") &
agent("sK3","sK0","sK3") &
agent("sK3","sK0","sK4") &
agent("sK3","sK1","sK0") &
agent("sK3","sK1","sK1") &
agent("sK3","sK1","sK2") &
agent("sK3","sK1","sK3") &
agent("sK3","sK1","sK4") &
agent("sK3","sK2","sK0") &
agent("sK3","sK2","sK1") &
agent("sK1","sK0","sK0") &
agent("sK1","sK0","sK1") &
agent("sK1","sK0","sK2") &
agent("sK1","sK0","sK3") &
agent("sK1","sK0","sK4") &
agent("sK1","sK1","sK0") &
agent("sK1","sK1","sK1") &
agent("sK1","sK1","sK2") &
agent("sK1","sK1","sK3") &
agent("sK1","sK1","sK4") &
agent("sK1","sK2","sK0") &
agent("sK1","sK2","sK1") &
agent("sK1","sK2","sK2") &
agent("sK1","sK2","sK3") &
agent("sK1","sK2","sK4") &
agent("sK1","sK3","sK0") &
agent("sK1","sK3","sK1") &
agent("sK1","sK3","sK2") &
agent("sK1","sK3","sK3") &
agent("sK1","sK3","sK4") &
agent("sK1","sK4","sK0") &
agent("sK1","sK4","sK1") &
agent("sK1","sK4","sK2") &
agent("sK1","sK4","sK3") &
agent("sK1","sK4","sK4") &
agent("sK2","sK0","sK0") &
agent("sK2","sK0","sK1") &
agent("sK2","sK0","sK2") &
agent("sK2","sK0","sK3") &
agent("sK2","sK0","sK4") &
agent("sK2","sK1","sK0") &
agent("sK4","sK3","sK4") &
agent("sK4","sK4","sK0") &
agent("sK4","sK4","sK1") &
agent("sK4","sK4","sK2") &
agent("sK4","sK4","sK3") &
agent("sK4","sK4","sK4") &
~agent("sK0","sK0","sK0") &
~agent("sK0","sK0","sK2") &
~agent("sK0","sK0","sK4") &
~agent("sK0","sK1","sK0") &
~agent("sK0","sK1","sK2") &
~agent("sK0","sK1","sK4") &
~agent("sK0","sK2","sK0") &
~agent("sK0","sK2","sK2") &
~agent("sK0","sK2","sK4") &
~agent("sK0","sK3","sK0") &
~agent("sK0","sK3","sK2") &
~agent("sK0","sK3","sK4") &
~agent("sK0","sK4","sK0") &
~agent("sK0","sK4","sK2") &
~agent("sK0","sK4","sK4") &
agent("sK0","sK0","sK1") &
agent("sK0","sK1","sK1") &
agent("sK0","sK2","sK1") &
agent("sK0","sK3","sK1") &
~agent("sK0","sK0","sK3") &
~agent("sK0","sK1","sK3") &
~agent("sK0","sK2","sK3") &
~agent("sK0","sK3","sK3") &
~agent("sK0","sK4","sK3") &
agent("sK0","sK4","sK1") &
agent("sK3","sK2","sK2") &
agent("sK3","sK2","sK3") &
agent("sK3","sK2","sK4") &
agent("sK3","sK3","sK0") &
agent("sK3","sK3","sK1") &
agent("sK3","sK3","sK2") &
agent("sK3","sK3","sK3") &
agent("sK3","sK3","sK4") &
agent("sK3","sK4","sK0") &
agent("sK3","sK4","sK1") &
agent("sK3","sK4","sK2") &
agent("sK3","sK4","sK3") &
agent("sK3","sK4","sK4") &
agent("sK4","sK0","sK0") &
agent("sK4","sK0","sK1") &
agent("sK4","sK0","sK2") &
agent("sK4","sK3","sK3") &
agent("sK4","sK3","sK2") &
agent("sK4","sK3","sK1") &
agent("sK4","sK3","sK0") &
agent("sK4","sK2","sK4") &
agent("sK4","sK2","sK3") &
agent("sK4","sK2","sK2") &
agent("sK4","sK2","sK1") &
agent("sK4","sK2","sK0") &
agent("sK4","sK1","sK4") &
agent("sK4","sK1","sK3") &
agent("sK4","sK1","sK2") &
agent("sK4","sK1","sK1") &
agent("sK4","sK1","sK0") &
agent("sK4","sK0","sK4") &
agent("sK4","sK0","sK3") &
~patient("sK2","sK4","sK0") &
~patient("sK2","sK3","sK4") &
~patient("sK2","sK3","sK3") &
~patient("sK2","sK3","sK2") &
~patient("sK2","sK3","sK1") &
~patient("sK2","sK3","sK0") &
~patient("sK2","sK2","sK4") &
~patient("sK2","sK2","sK3") &
~patient("sK2","sK2","sK2") &
~patient("sK2","sK2","sK1") &
~patient("sK2","sK2","sK0") &
~patient("sK2","sK1","sK4") &
~patient("sK2","sK1","sK3") &
~patient("sK2","sK1","sK2") &
~patient("sK2","sK1","sK1") &
~patient("sK2","sK4","sK1") &
~patient("sK2","sK4","sK2") &
~patient("sK2","sK4","sK3") &
~patient("sK2","sK4","sK4") &
~patient("sK3","sK0","sK0") &
~patient("sK3","sK0","sK1") &
~patient("sK3","sK0","sK2") &
~patient("sK3","sK0","sK3") &
~patient("sK3","sK0","sK4") &
~patient("sK3","sK1","sK0") &
~patient("sK3","sK1","sK1") &
~patient("sK3","sK1","sK2") &
~patient("sK3","sK1","sK3") &
~patient("sK3","sK1","sK4") &
~patient("sK3","sK2","sK0") &
~patient("sK3","sK2","sK1") &
~patient("sK1","sK0","sK0") &
~patient("sK1","sK0","sK1") &
~patient("sK1","sK0","sK2") &
~patient("sK1","sK0","sK3") &
~patient("sK1","sK0","sK4") &
~patient("sK1","sK1","sK0") &
~patient("sK1","sK1","sK1") &
~patient("sK1","sK1","sK2") &
~patient("sK1","sK1","sK3") &
~patient("sK1","sK1","sK4") &
~patient("sK1","sK2","sK0") &
~patient("sK1","sK2","sK1") &
~patient("sK1","sK2","sK2") &
~patient("sK1","sK2","sK3") &
~patient("sK1","sK2","sK4") &
~patient("sK1","sK3","sK0") &
~patient("sK1","sK3","sK1") &
~patient("sK1","sK3","sK2") &
~patient("sK1","sK3","sK3") &
~patient("sK1","sK3","sK4") &
~patient("sK1","sK4","sK0") &
~patient("sK1","sK4","sK1") &
~patient("sK1","sK4","sK2") &
~patient("sK1","sK4","sK3") &
~patient("sK1","sK4","sK4") &
~patient("sK2","sK0","sK0") &
~patient("sK2","sK0","sK1") &
~patient("sK2","sK0","sK2") &
~patient("sK2","sK0","sK3") &
~patient("sK2","sK0","sK4") &
~patient("sK2","sK1","sK0") &
~patient("sK4","sK3","sK4") &
~patient("sK4","sK4","sK0") &
~patient("sK4","sK4","sK1") &
~patient("sK4","sK4","sK2") &
~patient("sK4","sK4","sK3") &
~patient("sK4","sK4","sK4") &
patient("sK0","sK0","sK0") &
patient("sK0","sK0","sK2") &
patient("sK0","sK0","sK4") &
patient("sK0","sK1","sK0") &
patient("sK0","sK1","sK2") &
patient("sK0","sK1","sK4") &
patient("sK0","sK2","sK0") &
patient("sK0","sK2","sK2") &
patient("sK0","sK2","sK4") &
patient("sK0","sK3","sK0") &
patient("sK0","sK3","sK2") &
patient("sK0","sK3","sK4") &
patient("sK0","sK4","sK0") &
patient("sK0","sK4","sK2") &
patient("sK0","sK4","sK4") &
~patient("sK0","sK0","sK1") &
~patient("sK0","sK1","sK1") &
~patient("sK0","sK2","sK1") &
~patient("sK0","sK3","sK1") &
patient("sK0","sK0","sK3") &
patient("sK0","sK1","sK3") &
patient("sK0","sK2","sK3") &
patient("sK0","sK3","sK3") &
~patient("sK0","sK4","sK1") &
patient("sK0","sK4","sK3") &
~patient("sK3","sK2","sK2") &
~patient("sK3","sK2","sK3") &
~patient("sK3","sK2","sK4") &
~patient("sK3","sK3","sK0") &
~patient("sK3","sK3","sK1") &
~patient("sK3","sK3","sK2") &
~patient("sK3","sK3","sK3") &
~patient("sK3","sK3","sK4") &
~patient("sK3","sK4","sK0") &
~patient("sK3","sK4","sK1") &
~patient("sK3","sK4","sK2") &
~patient("sK3","sK4","sK3") &
~patient("sK3","sK4","sK4") &
~patient("sK4","sK0","sK0") &
~patient("sK4","sK0","sK1") &
~patient("sK4","sK0","sK2") &
~patient("sK4","sK3","sK3") &
~patient("sK4","sK3","sK2") &
~patient("sK4","sK3","sK1") &
~patient("sK4","sK3","sK0") &
~patient("sK4","sK2","sK4") &
~patient("sK4","sK2","sK3") &
~patient("sK4","sK2","sK2") &
~patient("sK4","sK2","sK1") &
~patient("sK4","sK2","sK0") &
~patient("sK4","sK1","sK4") &
~patient("sK4","sK1","sK3") &
~patient("sK4","sK1","sK2") &
~patient("sK4","sK1","sK1") &
~patient("sK4","sK1","sK0") &
~patient("sK4","sK0","sK4") &
~patient("sK4","sK0","sK3") &
~actual_world("sK1") &
~actual_world("sK2") &
~actual_world("sK3") &
~actual_world("sK4") &
actual_world("sK0") &
~past("sK1","sK0") &
~past("sK1","sK1") &
~past("sK1","sK2") &
~past("sK1","sK3") &
~past("sK1","sK4") &
~past("sK2","sK0") &
~past("sK2","sK1") &
~past("sK2","sK2") &
~past("sK2","sK3") &
~past("sK2","sK4") &
~past("sK3","sK0") &
~past("sK3","sK1") &
~past("sK3","sK2") &
~past("sK3","sK3") &
~past("sK3","sK4") &
~past("sK4","sK0") &
~past("sK4","sK1") &
~past("sK4","sK2") &
~past("sK4","sK3") &
~past("sK4","sK4") &
past("sK0","sK0") &
past("sK0","sK1") &
past("sK0","sK2") &
past("sK0","sK3") &
past("sK0","sK4") ) ).
% SZS output end FiniteModel for NLP042+1


### Sample solution for SWV017+1

Timeout :-(


## Zipperposition 0.2

Guillaume Burel, Simon Cruanes
ENSIIE/Cedric, France

### Sample solution for SEU140+2

# SZS status Theorem

# SZS output start Refutation
fof(13307, plain, \$false, inference('simplify_reflect-', [status(thm)], [13306,6220, theory(equality)])).
fof(13306, plain, (set_difference(sk0, set_difference(sk0, sk2)) = empty_set), inference('demod', [status(thm)], [13305,343, theory(equality)])).
fof(6220, plain, set_difference(sk0, set_difference(sk0, sk2)) != empty_set, inference('demod', [status(thm)], [329,790, theory(equality)])).
fof(13305, plain, (set_difference(set_difference(sk0, set_difference(sk0, sk2)), empty_set) = empty_set), inference('sup-', [status(thm)], [6072,345, theory(equality)])).
fof(343, plain, ![X1]: (set_difference(X1, empty_set) = X1), inference('elim', [status(esa)], [14, theory(equality)])).
fof(329, plain, ~disjoint(sk0, sk2), inference('elim', [status(esa)], [76, theory(equality)])).
fof(790, plain, ![X1]: ![X2]: (disjoint(X1, X2) <=> (set_difference(X1, set_difference(X1, X2)) = empty_set)), inference('demod', [status(thm)], [374,336, theory(equality)])).
fof(6072, plain, subset(set_difference(sk0, set_difference(sk0, sk2)), empty_set), inference('sup+', [status(thm)], [6029,653, theory(equality)])).
fof(345, plain, ![X1]: ![X2]: (~subset(X2, X1) | (set_difference(X2, X1) = empty_set)), inference('elim', [status(esa)], [134, theory(equality)])).
fof(14, axiom, ![X1]: (set_difference(X1, empty_set) = X1), file('SEU140+2.p', t3_boole)).
fof(76, plain, ~((subset(sk0, sk1) & disjoint(sk1, sk2)) => disjoint(sk0, sk2)), inference('elim', [status(esa)], [74, theory(equality)])).
fof(374, plain, ![X1]: ![X2]: (disjoint(X2, X1) <=> (set_intersection2(X2, X1) = empty_set)), inference('elim', [status(esa)], [214, theory(equality)])).
fof(336, plain, ![X1]: ![X2]: (set_difference(X2, set_difference(X2, X1)) = set_intersection2(X2, X1)), inference('elim', [status(esa)], [99, theory(equality)])).
fof(6029, plain, (set_difference(sk1, set_difference(sk1, sk2)) = empty_set), inference('demod', [status(thm)], [330,790, theory(equality)])).
fof(653, plain, ![X1]: subset(set_difference(sk0, set_difference(sk0, X1)), set_difference(sk1, set_difference(sk1, X1))), inference('sup-', [status(thm)], [331,644, theory(equality)])).
fof(134, plain, ![X1]: ![X2]: ((set_difference(X1, X2) = empty_set) <=> subset(X1, X2)), inference('elim', [status(esa)], [132, theory(equality)])).
fof(74, plain, ?[X1]: ~((subset(sk0, sk1) & disjoint(sk1, X1)) => disjoint(sk0, X1)), inference('elim', [status(esa)], [73, theory(equality)])).
fof(214, plain, ![X1]: ![X2]: (disjoint(X1, X2) <=> (set_intersection2(X1, X2) = empty_set)), inference('elim', [status(esa)], [41, theory(equality)])).
fof(99, plain, ![X1]: ![X2]: (set_difference(X1, set_difference(X1, X2)) = set_intersection2(X1, X2)), inference('elim', [status(esa)], [9, theory(equality)])).
fof(330, plain, disjoint(sk1, sk2), inference('elim', [status(esa)], [77, theory(equality)])).
fof(331, plain, subset(sk0, sk1), inference('elim', [status(esa)], [77, theory(equality)])).
fof(644, plain, ![X1]: ![X2]: ![X3]: (~subset(X2, X1) | subset(set_difference(X2, set_difference(X2, X3)), set_difference(X1, set_difference(X1, X3)))), inference('demod', [status(thm)], [354,336,336, theory(equality)])).
fof(132, plain, ![X1]: ![X2]: ((set_difference(X1, X2) = empty_set) <=> subset(X1, X2)), inference('elim', [status(esa)], [16, theory(equality)])).
fof(73, plain, ?[X1]: ?[X2]: ~((subset(sk0, X1) & disjoint(X1, X2)) => disjoint(sk0, X2)), inference('elim', [status(esa)], [5, theory(equality)])).
fof(41, axiom, ![X1]: ![X2]: (disjoint(X1, X2) <=> (set_intersection2(X1, X2) = empty_set)), file('SEU140+2.p', d7_xboole_0)).
fof(9, axiom, ![X1]: ![X2]: (set_difference(X1, set_difference(X1, X2)) = set_intersection2(X1, X2)), file('SEU140+2.p', t48_xboole_1)).
fof(77, plain, (subset(sk0, sk1) & disjoint(sk1, sk2)), inference('elim', [status(esa)], [76, theory(equality)])).
fof(354, plain, ![X1]: ![X2]: ![X3]: (~subset(X2, X3) | subset(set_intersection2(X2, X1), set_intersection2(X3, X1))), inference('elim', [status(esa)], [162, theory(equality)])).
fof(16, axiom, ![X1]: ![X2]: ((set_difference(X1, X2) = empty_set) <=> subset(X1, X2)), file('SEU140+2.p', t37_xboole_1)).
fof(5, axiom, ~![X1]: ![X2]: ![X3]: ((subset(X1, X2) & disjoint(X2, X3)) => disjoint(X1, X3)), file('SEU140+2.p', t63_xboole_1)).
fof(162, plain, ![X1]: ![X2]: ![X3]: (subset(X2, X3) => subset(set_intersection2(X2, X1), set_intersection2(X3, X1))), inference('elim', [status(esa)], [161, theory(equality)])).
fof(161, plain, ![X1]: ![X2]: ![X3]: (subset(X2, X1) => subset(set_intersection2(X2, X3), set_intersection2(X1, X3))), inference('elim', [status(esa)], [160, theory(equality)])).
fof(160, plain, ![X1]: ![X2]: ![X3]: (subset(X1, X2) => subset(set_intersection2(X1, X3), set_intersection2(X2, X3))), inference('elim', [status(esa)], [23, theory(equality)])).
fof(23, axiom, ![X1]: ![X2]: ![X3]: (subset(X1, X2) => subset(set_intersection2(X1, X3), set_intersection2(X2, X3))), file('SEU140+2.p', t26_xboole_1)).

# SZS output end Refutation