Anne is big. Anne is cold. Anne is nice. Anne is quiet. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is round. If something is red then it is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple9)]
("Charlie" "is" "red" "+")
triple9
Charlie is not furry.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "furry" "-")
triple6
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Charlie is cold.[(triple5)] Charlie is furry.[(triple6)] Charlie is nice.[(triple7)] Charlie is quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is round.[(triple10)] @1: Charlie is big.[(((triple9) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Charlie is big.
("Charlie" "is" "big" "+")
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1