Dave is white. Harry is nice. If something is green and nice then it is kind. White things are green. If something is nice then it is big. All nice things are kind. If something is white then it is nice. If something is round then it is kind.
Dave is white.
("Dave" "is" "white" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is green and nice then it is kind.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Harry is big.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "big" "+")
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Dave is white.[(triple1)] Harry is nice.[(triple2)] @1: Dave is green.[(((triple1) -> rule2))] Dave is nice.[(((triple1) -> rule5))] Harry is big.[(((triple2) -> rule3))] Harry is kind.[(((triple2) -> rule4))] @2: Dave is big.[(((((triple1) -> rule5)) -> rule3))] Dave is kind.[(((((triple1) -> rule5)) -> rule4) OR ((((triple1) -> rule2) ((triple1) -> rule5)) -> rule1))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3