Alan is very nice to people, but he's also rather big. Young Bob is wearing green pants. Dave looks big and is kind with red hair and green shoes. Because Harry is so young, he is rough and cold when he can be round instead. A person who's big and kind will also be cold. People who are nice, round and wearing blue will have red cheeks. Any green person is a round person. A kind, cold, round person will be nice in addition. Nice people who are looking green and seeing red usually feel rather rough.
Alan is nice.
("Alan" "is" "nice" "+")
Alan is big.
("Alan" "is" "big" "+")
Bob is young.
("Bob" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is big and kind then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and round and blue then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and round and kind then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and green and red then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Dave is red.
True
1
proof
[(triple5)]
("Dave" "is" "red" "+")
triple5
Harry is not round.
False
1
inv-proof
[(triple10)]
("Harry" "is" "round" "-")
triple10
Bob is round.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "round" "+")
((triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple7) -> rule3))]
("Dave" "is" "round" "-")
((triple7) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
True
7
proof
[(((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4))]
("Dave" "is" "nice" "+")
((((triple8 triple6) -> (rule1 % int3)) ((triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not nice.
False
7
inv-proof
[(((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4))]
("Dave" "is" "nice" "-")
((((triple8 triple6) -> (rule1 % int3)) ((triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is rough.
True
10
proof
[(((((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4) triple7 triple5) -> rule5))]
("Dave" "is" "rough" "+")
((((((triple8 triple6) -> (rule1 % int4)) ((triple7) -> (rule3 % int3)) triple6) -> (rule4 % int2)) triple7 triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is not rough.
False
10
inv-proof
[(((((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4) triple7 triple5) -> rule5))]
("Dave" "is" "rough" "-")
((((((triple8 triple6) -> (rule1 % int4)) ((triple7) -> (rule3 % int3)) triple6) -> (rule4 % int2)) triple7 triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Alan is not red.
Unknown
inv-rconc
[@1: Alan is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Alan" "is" "red" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Alan is cold.
Unknown
rconc
[@1: Alan is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Alan" "is" "cold" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Alan is green.
Unknown
random
[@0: Alan is green.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "green" "+")
@0: Alan is big.[(triple2)] Alan is nice.[(triple1)] Bob is green.[(triple4)] Bob is young.[(triple3)] Dave is big.[(triple8)] Dave is green.[(triple7)] Dave is kind.[(triple6)] Dave is red.[(triple5)] Harry is cold.[(triple12)] Harry is rough.[(triple11)] Harry is round.[(triple10)] Harry is young.[(triple9)] @1: Bob is round.[(((triple4) -> rule3))] Dave is cold.[(((triple8 triple6) -> rule1))] Dave is round.[(((triple7) -> rule3))] @2: Dave is nice.[(((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4))] @3: Dave is rough.[(((((((triple8 triple6) -> rule1) ((triple7) -> rule3) triple6) -> rule4) triple7 triple5) -> rule5))]
Alan is big.
("Alan" "is" "big" "+")
triple2
Alan is nice.
("Alan" "is" "nice" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
triple9
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple8 triple6) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple7) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple8 triple6) -> (rule1 % int3)) ((triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple8 triple6) -> (rule1 % int4)) ((triple7) -> (rule3 % int3)) triple6) -> (rule4 % int2)) triple7 triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Alan is very nice to people, but he's also rather big.
Young Bob is wearing green pants.
Dave looks big and is kind with red hair and green shoes.
Because Harry is so young, he is rough and cold when he can be round instead.
A person who's big and kind will also be cold.
People who are nice, round and wearing blue will have red cheeks.
Any green person is a round person.
A kind, cold, round person will be nice in addition.
Nice people who are looking green and seeing red usually feel rather rough.