Anne is kind. Dave is smart. Harry is quiet. If something is white and quiet then it is rough. If something is quiet then it is white.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is white and quiet then it is rough.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Harry is white.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "-")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "rough" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "rough" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Dave is smart.[(triple2)] Harry is quiet.[(triple3)] @1: Harry is white.[(((triple3) -> rule2))] @2: Harry is rough.[(((((triple3) -> rule2) triple3) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2