Anne is smart. Anne is white. Charlie is not white. Dave is furry. Dave is red. Harry is furry. Harry is smart. All smart things are nice. If something is smart and nice then it is big.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is smart and nice then it is big.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Harry is nice.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "nice" "-")
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
True
4
proof
[(((triple7 ((triple7) -> rule1)) -> rule2))]
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is smart.[(triple1)] Anne is white.[(triple2)] Charlie is not white.[(triple3)] Dave is furry.[(triple4)] Dave is red.[(triple5)] Harry is furry.[(triple6)] Harry is smart.[(triple7)] @1: Anne is nice.[(((triple1) -> rule1))] Harry is nice.[(((triple7) -> rule1))] @2: Anne is big.[(((triple1 ((triple1) -> rule1)) -> rule2))] Harry is big.[(((triple7 ((triple7) -> rule1)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2