Big Charlie is a kind man and often wears blue and green shirts. Dave ate some rotten meat and now feels green. Fred, a kind and nice man, is wearing a green sweatshirt. He is also a fairly round sized man in shape. They always call him rough Gary. Red and green people that are nice are cold to strangers. A green person who is cold and round is also big. If you have a big and round shape then you are going to be young, too. A person who is round and nice is cold. Round, nice people are normally cold and nasty.
If someone is red and nice and green then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and round and green then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is round and big then they are young.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is nice and round then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and nice then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Charlie is big.
True
1
proof
[(triple4)]
("Charlie" "is" "big" "+")
triple4
Dave is not green.
False
1
inv-proof
[(triple5)]
("Dave" "is" "green" "-")
triple5
Fred is cold.
True
3
proof
[(((triple6 triple7) -> rule5) OR ((triple7 triple6) -> rule4))]
("Fred" "is" "cold" "+")
((triple6 triple7) -> (rule5 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
((triple7 triple6) -> (rule4 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
Fred is not cold.
False
3
inv-proof
[(((triple6 triple7) -> rule5) OR ((triple7 triple6) -> rule4))]
("Fred" "is" "cold" "-")
((triple6 triple7) -> (rule5 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
((triple7 triple6) -> (rule4 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
Fred is big.
True
6
proof
[(((((triple6 triple7) -> rule5) triple6 triple9) -> rule2) OR ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2))]
("Fred" "is" "big" "+")
((((triple6 triple7) -> (rule5 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
((((triple7 triple6) -> (rule4 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
Fred is not big.
False
6
inv-proof
[(((((triple6 triple7) -> rule5) triple6 triple9) -> rule2) OR ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2))]
("Fred" "is" "big" "-")
((((triple6 triple7) -> (rule5 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
((((triple7 triple6) -> (rule4 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
Fred is young.
True
8
proof
[(((triple6 ((((triple6 triple7) -> rule5) triple6 triple9) -> rule2)) -> rule3) OR ((triple6 ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2)) -> rule3))]
("Fred" "is" "young" "+")
((triple6 ((((triple6 triple7) -> (rule5 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
((triple6 ((((triple7 triple6) -> (rule4 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
Fred is not young.
False
8
inv-proof
[(((triple6 ((((triple6 triple7) -> rule5) triple6 triple9) -> rule2)) -> rule3) OR ((triple6 ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2)) -> rule3))]
("Fred" "is" "young" "-")
((triple6 ((((triple6 triple7) -> (rule5 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
((triple6 ((((triple7 triple6) -> (rule4 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is big.[(triple4)] Charlie is blue.[(triple3)] Charlie is green.[(triple2)] Charlie is kind.[(triple1)] Dave is green.[(triple5)] Fred is green.[(triple9)] Fred is kind.[(triple8)] Fred is nice.[(triple7)] Fred is round.[(triple6)] Gary is rough.[(triple10)] @1: Fred is cold.[(((triple6 triple7) -> rule5) OR ((triple7 triple6) -> rule4))] @2: Fred is big.[(((((triple6 triple7) -> rule5) triple6 triple9) -> rule2) OR ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2))] @3: Fred is young.[(((triple6 ((((triple6 triple7) -> rule5) triple6 triple9) -> rule2)) -> rule3) OR ((triple6 ((((triple7 triple6) -> rule4) triple6 triple9) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple5
Fred is green.
("Fred" "is" "green" "+")
triple9
Fred is kind.
("Fred" "is" "kind" "+")
triple8
Fred is nice.
("Fred" "is" "nice" "+")
triple7
Fred is round.
("Fred" "is" "round" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Fred is cold.
("Fred" "is" "cold" "+")
((triple6 triple7) -> (rule5 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
((triple7 triple6) -> (rule4 % int1))
Fred is cold.
("Fred" "is" "cold" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
((((triple6 triple7) -> (rule5 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
((((triple7 triple6) -> (rule4 % int2)) triple6 triple9) -> (rule2 % int1))
Fred is big.
("Fred" "is" "big" "+")
int1
Fred is cold.
("Fred" "is" "cold" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
((triple6 ((((triple6 triple7) -> (rule5 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
((triple6 ((((triple7 triple6) -> (rule4 % int3)) triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is big.
("Fred" "is" "big" "+")
int2
Fred is cold.
("Fred" "is" "cold" "+")
int3
Big Charlie is a kind man and often wears blue and green shirts.
Dave ate some rotten meat and now feels green.
Fred, a kind and nice man, is wearing a green sweatshirt; He is also a fairly round sized man in shape.
They always call him rough Gary.
Red and green people that are nice are cold to strangers.
A green person who is cold and round is also big.
If you have a big and round shape then you are going to be young, too.
A person who is round and nice is cold.
Round, nice people are normally cold and nasty.