Bob is a blue but young, round man but is also cold and big. In the snow sits Dave, crying from being cold. Fred's skin turned blue and green in a lab accident.  Despite his outward appearance, he is really nice. Gary is so big, he is often blue, but always kind. Whoever is rough and red must be kind. A blue person who is feeling a bit rough and cold will be wearing red. People who are round, blue and cold are usually nice. If a big person is cold and nice, then they are green. Kind people who are nice find that they must also be rough. A person who is young and cold and green is kind.
Bob is young.
("Bob" "is" "young" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is big.
("Bob" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Fred is nice.
("Fred" "is" "nice" "+")
Fred is green.
("Fred" "is" "green" "+")
Fred is blue.
("Fred" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
If someone is rough and red then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and cold and rough then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is round and blue and cold then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and big and nice then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is kind and nice then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and young and cold then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Fred is green.
True
1
proof
[(triple8)]
("Fred" "is" "green" "+")
triple8
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Bob is nice.
True
4
proof
[(((triple2 triple4 triple3) -> rule3))]
("Bob" "is" "nice" "+")
((triple2 triple4 triple3) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
4
inv-proof
[(((triple2 triple4 triple3) -> rule3))]
("Bob" "is" "nice" "-")
((triple2 triple4 triple3) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
True
7
proof
[(((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4))]
("Bob" "is" "green" "+")
((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not green.
False
7
inv-proof
[(((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4))]
("Bob" "is" "green" "-")
((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
True
10
proof
[(((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6))]
("Bob" "is" "kind" "+")
((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple1 triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not kind.
False
10
inv-proof
[(((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6))]
("Bob" "is" "kind" "-")
((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple1 triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is rough.
True
15
proof
[(((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5))]
("Bob" "is" "rough" "+")
((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule4 % int3)) triple1 triple3) -> (rule6 % int2)) ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is not rough.
False
15
inv-proof
[(((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5))]
("Bob" "is" "rough" "-")
((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule4 % int3)) triple1 triple3) -> (rule6 % int2)) ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is red.
True
18
proof
[(((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "red" "+")
((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule4 % int4)) triple1 triple3) -> (rule6 % int3)) ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Bob is not red.
False
18
inv-proof
[(((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "red" "-")
((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule4 % int4)) triple1 triple3) -> (rule6 % int3)) ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Fred is not red.
Unknown
inv-rconc
[@1: Fred is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fred" "is" "red" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Fred is not kind.
Unknown
inv-rconc
[@2: Fred is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fred" "is" "kind" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Fred is not round.
Unknown
inv-random
[@0: Fred is round.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Fred is not cold.
Unknown
inv-random
[@0: Fred is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "cold" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is big.[(triple5)] Bob is blue.[(triple4)] Bob is cold.[(triple3)] Bob is round.[(triple2)] Bob is young.[(triple1)] Dave is cold.[(triple6)] Fred is blue.[(triple9)] Fred is green.[(triple8)] Fred is nice.[(triple7)] Gary is big.[(triple12)] Gary is blue.[(triple11)] Gary is kind.[(triple10)] @1: Bob is nice.[(((triple2 triple4 triple3) -> rule3))] @2: Bob is green.[(((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4))] @3: Bob is kind.[(((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6))] @4: Bob is rough.[(((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5))] @5: Bob is red.[(((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> rule3)) -> rule4) triple1 triple3) -> rule6) ((triple2 triple4 triple3) -> rule3)) -> rule5)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Fred is blue.
("Fred" "is" "blue" "+")
triple9
Fred is green.
("Fred" "is" "green" "+")
triple8
Fred is nice.
("Fred" "is" "nice" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple4 triple3) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple1 triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule4 % int3)) triple1 triple3) -> (rule6 % int2)) ((triple2 triple4 triple3) -> (rule3 % int4))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((triple4 triple3 ((((((triple3 triple5 ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule4 % int4)) triple1 triple3) -> (rule6 % int3)) ((triple2 triple4 triple3) -> (rule3 % int5))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Bob is a blue but young, round man but is also cold and big.
In the snow sits Dave, crying from being cold.
Fred's skin turned blue and green in a lab accident; Despite his outward appearance, he is really nice.
Gary is so big, he is often blue, but always kind.
Whoever is rough and red must be kind.
A blue person who is feeling a bit rough and cold will be wearing red.
People who are round, blue and cold are usually nice.
If a big person is cold and nice, then they are green.
Kind people who are nice find that they must also be rough.
A person who is young and cold and green is kind.