Charlie is nice. Charlie is rough. Dave is big. Rough people are furry. All nice, white people are green. If someone is furry then they are white.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All nice, white people are green.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Charlie is furry.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
True
5
proof
[(((triple1 ((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "green" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not green.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "green" "-")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is nice.[(triple1)] Charlie is rough.[(triple2)] Dave is big.[(triple3)] @1: Charlie is furry.[(((triple2) -> rule1))] @2: Charlie is white.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is green.[(((triple1 ((((triple2) -> rule1)) -> rule3)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3