Anne is blue. Anne is furry. Anne is green. Anne is kind. Anne is round. Anne is smart. Charlie is big. Charlie is blue. Charlie is smart. Harry is blue. Harry is furry. Harry is green. If something is blue then it is round. If something is big and furry then it is green. All green things are round.
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 round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is big and furry then it is green.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple5 OR ((triple1) -> rule1) OR ((triple3) -> rule3))]
("Anne" "is" "round" "+")
triple5
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule1) OR ((triple3) -> rule3))]
("Anne" "is" "round" "-")
triple5
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is round.[(triple5 OR ((triple1) -> rule1) OR ((triple3) -> rule3))] Anne is smart.[(triple6)] Charlie is big.[(triple7)] Charlie is blue.[(triple8)] Charlie is smart.[(triple9)] Harry is blue.[(triple10)] Harry is furry.[(triple11)] Harry is green.[(triple12)] @1: Charlie is round.[(((triple8) -> rule1))] Harry is round.[(((triple10) -> rule1) OR ((triple12) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
((triple8) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple10) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1