Anne is big. Anne is blue. Anne is furry. Anne is red. Anne is round. Bob is big. Bob is furry. Charlie is not blue. Charlie is furry. Charlie is smart. Gary is big. Gary is not furry. Gary is red. Gary is not smart. Gary is not young. If something is young and not furry then it is blue. Big things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is not young.
("Gary" "is" "young" "-")
If something is young and not furry then it is blue.
((("something" "is" "young" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Bob is furry.
True
1
proof
[(triple7)]
("Bob" "is" "furry" "+")
triple7
Bob is not furry.
False
1
inv-proof
[(triple7)]
("Bob" "is" "furry" "-")
triple7
Bob is round.
True
2
proof
[(((triple6) -> rule2))]
("Bob" "is" "round" "+")
((triple6) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple6) -> rule2))]
("Bob" "is" "round" "-")
((triple6) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5 OR ((triple1) -> rule2))] Bob is big.[(triple6)] Bob is furry.[(triple7)] Charlie is furry.[(triple9)] Charlie is not blue.[(triple8)] Charlie is smart.[(triple10)] Gary is big.[(triple11)] Gary is not furry.[(triple12)] Gary is not smart.[(triple14)] Gary is not young.[(triple15)] Gary is red.[(triple13)] @1: Bob is round.[(((triple6) -> rule2))] Gary is round.[(((triple11) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is not furry.
("Gary" "is" "furry" "-")
triple12
Gary is not smart.
("Gary" "is" "smart" "-")
triple14
Gary is not young.
("Gary" "is" "young" "-")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple13
Bob is round.
("Bob" "is" "round" "+")
((triple6) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple11) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1