Anne is blue. Anne is furry. Anne is green. Anne is kind. Anne is red. Anne is smart. Charlie is furry. Charlie is green. Charlie is kind. Charlie is red. Charlie is smart. Harry is blue. Harry is green. Harry is kind. Harry is quiet. All red things are green. If Harry is green then Harry is quiet. Blue, smart things are kind. Smart, blue things are kind. If something is blue then it is quiet. All green, furry things are red. If Harry is kind and Harry is furry then Harry is green. If something is green and furry then it is red.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Harry is green then Harry is quiet.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "quiet" "+"))
Blue, smart things are kind.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Smart, blue things are kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All green, furry things are red.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Harry is kind and Harry is furry then Harry is green.
((("Harry" "is" "kind" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "green" "+"))
If something is green and furry then it is red.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "kind" "-")
triple9
Anne is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3 OR ((triple5) -> rule1))] Anne is kind.[(triple4 OR ((triple1 triple6) -> rule3) OR ((triple6 triple1) -> rule4))] Anne is red.[(triple5 OR ((triple3 triple2) -> rule6) OR ((triple3 triple2) -> rule8))] Anne is smart.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8 OR ((triple10) -> rule1))] Charlie is kind.[(triple9)] Charlie is red.[(triple10 OR ((triple8 triple7) -> rule6) OR ((triple8 triple7) -> rule8))] Charlie is smart.[(triple11)] Harry is blue.[(triple12)] Harry is green.[(triple13)] Harry is kind.[(triple14)] Harry is quiet.[(triple15 OR ((triple12) -> rule5) OR ((triple13) -> rule2))] @1: Anne is quiet.[(((triple1) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple5) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple1 triple6) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple6 triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple3 triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple2) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple10) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple8 triple7) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple8 triple7) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
((triple12) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple13) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1