Bob is big. Bob is not kind. Harry is kind. All big, young things are nice. Kind things are not big. If Harry is not big then Harry is cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Harry is kind.
("Harry" "is" "kind" "+")
All big, young things are nice.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Kind things are not big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
If Harry is not big then Harry is cold.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "cold" "+"))
Bob is not kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is not kind.[(triple2)] Harry is kind.[(triple3)] @1: Harry is not big.[(((triple3) -> rule2))] @2: Harry is cold.[(((((triple3) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not kind.
("Bob" "is" "kind" "-")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is not big.
("Harry" "is" "big" "-")
((triple3) -> (rule2 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2