Anne is kind. Anne is nice. Anne is red. Anne is round. Anne is white. Bob is green. Bob is nice. Bob is round. Dave is nice. Dave is quiet. Dave is red. Dave is round. Dave is white. Erin is green. Erin is kind. If something is round and white then it is nice. Green things are white. If something is red and not green then it is not white. If something is nice and not green then it is red. Round things are red. If something is white and green then it is round. All white, nice things are kind. Quiet, round things are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If something is round and white then it is nice.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is red and not green then it is not white.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "-"))
If something is nice and not green then it is red.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is white and green then it is round.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All white, nice things are kind.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Quiet, round things are kind.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Anne is nice.
True
1
proof
[(triple2 OR ((triple4 triple5) -> rule1))]
("Anne" "is" "nice" "+")
triple2
((triple4 triple5) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is not red.
False
1
inv-proof
[(triple11 OR ((triple12) -> rule5))]
("Dave" "is" "red" "-")
triple11
((triple12) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is red.
True
2
proof
[(((triple8) -> rule5) OR ((((((triple6) -> rule2) triple6) -> rule6)) -> rule5))]
("Bob" "is" "red" "+")
((triple8) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((((triple6) -> (rule2 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not white.
False
2
inv-proof
[(((triple6) -> rule2))]
("Bob" "is" "white" "-")
((triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is kind.[(triple1 OR ((triple5 triple2) -> rule7) OR ((triple5 ((triple4 triple5) -> rule1)) -> rule7))] Anne is nice.[(triple2 OR ((triple4 triple5) -> rule1))] Anne is red.[(triple3 OR ((triple4) -> rule5))] Anne is round.[(triple4)] Anne is white.[(triple5)] Bob is green.[(triple6)] Bob is nice.[(triple7 OR ((triple8 ((triple6) -> rule2)) -> rule1) OR ((((((triple6) -> rule2) triple6) -> rule6) ((triple6) -> rule2)) -> rule1))] Bob is round.[(triple8 OR ((((triple6) -> rule2) triple6) -> rule6))] Dave is nice.[(triple9 OR ((triple12 triple13) -> rule1))] Dave is quiet.[(triple10)] Dave is red.[(triple11 OR ((triple12) -> rule5))] Dave is round.[(triple12)] Dave is white.[(triple13)] Erin is green.[(triple14)] Erin is kind.[(triple15 OR ((((triple14) -> rule2) ((((((triple14) -> rule2) triple14) -> rule6) ((triple14) -> rule2)) -> rule1)) -> rule7))] @1: Bob is red.[(((triple8) -> rule5) OR ((((((triple6) -> rule2) triple6) -> rule6)) -> rule5))] Bob is white.[(((triple6) -> rule2))] Dave is kind.[(((triple10 triple12) -> rule8) OR ((triple13 triple9) -> rule7) OR ((triple13 ((triple12 triple13) -> rule1)) -> rule7))] Erin is white.[(((triple14) -> rule2))] @2: Bob is kind.[(((((triple6) -> rule2) triple7) -> rule7) OR ((((triple6) -> rule2) ((triple8 ((triple6) -> rule2)) -> rule1)) -> rule7) OR ((((triple6) -> rule2) ((((((triple6) -> rule2) triple6) -> rule6) ((triple6) -> rule2)) -> rule1)) -> rule7))] Erin is round.[(((((triple14) -> rule2) triple14) -> rule6))] @3: Erin is nice.[(((((((triple14) -> rule2) triple14) -> rule6) ((triple14) -> rule2)) -> rule1))] Erin is red.[(((((((triple14) -> rule2) triple14) -> rule6)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple5 triple2) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple4 triple5) -> (rule1 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple4 triple5) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple6) -> (rule2 % int3)) triple6) -> (rule6 % int2)) ((triple6) -> (rule2 % int3))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple8
((((triple6) -> (rule2 % int2)) triple6) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple12 triple13) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple11
((triple12) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple13
Erin is green.
("Erin" "is" "green" "+")
triple14
Erin is kind.
("Erin" "is" "kind" "+")
triple15
((((triple14) -> (rule2 % int4)) ((((((triple14) -> (rule2 % int4)) triple14) -> (rule6 % int3)) ((triple14) -> (rule2 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((triple8) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((((triple6) -> (rule2 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple10 triple12) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple13 triple9) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple13 ((triple12 triple13) -> (rule1 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple14) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple6) -> (rule2 % int2)) triple7) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple8 ((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple6) -> (rule2 % int4)) ((((((triple6) -> (rule2 % int4)) triple6) -> (rule6 % int3)) ((triple6) -> (rule2 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((((triple14) -> (rule2 % int2)) triple14) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple14) -> (rule2 % int3)) triple14) -> (rule6 % int2)) ((triple14) -> (rule2 % int3))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((((triple14) -> (rule2 % int3)) triple14) -> (rule6 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3