Anne is cold. Bob is blue. Bob is kind. Bob is not smart. Dave is cold. Dave is kind. Harry is big. If something is green then it is smart. Cold things are green.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple5)]
("Dave" "is" "cold" "-")
triple5
Dave is green.
True
2
proof
[(((triple5) -> rule2))]
("Dave" "is" "green" "+")
((triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "-")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is smart.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Bob is not smart.[(triple4)] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Harry is big.[(triple7)] @1: Anne is green.[(((triple1) -> rule2))] Dave is green.[(((triple5) -> rule2))] @2: Anne is smart.[(((((triple1) -> rule2)) -> rule1))] Dave is smart.[(((((triple5) -> rule2)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2