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