Bob always goes out of his way to show that he is kind to people. Charlie is a rough but very kind and blue person. Dave who is considered nice was feeling rather rough today. Gary always goes out of his way to show that he is kind to people. Blue Christmas ornaments are also red. People who are green and blue tend to be round in shape. If someone is blue, young, and rough, they qualify as being round. Rough people will often be blue.  They thrive on being kind and nice. All nice people are young. It's true that green and blue people are also red people.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is green and blue then they are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and young and blue then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and kind and blue then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is green and blue then they are red.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Gary is kind.
True
1
proof
[(triple7)]
("Gary" "is" "kind" "+")
triple7
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Dave is young.
True
2
proof
[(((triple6) -> rule5))]
("Dave" "is" "young" "+")
((triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is not nice.
False
4
inv-proof
[(((triple2 triple3 triple4) -> rule4))]
("Charlie" "is" "nice" "-")
((triple2 triple3 triple4) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
True
5
proof
[(((((triple2 triple3 triple4) -> rule4)) -> rule5))]
("Charlie" "is" "young" "+")
((((triple2 triple3 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not young.
False
5
inv-proof
[(((((triple2 triple3 triple4) -> rule4)) -> rule5))]
("Charlie" "is" "young" "-")
((((triple2 triple3 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
True
8
proof
[(((triple2 ((((triple2 triple3 triple4) -> rule4)) -> rule5) triple4) -> rule3))]
("Charlie" "is" "round" "+")
((triple2 ((((triple2 triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not round.
False
8
inv-proof
[(((triple2 ((((triple2 triple3 triple4) -> rule4)) -> rule5) triple4) -> rule3))]
("Charlie" "is" "round" "-")
((triple2 ((((triple2 triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Charlie is blue.[(triple4)] Charlie is kind.[(triple3)] Charlie is rough.[(triple2)] Dave is nice.[(triple6)] Dave is rough.[(triple5)] Gary is kind.[(triple7)] @1: Charlie is nice.[(((triple2 triple3 triple4) -> rule4))] Charlie is red.[(((triple4) -> rule1))] Dave is young.[(((triple6) -> rule5))] @2: Charlie is young.[(((((triple2 triple3 triple4) -> rule4)) -> rule5))] @3: Charlie is round.[(((triple2 ((((triple2 triple3 triple4) -> rule4)) -> rule5) triple4) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2 triple3 triple4) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2 triple3 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple2 ((((triple2 triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Bob always goes out of his way to show that he is kind to people.
Charlie is a rough but very kind and blue person.
Dave who is considered nice was feeling rather rough today.
Gary always goes out of his way to show that he is kind to people.
Blue Christmas ornaments are also red.
People who are green and blue tend to be round in shape.
If someone is blue, young, and rough, they qualify as being round.
Rough people will often be blue; They thrive on being kind and nice.
All nice people are young.
It's true that green and blue people are also red people.