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