Dave is cold. Dave is kind. Dave is rough. Dave is young. Erin is blue. Erin is cold. Erin is kind. Erin is rough. Erin is round. Erin is white. Erin is young. Harry is blue. Harry is cold. Harry is kind. Harry is round. Harry is young. If something is white and kind then it is rough. If something is kind and round then it is cold.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and kind then it is rough.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is kind and round then it is cold.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Erin is rough.
True
1
proof
[(triple8 OR ((triple10 triple7) -> rule1))]
("Erin" "is" "rough" "+")
triple8
((triple10 triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not kind.
False
1
inv-proof
[(triple7)]
("Erin" "is" "kind" "-")
triple7
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2)] Dave is rough.[(triple3)] Dave is young.[(triple4)] Erin is blue.[(triple5)] Erin is cold.[(triple6 OR ((triple7 triple9) -> rule2))] Erin is kind.[(triple7)] Erin is rough.[(triple8 OR ((triple10 triple7) -> rule1))] Erin is round.[(triple9)] Erin is white.[(triple10)] Erin is young.[(triple11)] Harry is blue.[(triple12)] Harry is cold.[(triple13 OR ((triple14 triple15) -> rule2))] Harry is kind.[(triple14)] Harry is round.[(triple15)] Harry is young.[(triple16)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple7 triple9) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple10 triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple14 triple15) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16