Anne is kind. Anne is young. Bob is not nice. Gary is smart. Harry is cold. Harry is kind. Harry is smart. If someone is smart and kind then they are cold. All young people are smart.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart and kind then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Harry is kind.
True
1
proof
[(triple6)]
("Harry" "is" "kind" "+")
triple6
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
Anne is smart.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
True
4
proof
[(((((triple2) -> rule2) triple1) -> rule1))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not cold.
False
4
inv-proof
[(((((triple2) -> rule2) triple1) -> rule1))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is young.[(triple2)] Bob is not nice.[(triple3)] Gary is smart.[(triple4)] Harry is cold.[(triple5 OR ((triple7 triple6) -> rule1))] Harry is kind.[(triple6)] Harry is smart.[(triple7)] @1: Anne is smart.[(((triple2) -> rule2))] @2: Anne is cold.[(((((triple2) -> rule2) triple1) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
((triple7 triple6) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2