Bob is big. Bob is furry. Bob is green. Bob is quiet. Bob is red. Bob is round. Charlie is big. Charlie is blue. Charlie is furry. Charlie is quiet. All red people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Charlie is blue.
True
1
proof
[(triple8)]
("Charlie" "is" "blue" "+")
triple8
Charlie is not big.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "big" "-")
triple7
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is big.[(triple1 OR ((triple5) -> rule1))] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is round.[(triple6)] Charlie is big.[(triple7)] Charlie is blue.[(triple8)] Charlie is furry.[(triple9)] Charlie is quiet.[(triple10)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10