Anne is blue. Anne is nice. Anne is young. Harry is cold. Harry is quiet. Harry is smart. Harry is young. Nice people are green. If Anne is green then Anne is cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Anne is green then Anne is cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "+"))
Harry is smart.
True
1
proof
[(triple6)]
("Harry" "is" "smart" "+")
triple6
Harry is not quiet.
False
1
inv-proof
[(triple5)]
("Harry" "is" "quiet" "-")
triple5
Anne is green.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "green" "-")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is young.[(triple3)] Harry is cold.[(triple4)] Harry is quiet.[(triple5)] Harry is smart.[(triple6)] Harry is young.[(triple7)] @1: Anne is green.[(((triple2) -> rule1))] @2: Anne is cold.[(((((triple2) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2