Anne is green. Dave is green. Dave is nice. Dave is quiet. Dave is smart. Fiona is green. Fiona is quiet. Fiona is smart. Harry is cold. Harry is green. Harry is kind. Harry is nice. Harry is quiet. Harry is red. Harry is smart. All cold, quiet people are red. If someone is green then they are red. If someone is smart then they are kind.
Anne is green.
("Anne" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All cold, quiet people are red.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Fiona is not quiet.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "quiet" "-")
triple7
Fiona is red.
True
2
proof
[(((triple6) -> rule2))]
("Fiona" "is" "red" "+")
((triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "red" "-")
((triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is green.[(triple1)] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Fiona is green.[(triple6)] Fiona is quiet.[(triple7)] Fiona is smart.[(triple8)] Harry is cold.[(triple9)] Harry is green.[(triple10)] Harry is kind.[(triple11 OR ((triple15) -> rule3))] Harry is nice.[(triple12)] Harry is quiet.[(triple13)] Harry is red.[(triple14 OR ((triple10) -> rule2) OR ((triple9 triple13) -> rule1))] Harry is smart.[(triple15)] @1: Anne is red.[(((triple1) -> rule2))] Dave is kind.[(((triple5) -> rule3))] Dave is red.[(((triple2) -> rule2))] Fiona is kind.[(((triple8) -> rule3))] Fiona is red.[(((triple6) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
((triple15) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple13) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1