Charlie is green. Harry is kind. Harry is smart. Rough things are smart. If something is smart then it is big. Big, smart things are green. If Harry is white then Harry is green. If Charlie is big then Charlie is green. If something is kind and white then it is big.
Charlie is green.
("Charlie" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Big, smart things are green.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Harry is white then Harry is green.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "green" "+"))
If Charlie is big then Charlie is green.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
If something is kind and white then it is big.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple2)]
("Harry" "is" "kind" "-")
triple2
Harry is big.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "big" "+")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "big" "-")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule3))]
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule3))]
("Harry" "is" "green" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is green.[(triple1)] Harry is kind.[(triple2)] Harry is smart.[(triple3)] @1: Harry is big.[(((triple3) -> rule2))] @2: Harry is green.[(((((triple3) -> rule2) triple3) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2