Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is kind. Anne is not nice. Anne is not quiet. Dave is cold. Dave is furry. Dave is quiet. Gary is big. Gary is blue. Gary is cold. Gary is furry. Gary is quiet. If someone is big then they are kind. Furry people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Gary is blue.
True
1
proof
[(triple12)]
("Gary" "is" "blue" "+")
triple12
Anne is not kind.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule1) OR ((((triple4) -> rule2)) -> rule1))]
("Anne" "is" "kind" "-")
triple5
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Gary is kind.
True
2
proof
[(((triple11) -> rule1) OR ((((triple14) -> rule2)) -> rule1))]
("Gary" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not big.
False
2
inv-proof
[(((triple9) -> rule2))]
("Dave" "is" "big" "-")
((triple9) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
True
3
proof
[(((((triple9) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule2))] Anne is blue.[(triple2)] Anne is cold.[(triple3)] Anne is furry.[(triple4)] Anne is kind.[(triple5 OR ((triple1) -> rule1) OR ((((triple4) -> rule2)) -> rule1))] Anne is not nice.[(triple6)] Anne is not quiet.[(triple7)] Dave is cold.[(triple8)] Dave is furry.[(triple9)] Dave is quiet.[(triple10)] Gary is big.[(triple11 OR ((triple14) -> rule2))] Gary is blue.[(triple12)] Gary is cold.[(triple13)] Gary is furry.[(triple14)] Gary is quiet.[(triple15)] @1: Dave is big.[(((triple9) -> rule2))] Gary is kind.[(((triple11) -> rule1) OR ((((triple14) -> rule2)) -> rule1))] @2: Dave is kind.[(((((triple9) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
triple5
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
triple6
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
((triple14) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is furry.
("Gary" "is" "furry" "+")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Dave is big.
("Dave" "is" "big" "+")
((triple9) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2