Charlie is furry. Furry people are big. Quiet people are cold. If Charlie is cold and Charlie is big then Charlie is kind. If Charlie is big and Charlie is nice then Charlie is blue. All kind, nice people are big. All big people are quiet.
Charlie is furry.
("Charlie" "is" "furry" "+")
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is big then Charlie is kind.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "kind" "+"))
If Charlie is big and Charlie is nice then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "blue" "+"))
All kind, nice people are big.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "-")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is furry.[(triple1)] @1: Charlie is big.[(((triple1) -> rule1))] @2: Charlie is quiet.[(((((triple1) -> rule1)) -> rule6))] @3: Charlie is cold.[(((((((triple1) -> rule1)) -> rule6)) -> rule2))] @4: Charlie is kind.[(((((((((triple1) -> rule1)) -> rule6)) -> rule2) ((triple1) -> rule1)) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int4))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4