Charlie is big. Harry is big. Harry is red. Kind, young people are smart. All furry, big people are kind. If someone is red then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Kind, young people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All furry, big people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple2 OR ((triple3) -> rule3))]
("Harry" "is" "big" "+")
triple2
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule3))]
("Harry" "is" "big" "-")
triple2
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Harry is big.[(triple2 OR ((triple3) -> rule3))] Harry is red.[(triple3)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple3