Anne is big. Anne is blue. Anne is nice. Anne is quiet. Anne is red. Anne is round. Bob is big. Bob is blue. Bob is furry. Bob is nice. Bob is quiet. Erin is big. Erin is quiet. Erin is round. Gary is big. Gary is round. If something is round then it is blue. If something is blue then it is nice. If something is nice and round then it is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is nice and round then it is furry.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Anne is nice.
True
1
proof
[(triple3 OR ((triple2) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
("Anne" "is" "nice" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is furry.
True
3
proof
[(((triple3 triple6) -> rule3) OR ((((triple2) -> rule2) triple6) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple6) -> rule3))]
("Anne" "is" "furry" "+")
((triple3 triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not furry.
False
3
inv-proof
[(((triple3 triple6) -> rule3) OR ((((triple2) -> rule2) triple6) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple6) -> rule3))]
("Anne" "is" "furry" "-")
((triple3 triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Gary is nice.
True
3
proof
[(((((triple16) -> rule1)) -> rule2))]
("Gary" "is" "nice" "+")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule2))]
("Erin" "is" "nice" "-")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
True
5
proof
[(((((((triple14) -> rule1)) -> rule2) triple14) -> rule3))]
("Erin" "is" "furry" "+")
((((((triple14) -> (rule1 % int3))) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Gary is not furry.
False
5
inv-proof
[(((((((triple16) -> rule1)) -> rule2) triple16) -> rule3))]
("Gary" "is" "furry" "-")
((((((triple16) -> (rule1 % int3))) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple6) -> rule1))] Anne is nice.[(triple3 OR ((triple2) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Anne is quiet.[(triple4)] Anne is red.[(triple5)] Anne is round.[(triple6)] Bob is big.[(triple7)] Bob is blue.[(triple8)] Bob is furry.[(triple9)] Bob is nice.[(triple10 OR ((triple8) -> rule2))] Bob is quiet.[(triple11)] Erin is big.[(triple12)] Erin is quiet.[(triple13)] Erin is round.[(triple14)] Gary is big.[(triple15)] Gary is round.[(triple16)] @1: Anne is furry.[(((triple3 triple6) -> rule3) OR ((((triple2) -> rule2) triple6) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple6) -> rule3))] Erin is blue.[(((triple14) -> rule1))] Gary is blue.[(((triple16) -> rule1))] @2: Erin is nice.[(((((triple14) -> rule1)) -> rule2))] Gary is nice.[(((((triple16) -> rule1)) -> rule2))] @3: Erin is furry.[(((((((triple14) -> rule1)) -> rule2) triple14) -> rule3))] Gary is furry.[(((((((triple16) -> rule1)) -> rule2) triple16) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple6) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
triple8
Bob is furry.
("Bob" "is" "furry" "+")
triple9
Bob is nice.
("Bob" "is" "nice" "+")
triple10
((triple8) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
Erin is round.
("Erin" "is" "round" "+")
triple14
Gary is big.
("Gary" "is" "big" "+")
triple15
Gary is round.
("Gary" "is" "round" "+")
triple16
Anne is furry.
("Anne" "is" "furry" "+")
((triple3 triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((triple14) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple16) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple14) -> (rule1 % int3))) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple16) -> (rule1 % int3))) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3