Anne is big. Anne is blue. Anne is furry. Anne is kind. Anne is quiet. Charlie is big. Charlie is blue. Charlie is furry. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is white. Harry is blue. Harry is quiet. Harry is white. All quiet, blue things are white. All furry things are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
All quiet, blue things are white.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Harry is blue.
True
1
proof
[(triple13)]
("Harry" "is" "blue" "+")
triple13
Charlie is not kind.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "kind" "-")
triple9
Anne is white.
True
3
proof
[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not white.
False
3
inv-proof
[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple3) -> rule2))] Anne is furry.[(triple3)] Anne is kind.[(triple4)] Anne is quiet.[(triple5)] Charlie is big.[(triple6)] Charlie is blue.[(triple7 OR ((triple8) -> rule2))] Charlie is furry.[(triple8)] Charlie is kind.[(triple9)] Charlie is quiet.[(triple10)] Charlie is red.[(triple11)] Charlie is white.[(triple12 OR ((triple10 triple7) -> rule1) OR ((triple10 ((triple8) -> rule2)) -> rule1))] Harry is blue.[(triple13)] Harry is quiet.[(triple14)] Harry is white.[(triple15 OR ((triple14 triple13) -> rule1))] @1: Anne is white.[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple10 triple7) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple10 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple14 triple13) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2