Bob is green. Bob is quiet. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is rough. Dave is round. Erin is not blue. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Erin is not round. If someone is green then they are not blue. If someone is rough and kind then they are not blue. If Bob is rough and Bob is round then Bob is not nice. Kind, quiet people are rough. If someone is nice and not quiet then they are kind. If Bob is blue then Bob is round.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not round.
("Erin" "is" "round" "-")
If someone is green then they are not blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
If someone is rough and kind then they are not blue.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
If Bob is rough and Bob is round then Bob is not nice.
((("Bob" "is" "rough" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "nice" "-"))
Kind, quiet people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and not quiet then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "kind" "+"))
If Bob is blue then Bob is round.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
Erin is nice.
True
1
proof
[(triple12)]
("Erin" "is" "nice" "+")
triple12
Erin is blue.
False
1
inv-proof
[(triple9 OR ((triple10) -> rule1) OR ((triple14 triple11) -> rule2) OR ((((triple11 triple13) -> rule4) triple11) -> rule2))]
("Erin" "is" "blue" "+")
triple9
((triple10) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((triple14 triple11) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((((triple11 triple13) -> (rule4 % int2)) triple11) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2)] Dave is green.[(triple3)] Dave is kind.[(triple4)] Dave is nice.[(triple5)] Dave is quiet.[(triple6)] Dave is rough.[(triple7 OR ((triple4 triple6) -> rule4))] Dave is round.[(triple8)] Erin is green.[(triple10)] Erin is kind.[(triple11)] Erin is nice.[(triple12)] Erin is not blue.[(triple9 OR ((triple10) -> rule1) OR ((triple14 triple11) -> rule2) OR ((((triple11 triple13) -> rule4) triple11) -> rule2))] Erin is not round.[(triple15)] Erin is quiet.[(triple13)] Erin is rough.[(triple14 OR ((triple11 triple13) -> rule4))] @1: Bob is not blue.[(((triple1) -> rule1))] Dave is not blue.[(((triple3) -> rule1) OR ((triple7 triple4) -> rule2) OR ((((triple4 triple6) -> rule4) triple4) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((triple4 triple6) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is nice.
("Erin" "is" "nice" "+")
triple12
Erin is not blue.
("Erin" "is" "blue" "-")
triple9
((triple10) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((triple14 triple11) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((((triple11 triple13) -> (rule4 % int2)) triple11) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not round.
("Erin" "is" "round" "-")
triple15
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
Erin is rough.
("Erin" "is" "rough" "+")
triple14
((triple11 triple13) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
((triple7 triple4) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
((((triple4 triple6) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2