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