Anne is quiet. Anne is red. Dave is big. Dave is not cold. Dave is green. Dave is nice. Dave is quiet. Dave is red. Dave is smart. Erin is big. Erin is not cold. Erin is green. Erin is nice. Erin is red. Erin is smart. Harry is nice. If Harry is smart then Harry is quiet. If something is quiet and smart then it is red. If Dave is green then Dave is smart. All green things are nice. Green things are nice. If Harry is quiet then Harry is red. If Harry is quiet and Harry is not cold then Harry is not smart. If Dave is smart then Dave is big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
If something is quiet and smart then it is red.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If Dave is green then Dave is smart.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "smart" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Harry is quiet then Harry is red.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "red" "+"))
If Harry is quiet and Harry is not cold then Harry is not smart.
((("Harry" "is" "quiet" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "smart" "-"))
If Dave is smart then Dave is big.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple9 OR ((triple5) -> rule3))]
("Dave" "is" "smart" "+")
triple9
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule4) OR ((triple5) -> rule5))]
("Dave" "is" "nice" "-")
triple6
((triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Dave is big.[(triple3 OR ((triple9) -> rule8) OR ((((triple5) -> rule3)) -> rule8))] Dave is green.[(triple5)] Dave is nice.[(triple6 OR ((triple5) -> rule4) OR ((triple5) -> rule5))] Dave is not cold.[(triple4)] Dave is quiet.[(triple7)] Dave is red.[(triple8 OR ((triple7 triple9) -> rule2) OR ((triple7 ((triple5) -> rule3)) -> rule2))] Dave is smart.[(triple9 OR ((triple5) -> rule3))] Erin is big.[(triple10)] Erin is green.[(triple12)] Erin is nice.[(triple13 OR ((triple12) -> rule4) OR ((triple12) -> rule5))] Erin is not cold.[(triple11)] Erin is red.[(triple14)] Erin is smart.[(triple15)] Harry is nice.[(triple16)]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
((triple9) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple7 triple9) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple7 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
triple13
((triple12) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple12) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple14
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Harry is nice.
("Harry" "is" "nice" "+")
triple16