Charlie is kind. Charlie is red. Charlie is not young. Dave is not red. Dave is rough. Dave is young. Erin is green. Erin is kind. Erin is nice. Erin is red. Erin is not rough. Gary is not green. Gary is not nice. Gary is red. Gary is not young. If something is rough and nice then it is not kind. Kind things are green. Red, rough things are not green. If Dave is kind and Dave is green then Dave is blue. Rough things are young. If something is kind and not rough then it is nice. If something is young and not kind then it is not blue. Nice, green things are blue.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Gary is not green.
("Gary" "is" "green" "-")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is not young.
("Gary" "is" "young" "-")
If something is rough and nice then it is not kind.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Red, rough things are not green.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "-"))
If Dave is kind and Dave is green then Dave is blue.
((("Dave" "is" "kind" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "blue" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is kind and not rough then it is nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "nice" "+"))
If something is young and not kind then it is not blue.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "-"))
Nice, green things are blue.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Gary is not nice.
True
1
proof
[(triple13)]
("Gary" "is" "nice" "-")
triple13
Gary is young.
False
1
inv-proof
[(triple15)]
("Gary" "is" "young" "+")
triple15
Erin is blue.
True
3
proof
[(((triple9 triple7) -> rule8) OR ((triple9 ((triple8) -> rule2)) -> rule8) OR ((((triple8 triple11) -> rule6) triple7) -> rule8) OR ((((triple8 triple11) -> rule6) ((triple8) -> rule2)) -> rule8))]
("Erin" "is" "blue" "+")
((triple9 triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple9 ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8 triple11) -> (rule6 % int2)) triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple8 triple11) -> (rule6 % int3)) ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not blue.
False
3
inv-proof
[(((triple9 triple7) -> rule8) OR ((triple9 ((triple8) -> rule2)) -> rule8) OR ((((triple8 triple11) -> rule6) triple7) -> rule8) OR ((((triple8 triple11) -> rule6) ((triple8) -> rule2)) -> rule8))]
("Erin" "is" "blue" "-")
((triple9 triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple9 ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8 triple11) -> (rule6 % int2)) triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple8 triple11) -> (rule6 % int3)) ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Charlie is kind.[(triple1)] Charlie is not young.[(triple3)] Charlie is red.[(triple2)] Dave is not red.[(triple4)] Dave is rough.[(triple5)] Dave is young.[(triple6 OR ((triple5) -> rule5))] Erin is green.[(triple7 OR ((triple8) -> rule2))] Erin is kind.[(triple8)] Erin is nice.[(triple9 OR ((triple8 triple11) -> rule6))] Erin is not rough.[(triple11)] Erin is red.[(triple10)] Gary is not green.[(triple12)] Gary is not nice.[(triple13)] Gary is not young.[(triple15)] Gary is red.[(triple14)] @1: Charlie is green.[(((triple1) -> rule2))] Erin is blue.[(((triple9 triple7) -> rule8) OR ((triple9 ((triple8) -> rule2)) -> rule8) OR ((((triple8 triple11) -> rule6) triple7) -> rule8) OR ((((triple8 triple11) -> rule6) ((triple8) -> rule2)) -> rule8))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is not young.
("Charlie" "is" "young" "-")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple8 triple11) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple10
Gary is not green.
("Gary" "is" "green" "-")
triple12
Gary is not nice.
("Gary" "is" "nice" "-")
triple13
Gary is not young.
("Gary" "is" "young" "-")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple14
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple9 triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple9 ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8 triple11) -> (rule6 % int2)) triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple8 triple11) -> (rule6 % int3)) ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3