Bob was born only a few years ago so he is young. Fred ate some rotten meat and now feels green. Gary is a nice person who is red because he has a rash. Big, rough Harry is also kind with red hair and green shoes. A quite nice person who is red and green is also big. Kind big people are green and young. A nice person with rough skin will be round, you can count on it. Everyone knows that if you are cold, kind, and big, it goes without saying that you are round. If you meet a young and kind person who is also rough, they are cold, too.
Bob is young.
("Bob" "is" "young" "+")
Fred is green.
("Fred" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is red and green and nice then they are big.
((("someone" "is" "red" "+") ("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and green and big then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and nice then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and kind and big then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and young and kind then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Harry is red.
True
1
proof
[(triple6)]
("Harry" "is" "red" "+")
triple6
Harry is not green.
False
1
inv-proof
[(triple8)]
("Harry" "is" "green" "-")
triple8
Harry is young.
True
4
proof
[(((triple7 triple8 triple9) -> rule2))]
("Harry" "is" "young" "+")
((triple7 triple8 triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
4
inv-proof
[(((triple7 triple8 triple9) -> rule2))]
("Harry" "is" "young" "-")
((triple7 triple8 triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
True
7
proof
[(((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5))]
("Harry" "is" "cold" "+")
((triple5 ((triple7 triple8 triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not cold.
False
7
inv-proof
[(((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5))]
("Harry" "is" "cold" "-")
((triple5 ((triple7 triple8 triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
True
10
proof
[(((((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5) triple7 triple9) -> rule4))]
("Harry" "is" "round" "+")
((((triple5 ((triple7 triple8 triple9) -> (rule2 % int3)) triple7) -> (rule5 % int2)) triple7 triple9) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not round.
False
10
inv-proof
[(((((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5) triple7 triple9) -> rule4))]
("Harry" "is" "round" "-")
((((triple5 ((triple7 triple8 triple9) -> (rule2 % int3)) triple7) -> (rule5 % int2)) triple7 triple9) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Fred is big.
Unknown
rconc
[@1: Fred is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fred" "is" "big" "+")
Fred is not cold.
Unknown
inv-rconc
[@1: Fred is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fred" "is" "cold" "-")
Fred is round.
Unknown
rconc
[@1: Fred is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fred" "is" "round" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Fred is red.
Unknown
random
[@0: Fred is red.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "red" "+")
@0: Bob is young.[(triple1)] Fred is green.[(triple2)] Gary is nice.[(triple4)] Gary is red.[(triple3)] Harry is big.[(triple9)] Harry is green.[(triple8)] Harry is kind.[(triple7)] Harry is red.[(triple6)] Harry is rough.[(triple5)] @1: Harry is young.[(((triple7 triple8 triple9) -> rule2))] @2: Harry is cold.[(((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5))] @3: Harry is round.[(((((triple5 ((triple7 triple8 triple9) -> rule2) triple7) -> rule5) triple7 triple9) -> rule4))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Fred is green.
("Fred" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is young.
("Harry" "is" "young" "+")
((triple7 triple8 triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple5 ((triple7 triple8 triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple5 ((triple7 triple8 triple9) -> (rule2 % int3)) triple7) -> (rule5 % int2)) triple7 triple9) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Bob was born only a few years ago so he is young.
Fred ate some rotten meat and now feels green.
Gary is a nice person who is red because he has a rash.
Big, rough Harry is also kind with red hair and green shoes.
A quite nice person who is red and green is also big.
Kind big people are green and young.
A nice person with rough skin will be round, you can count on it.
Everyone knows that if you are cold, kind, and big, it goes without saying that you are round.
If you meet a young and kind person who is also rough, they are cold, too.