Anne is furry. Anne is green. Anne is quiet. Anne is red. Anne is young. Charlie is furry. Charlie is quiet. Charlie is smart. Charlie is white. Charlie is young. All quiet, smart people are red. All smart people are quiet. If someone is quiet then they are green.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All quiet, smart people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "smart" "-")
triple8
Charlie is green.
True
2
proof
[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((triple7) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not green.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Charlie" "is" "green" "-")
((triple7) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2 OR ((triple3) -> rule3))] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is young.[(triple5)] Charlie is furry.[(triple6)] Charlie is quiet.[(triple7 OR ((triple8) -> rule2))] Charlie is smart.[(triple8)] Charlie is white.[(triple9)] Charlie is young.[(triple10)] @1: Charlie is green.[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] Charlie is red.[(((triple7 triple8) -> rule1) OR ((((triple8) -> rule2) triple8) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
((triple7) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple7 triple8) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2