Anne is cold. Anne is kind. Anne is nice. Anne is smart. Anne is young. Dave is not cold. Dave is furry. Dave is red. Fiona is cold. Fiona is red. Fiona is young. Harry is furry. Harry is kind. Harry is red. Harry is smart. Harry is young. If something is nice and young then it is red. All young things are red. If Dave is cold and Dave is nice then Dave is not smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is nice and young then it is red.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If Dave is cold and Dave is nice then Dave is not smart.
((("Dave" "is" "cold" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "smart" "-"))
Harry is furry.
True
1
proof
[(triple12)]
("Harry" "is" "furry" "+")
triple12
Anne is not nice.
False
1
inv-proof
[(triple3)]
("Anne" "is" "nice" "-")
triple3
Anne is red.
True
2
proof
[(((triple5) -> rule2) OR ((triple3 triple5) -> rule1))]
("Anne" "is" "red" "+")
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple3 triple5) -> rule1))]
("Anne" "is" "red" "-")
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is smart.[(triple4)] Anne is young.[(triple5)] Dave is furry.[(triple7)] Dave is not cold.[(triple6)] Dave is red.[(triple8)] Fiona is cold.[(triple9)] Fiona is red.[(triple10 OR ((triple11) -> rule2))] Fiona is young.[(triple11)] Harry is furry.[(triple12)] Harry is kind.[(triple13)] Harry is red.[(triple14 OR ((triple16) -> rule2))] Harry is smart.[(triple15)] Harry is young.[(triple16)] @1: Anne is red.[(((triple5) -> rule2) OR ((triple3 triple5) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is not cold.
("Dave" "is" "cold" "-")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
((triple11) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple16) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Anne is red.
("Anne" "is" "red" "+")
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1