Anne is furry. Anne is green. Anne is kind. Anne is red. Anne is rough. Anne is white. Erin is red. Red things are white. If something is white then it is big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Anne is red.
True
1
proof
[(triple4)]
("Anne" "is" "red" "+")
triple4
Erin is not red.
False
1
inv-proof
[(triple7)]
("Erin" "is" "red" "-")
triple7
Erin is white.
True
2
proof
[(((triple7) -> rule1))]
("Erin" "is" "white" "+")
((triple7) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is big.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("Erin" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Erin" "is" "big" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is red.[(triple4)] Anne is rough.[(triple5)] Anne is white.[(triple6 OR ((triple4) -> rule1))] Erin is red.[(triple7)] @1: Anne is big.[(((triple6) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Erin is white.[(((triple7) -> rule1))] @2: Erin is big.[(((((triple7) -> rule1)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2