Charlie is big. Charlie is green. Harry is white. White things are furry. All green, smart things are white. If something is green then it is white. All kind things are white. Furry things are smart. If something is kind and smart then it is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All green, smart things are white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is kind and smart then it is nice.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Harry is furry.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "white" "-")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Harry is white.[(triple3)] @1: Charlie is white.[(((triple2) -> rule3))] Harry is furry.[(((triple3) -> rule1))] @2: Charlie is furry.[(((((triple2) -> rule3)) -> rule1))] Harry is smart.[(((((triple3) -> rule1)) -> rule5))] @3: Charlie is smart.[(((((((triple2) -> rule3)) -> rule1)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3