Charlie is rough and cold, but he's young and will get over it. Dave was looking rather round and feeling rather cold, but people thought he is kind. They always call him rough Eric. Gary is big and tends to wear red shirts. Big, young people feel cold all the time. People who are green and blue tend to be round in shape. People who are rough are young. All the big and young boys at the park are red. There are so many rough, young people and for some reason they are all big too. Blue, kind, and cold people are habitually rough. Kind people, for example, like the ones at the bank are always blue.
Charlie is young.
("Charlie" "is" "young" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Eric is rough.
("Eric" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
If someone is young and big then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and blue then they are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is big and young then they are red.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is young and rough then they are big.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and kind and cold then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Dave is cold.
True
1
proof
[(triple6)]
("Dave" "is" "cold" "+")
triple6
Dave is not round.
False
1
inv-proof
[(triple4)]
("Dave" "is" "round" "-")
triple4
Dave is blue.
True
2
proof
[(((triple5) -> rule7))]
("Dave" "is" "blue" "+")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple5) -> rule7))]
("Dave" "is" "blue" "-")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Charlie is red.
True
5
proof
[(((((triple1 triple2) -> rule5) triple1) -> rule4) OR ((((triple1 triple2) -> rule5) ((triple2) -> rule3)) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule5) triple1) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule5) ((triple2) -> rule3)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple1 triple2) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple1 triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Dave is not rough.
False
5
inv-proof
[(((((triple5) -> rule7) triple5 triple6) -> rule6))]
("Dave" "is" "rough" "-")
((((triple5) -> (rule7 % int2)) triple5 triple6) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Eric is cold.
True
7
proof
[(((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule5)) -> rule1))]
("Eric" "is" "cold" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3)) triple7) -> (rule5 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Dave is not young.
False
6
inv-proof
[(((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3))]
("Dave" "is" "young" "-")
((((((triple5) -> (rule7 % int3)) triple5 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is big.
True
12
proof
[(((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5))]
("Dave" "is" "big" "+")
((((((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not big.
False
12
inv-proof
[(((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5))]
("Dave" "is" "big" "-")
((((((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is red.
True
19
proof
[(((((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5) ((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3)) -> rule4))]
("Dave" "is" "red" "+")
((((((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule5 % int2)) ((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is not red.
False
19
inv-proof
[(((((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5) ((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3)) -> rule4))]
("Dave" "is" "red" "-")
((((((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule5 % int2)) ((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Eric is blue.
Unknown
rconc
[@1: Eric is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Eric" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "blue" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is cold.[(triple3 OR ((triple1 ((triple1 triple2) -> rule5)) -> rule1) OR ((((triple2) -> rule3) ((triple1 triple2) -> rule5)) -> rule1) OR ((triple1 ((((triple2) -> rule3) triple2) -> rule5)) -> rule1) OR ((((triple2) -> rule3) ((((triple2) -> rule3) triple2) -> rule5)) -> rule1))] Charlie is rough.[(triple2)] Charlie is young.[(triple1 OR ((triple2) -> rule3))] Dave is cold.[(triple6)] Dave is kind.[(triple5)] Dave is round.[(triple4)] Eric is rough.[(triple7)] Gary is big.[(triple9)] Gary is red.[(triple8)] @1: Charlie is big.[(((triple1 triple2) -> rule5) OR ((((triple2) -> rule3) triple2) -> rule5))] Dave is blue.[(((triple5) -> rule7))] Eric is young.[(((triple7) -> rule3))] @2: Charlie is red.[(((((triple1 triple2) -> rule5) triple1) -> rule4) OR ((((triple1 triple2) -> rule5) ((triple2) -> rule3)) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule5) triple1) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule5) ((triple2) -> rule3)) -> rule4))] Dave is rough.[(((((triple5) -> rule7) triple5 triple6) -> rule6))] Eric is big.[(((((triple7) -> rule3) triple7) -> rule5))] @3: Dave is young.[(((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3))] Eric is cold.[(((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule5)) -> rule1))] Eric is red.[(((((((triple7) -> rule3) triple7) -> rule5) ((triple7) -> rule3)) -> rule4))] @4: Dave is big.[(((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5))] @5: Dave is red.[(((((((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3) ((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule5) ((((((triple5) -> rule7) triple5 triple6) -> rule6)) -> rule3)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple1 ((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple4
Eric is rough.
("Eric" "is" "rough" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple8
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
((triple7) -> (rule3 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1 triple2) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple1 triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple5) -> (rule7 % int2)) triple5 triple6) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((((triple5) -> (rule7 % int3)) triple5 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Eric is cold.
("Eric" "is" "cold" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3)) triple7) -> (rule5 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
((((((triple7) -> (rule3 % int3)) triple7) -> (rule5 % int2)) ((triple7) -> (rule3 % int3))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple5) -> (rule7 % int4)) triple5 triple6) -> (rule6 % int3))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule5 % int2)) ((((((triple5) -> (rule7 % int5)) triple5 triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Charlie is rough and cold, but he's young and will get over it.
Dave was looking rather round and feeling rather cold, but people thought he is kind.
They always call him rough Eric.
Gary is big and tends to wear red shirts.
Big, young people feel cold all the time.
People who are green and blue tend to be round in shape.
People who are rough are young.
All the big and young boys at the park are red.
There are so many rough, young people and for some reason they are all big too.
Blue, kind, and cold people are habitually rough.
Kind people, for example, like the ones at the bank are always blue.