Anne is big. Anne is blue. Anne is furry. Anne is not nice. Anne is quiet. Anne is red. Bob is big. Bob is blue. Bob is furry. Bob is quiet. Erin is big. Erin is blue. Erin is not nice. Erin is quiet. Erin is red. Nice, red people are not big. If someone is blue then they are big. All quiet people are furry. If Bob is red and Bob is nice then Bob is not quiet. If Bob is furry then Bob is red. If Bob is blue then Bob is red. If Bob is furry and Bob is not quiet then Bob is smart. If Bob is quiet and Bob is red then Bob is not smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Nice, red people are not big.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "-"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Bob is red and Bob is nice then Bob is not quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "quiet" "-"))
If Bob is furry then Bob is red.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "red" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
If Bob is furry and Bob is not quiet then Bob is smart.
((("Bob" "is" "furry" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "smart" "+"))
If Bob is quiet and Bob is red then Bob is not smart.
((("Bob" "is" "quiet" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "smart" "-"))
Erin is big.
True
1
proof
[(triple11 OR ((triple12) -> rule2))]
("Erin" "is" "big" "+")
triple11
((triple12) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not quiet.
False
1
inv-proof
[(triple14)]
("Erin" "is" "quiet" "-")
triple14
Erin is furry.
True
2
proof
[(((triple14) -> rule3))]
("Erin" "is" "furry" "+")
((triple14) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple14) -> rule3))]
("Erin" "is" "furry" "-")
((triple14) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is not smart.
True
4
proof
[(((triple10 ((triple8) -> rule6)) -> rule8) OR ((triple10 ((triple9) -> rule5)) -> rule8) OR ((triple10 ((((triple10) -> rule3)) -> rule5)) -> rule8))]
("Bob" "is" "smart" "-")
((triple10 ((triple8) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
False
4
inv-proof
[(((triple10 ((triple8) -> rule6)) -> rule8) OR ((triple10 ((triple9) -> rule5)) -> rule8) OR ((triple10 ((((triple10) -> rule3)) -> rule5)) -> rule8))]
("Bob" "is" "smart" "+")
((triple10 ((triple8) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule2))] Anne is blue.[(triple2)] Anne is furry.[(triple3 OR ((triple5) -> rule3))] Anne is not nice.[(triple4)] Anne is quiet.[(triple5)] Anne is red.[(triple6)] Bob is big.[(triple7 OR ((triple8) -> rule2))] Bob is blue.[(triple8)] Bob is furry.[(triple9 OR ((triple10) -> rule3))] Bob is quiet.[(triple10)] Erin is big.[(triple11 OR ((triple12) -> rule2))] Erin is blue.[(triple12)] Erin is not nice.[(triple13)] Erin is quiet.[(triple14)] Erin is red.[(triple15)] @1: Bob is red.[(((triple8) -> rule6) OR ((triple9) -> rule5) OR ((((triple10) -> rule3)) -> rule5))] Erin is furry.[(((triple14) -> rule3))] @2: Bob is not smart.[(((triple10 ((triple8) -> rule6)) -> rule8) OR ((triple10 ((triple9) -> rule5)) -> rule8) OR ((triple10 ((((triple10) -> rule3)) -> rule5)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple5) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple6
Bob is big.
("Bob" "is" "big" "+")
triple7
((triple8) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple8
Bob is furry.
("Bob" "is" "furry" "+")
triple9
((triple10) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple12) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple12
Erin is not nice.
("Erin" "is" "nice" "-")
triple13
Erin is quiet.
("Erin" "is" "quiet" "+")
triple14
Erin is red.
("Erin" "is" "red" "+")
triple15
Bob is red.
("Bob" "is" "red" "+")
((triple8) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple9) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple14) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((triple10 ((triple8) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3