Charlie wears all blue. Dave wears all blue. Eric is both young and fairly round in size. Fred is so big, he is often blue, but always kind. A big round person is nice. A green, round, blue male or female will be a big male or female, too. Like a blueberry, a big blue person is round as anything. Round and big people are sure to be rough. All nice people are young.
If someone is round and big then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is green and round and blue then they are big.
((("someone" "is" "green" "+") ("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and big then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is round and big then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Eric is not young.
False
1
inv-proof
[(triple3)]
("Eric" "is" "young" "-")
triple3
Fred is round.
True
3
proof
[(((triple6 triple7) -> rule3))]
("Fred" "is" "round" "+")
((triple6 triple7) -> (rule3 % int1))
Fred is round.
("Fred" "is" "round" "+")
int1
Fred is not round.
False
3
inv-proof
[(((triple6 triple7) -> rule3))]
("Fred" "is" "round" "-")
((triple6 triple7) -> (rule3 % int1))
Fred is round.
("Fred" "is" "round" "+")
int1
Fred is rough.
True
5
proof
[(((((triple6 triple7) -> rule3) triple7) -> rule4))]
("Fred" "is" "rough" "+")
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is not rough.
False
5
inv-proof
[(((((triple6 triple7) -> rule3) triple7) -> rule4))]
("Fred" "is" "rough" "-")
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
True
6
proof
[(((((((triple6 triple7) -> rule3) triple7) -> rule1)) -> rule5))]
("Fred" "is" "young" "+")
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is nice.
("Fred" "is" "nice" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Fred is not young.
False
6
inv-proof
[(((((((triple6 triple7) -> rule3) triple7) -> rule1)) -> rule5))]
("Fred" "is" "young" "-")
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is nice.
("Fred" "is" "nice" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Eric is not rough.
Unknown
inv-rconc
[@2: Eric is rough.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Eric" "is" "rough" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is nice.
Unknown
rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Eric is not blue.
Unknown
inv-random
[@0: Eric is blue.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "blue" "-")
Fred is green.
Unknown
random
[@0: Fred is green.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Dave is blue.[(triple2)] Eric is round.[(triple4)] Eric is young.[(triple3)] Fred is big.[(triple7)] Fred is blue.[(triple6)] Fred is kind.[(triple5)] @1: Fred is round.[(((triple6 triple7) -> rule3))] @2: Fred is nice.[(((((triple6 triple7) -> rule3) triple7) -> rule1))] Fred is rough.[(((((triple6 triple7) -> rule3) triple7) -> rule4))] @3: Fred is young.[(((((((triple6 triple7) -> rule3) triple7) -> rule1)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Eric is round.
("Eric" "is" "round" "+")
triple4
Eric is young.
("Eric" "is" "young" "+")
triple3
Fred is big.
("Fred" "is" "big" "+")
triple7
Fred is blue.
("Fred" "is" "blue" "+")
triple6
Fred is kind.
("Fred" "is" "kind" "+")
triple5
Fred is round.
("Fred" "is" "round" "+")
((triple6 triple7) -> (rule3 % int1))
Fred is round.
("Fred" "is" "round" "+")
int1
Fred is nice.
("Fred" "is" "nice" "+")
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Fred is nice.
("Fred" "is" "nice" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is rough.
("Fred" "is" "rough" "+")
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Fred is nice.
("Fred" "is" "nice" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Charlie wears all blue.
Dave wears all blue.
Eric is both young and fairly round in size.
Fred is so big, he is often blue, but always kind.
A big round person is nice.
A green, round, blue male or female will be a big male or female, too.
Like a blueberry, a big blue person is round as anything.
Round and big people are sure to be rough.
All nice people are young.