Anne is green. Anne is quiet. Anne is red. Anne is rough. Anne is smart. Bob is blue. Bob is not furry. Bob is quiet. Bob is red. Bob is smart. Erin is furry. Erin is green. Erin is not quiet. Erin is red. Erin is not rough. Erin is not smart. Quiet things are blue. If something is red and not quiet then it is not blue. If something is quiet and not red then it is not rough. If something is blue and rough then it is furry. If something is green and not quiet then it is furry. Rough things are smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is red and not quiet then it is not blue.
((("something" "is" "red" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "blue" "-"))
If something is quiet and not red then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "red" "~")) -> ("something" "is" "rough" "-"))
If something is blue and rough then it is furry.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is green and not quiet then it is furry.
((("something" "is" "green" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "furry" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple4)]
("Anne" "is" "rough" "-")
triple4
Erin is not blue.
True
3
proof
[(((triple14 triple13) -> rule2))]
("Erin" "is" "blue" "-")
((triple14 triple13) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is blue.
False
3
inv-proof
[(((triple14 triple13) -> rule2))]
("Erin" "is" "blue" "+")
((triple14 triple13) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Anne is furry.
True
4
proof
[(((((triple2) -> rule1) triple4) -> rule4))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not furry.
False
4
inv-proof
[(((((triple2) -> rule1) triple4) -> rule4))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5 OR ((triple4) -> rule6))] Bob is blue.[(triple6 OR ((triple8) -> rule1))] Bob is not furry.[(triple7)] Bob is quiet.[(triple8)] Bob is red.[(triple9)] Bob is smart.[(triple10)] Erin is furry.[(triple11 OR ((triple12 triple13) -> rule5))] Erin is green.[(triple12)] Erin is not quiet.[(triple13)] Erin is not rough.[(triple15)] Erin is not smart.[(triple16)] Erin is red.[(triple14)] @1: Anne is blue.[(((triple2) -> rule1))] Erin is not blue.[(((triple14 triple13) -> rule2))] @2: Anne is furry.[(((((triple2) -> rule1) triple4) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple4) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple6
((triple8) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple10
Erin is furry.
("Erin" "is" "furry" "+")
triple11
((triple12 triple13) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple12
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple13
Erin is not rough.
("Erin" "is" "rough" "-")
triple15
Erin is not smart.
("Erin" "is" "smart" "-")
triple16
Erin is red.
("Erin" "is" "red" "+")
triple14
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
((triple14 triple13) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2