Charlie is furry. Furry people are blue. Furry people are round. Round people are red. If someone is blue and red then they are nice. Nice people are furry. If someone is red and not nice then they are big.
Charlie is furry.
("Charlie" "is" "furry" "+")
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and red then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is red and not nice then they are big.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "+"))
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 round.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Charlie" "is" "nice" "+")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is not nice.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is furry.[(triple1)] @1: Charlie is blue.[(((triple1) -> rule1))] Charlie is round.[(((triple1) -> rule2))] @2: Charlie is red.[(((((triple1) -> rule2)) -> rule3))] @3: Charlie is nice.[(((((triple1) -> rule1) ((((triple1) -> rule2)) -> rule3)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4