Charlie is furry. Charlie is rough. Charlie is white. All furry people are nice. If someone is white and rough then they are furry. If Charlie is nice and Charlie is furry then Charlie is white.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and rough then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is nice and Charlie is furry then Charlie is white.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "white" "+"))
Charlie is furry.
True
1
proof
[(triple1 OR ((triple3 triple2) -> rule2))]
("Charlie" "is" "furry" "+")
triple1
((triple3 triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Charlie is nice.
True
2
proof
[(((triple1) -> rule1) OR ((((triple3 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple3 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is furry.[(triple1 OR ((triple3 triple2) -> rule2))] Charlie is rough.[(triple2)] Charlie is white.[(triple3 OR ((((triple1) -> rule1) triple1) -> rule3))] @1: Charlie is nice.[(((triple1) -> rule1) OR ((((triple3 triple2) -> rule2)) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((triple3 triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2