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