Anne is furry. Anne is kind. Anne is quiet. Anne is rough. Anne is smart. Anne is young. Bob is blue. Bob is furry. Bob is kind. Bob is quiet. Bob is rough. Bob is young. Erin is blue. Erin is furry. Erin is kind. Erin is quiet. Rough, blue people are smart. Blue, quiet people are smart. If someone is smart and kind then they are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Rough, blue people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Blue, quiet people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and kind then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Erin is furry.
True
1
proof
[(triple14 OR ((((triple13 triple16) -> rule2) triple15) -> rule3))]
("Erin" "is" "furry" "+")
triple14
((((triple13 triple16) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Bob is not quiet.
False
1
inv-proof
[(triple10)]
("Bob" "is" "quiet" "-")
triple10
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is furry.[(triple1 OR ((triple5 triple2) -> rule3))] Anne is kind.[(triple2)] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5)] Anne is young.[(triple6)] Bob is blue.[(triple7)] Bob is furry.[(triple8 OR ((((triple11 triple7) -> rule1) triple9) -> rule3) OR ((((triple7 triple10) -> rule2) triple9) -> rule3))] Bob is kind.[(triple9)] Bob is quiet.[(triple10)] Bob is rough.[(triple11)] Bob is young.[(triple12)] Erin is blue.[(triple13)] Erin is furry.[(triple14 OR ((((triple13 triple16) -> rule2) triple15) -> rule3))] Erin is kind.[(triple15)] Erin is quiet.[(triple16)] @1: Bob is smart.[(((triple11 triple7) -> rule1) OR ((triple7 triple10) -> rule2))] Erin is smart.[(((triple13 triple16) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple5 triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is blue.
("Bob" "is" "blue" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
triple8
((((triple11 triple7) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple7 triple10) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple9
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
triple11
Bob is young.
("Bob" "is" "young" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
triple13
Erin is furry.
("Erin" "is" "furry" "+")
triple14
((((triple13 triple16) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple15
Erin is quiet.
("Erin" "is" "quiet" "+")
triple16
Bob is smart.
("Bob" "is" "smart" "+")
((triple11 triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple7 triple10) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple13 triple16) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1