Charlie is cold. Charlie is furry. Charlie is quiet. Charlie is young. Harry is cold. Harry is quiet. Harry is rough. If someone is rough and round then they are red. If Harry is rough and Harry is young then Harry is round. All round people are red. All rough, quiet people are young. If someone is red and young then they are round. All red, round people are quiet.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough and round then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Harry is rough and Harry is young then Harry is round.
((("Harry" "is" "rough" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "round" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All rough, quiet people are young.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is red and young then they are round.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All red, round people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Harry is young.
True
3
proof
[(((triple7 triple6) -> rule4))]
("Harry" "is" "young" "+")
((triple7 triple6) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
3
inv-proof
[(((triple7 triple6) -> rule4))]
("Harry" "is" "young" "-")
((triple7 triple6) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
True
5
proof
[(((triple7 ((triple7 triple6) -> rule4)) -> rule2))]
("Harry" "is" "round" "+")
((triple7 ((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not round.
False
5
inv-proof
[(((triple7 ((triple7 triple6) -> rule4)) -> rule2))]
("Harry" "is" "round" "-")
((triple7 ((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
True
6
proof
[(((((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule3) OR ((triple7 ((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "red" "+")
((((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple7 ((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not red.
False
6
inv-proof
[(((((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule3) OR ((triple7 ((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "red" "-")
((((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple7 ((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is quiet.[(triple3)] Charlie is young.[(triple4)] Harry is cold.[(triple5)] Harry is quiet.[(triple6)] Harry is rough.[(triple7)] @1: Harry is young.[(((triple7 triple6) -> rule4))] @2: Harry is round.[(((triple7 ((triple7 triple6) -> rule4)) -> rule2))] @3: Harry is red.[(((((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule3) OR ((triple7 ((triple7 ((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Harry is young.
("Harry" "is" "young" "+")
((triple7 triple6) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple7 ((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple7 ((triple7 ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3