Alan has a round face and is very nice. Young Charlie got into a fight that left him with red sores on his face. Dave is a nice person who is red because he has a rash. Harry is a person both green and big. Someone who has rough nails and blue teeth as well as being kind to adults are often noted to having big fingers. Green people will be nice even when they have been rough. If someone is a bit rough, but also nice, then they qualify as round. A nice and cold person can be counted on to be a young person at the same time. People that are big but also green, may ultimately be very nice. A person that is green also someone who is big.
Alan is round.
("Alan" "is" "round" "+")
Alan is nice.
("Alan" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is rough and blue and kind then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is green and nice then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and rough then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and cold then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is big and green then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Harry is nice.
True
3
proof
[(((triple8 triple7) -> rule5) OR ((((triple7) -> rule6) triple7) -> rule5))]
("Harry" "is" "nice" "+")
((triple8 triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((triple8 triple7) -> rule5) OR ((((triple7) -> rule6) triple7) -> rule5))]
("Harry" "is" "nice" "-")
((triple8 triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
True
5
proof
[(((triple7 ((triple8 triple7) -> rule5)) -> rule2) OR ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2))]
("Harry" "is" "rough" "+")
((triple7 ((triple8 triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not rough.
False
5
inv-proof
[(((triple7 ((triple8 triple7) -> rule5)) -> rule2) OR ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2))]
("Harry" "is" "rough" "-")
((triple7 ((triple8 triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
True
9
proof
[(((((triple8 triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((triple8 triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3))]
("Harry" "is" "round" "+")
((((triple8 triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple8 triple7) -> (rule5 % int4)) ((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not round.
False
9
inv-proof
[(((((triple8 triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((triple8 triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3))]
("Harry" "is" "round" "-")
((((triple8 triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple8 triple7) -> (rule5 % int4)) ((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "young" "-")
Alan is rough.
Unknown
rconc
[@1: Alan is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Alan" "is" "rough" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Alan is kind.
Unknown
random
[@0: Alan is kind.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "kind" "+")
Alan is not cold.
Unknown
inv-random
[@0: Alan is cold.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "cold" "-")
Alan is blue.
Unknown
random
[@0: Alan is blue.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "blue" "+")
@0: Alan is nice.[(triple2)] Alan is round.[(triple1)] Charlie is red.[(triple4)] Charlie is young.[(triple3)] Dave is nice.[(triple6)] Dave is red.[(triple5)] Harry is big.[(triple8 OR ((triple7) -> rule6))] Harry is green.[(triple7)] @1: Harry is nice.[(((triple8 triple7) -> rule5) OR ((((triple7) -> rule6) triple7) -> rule5))] @2: Harry is rough.[(((triple7 ((triple8 triple7) -> rule5)) -> rule2) OR ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2))] @3: Harry is round.[(((((triple8 triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((triple8 triple7) -> rule5)) -> rule2)) -> rule3) OR ((((triple8 triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3) OR ((((((triple7) -> rule6) triple7) -> rule5) ((triple7 ((((triple7) -> rule6) triple7) -> rule5)) -> rule2)) -> rule3))]
Alan is nice.
("Alan" "is" "nice" "+")
triple2
Alan is round.
("Alan" "is" "round" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple7) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
((triple8 triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple7 ((triple8 triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((triple8 triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((triple8 triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple8 triple7) -> (rule5 % int4)) ((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3)) ((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Alan has a round face and is very nice.
Young Charlie got into a fight that left him with red sores on his face.
Dave is a nice person who is red because he has a rash.
Harry is a person both green and big.
Someone who has rough nails and blue teeth as well as being kind to adults are often noted to having big fingers.
Green people will be nice even when they have been rough.
If someone is a bit rough, but also nice, then they qualify as round.
A nice and cold person can be counted on to be a young person at the same time.
People that are big but also green, may ultimately be very nice.
A person that is green also someone who is big.