Bob is young. Dave is big. Dave is cold. Dave is young. Harry is big. Harry is kind. Harry is white. Kind, rough people are young. If someone is young then they are cold.
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
Kind, rough people are young.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Harry is kind.
True
1
proof
[(triple6)]
("Harry" "is" "kind" "+")
triple6
Dave is not cold.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule2))]
("Dave" "is" "cold" "-")
triple3
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is young.[(triple1)] Dave is big.[(triple2)] Dave is cold.[(triple3 OR ((triple4) -> rule2))] Dave is young.[(triple4)] Harry is big.[(triple5)] Harry is kind.[(triple6)] Harry is white.[(triple7)] @1: Bob is cold.[(((triple1) -> rule2))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1