Anne is nice. Bob is not rough. Dave is not young. Harry is cold. All nice, big things are rough. If Anne is nice then Anne is big. If something is green then it is not nice.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Dave is not young.
("Dave" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
All nice, big things are rough.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Anne is nice then Anne is big.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If something is green then it is not nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "-"))
Harry is cold.
True
1
proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Dave is young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Anne is big.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is nice.[(triple1)] Bob is not rough.[(triple2)] Dave is not young.[(triple3)] Harry is cold.[(triple4)] @1: Anne is big.[(((triple1) -> rule2))] @2: Anne is rough.[(((triple1 ((triple1) -> rule2)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is not rough.
("Bob" "is" "rough" "-")
triple2
Dave is not young.
("Dave" "is" "young" "-")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2