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