Anne is big. Anne is blue. Anne is cold. Anne is quiet. Anne is smart. Charlie is blue. Charlie is cold. Charlie is quiet. Charlie is rough. Charlie is smart. Dave is big. Dave is blue. Dave is cold. Dave is furry. Dave is rough. Dave is smart. Rough things are furry. All blue, furry things are smart. If Charlie is cold then Charlie is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All blue, furry things are smart.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Charlie is cold then Charlie is big.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "big" "+"))
Charlie is smart.
True
1
proof
[(triple10 OR ((triple6 ((triple9) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "+")
triple10
((triple6 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Anne is not smart.
False
1
inv-proof
[(triple5)]
("Anne" "is" "smart" "-")
triple5
Charlie is furry.
True
2
proof
[(((triple9) -> rule1))]
("Charlie" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple7) -> rule3))]
("Charlie" "is" "big" "-")
((triple7) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is cold.[(triple3)] Anne is quiet.[(triple4)] Anne is smart.[(triple5)] Charlie is blue.[(triple6)] Charlie is cold.[(triple7)] Charlie is quiet.[(triple8)] Charlie is rough.[(triple9)] Charlie is smart.[(triple10 OR ((triple6 ((triple9) -> rule1)) -> rule2))] Dave is big.[(triple11)] Dave is blue.[(triple12)] Dave is cold.[(triple13)] Dave is furry.[(triple14 OR ((triple15) -> rule1))] Dave is rough.[(triple15)] Dave is smart.[(triple16 OR ((triple12 triple14) -> rule2) OR ((triple12 ((triple15) -> rule1)) -> rule2))] @1: Charlie is big.[(((triple7) -> rule3))] Charlie is furry.[(((triple9) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
((triple6 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
triple13
Dave is furry.
("Dave" "is" "furry" "+")
triple14
((triple15) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple15
Dave is smart.
("Dave" "is" "smart" "+")
triple16
((triple12 triple14) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple12 ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1