Dave is kind. Dave is round. Harry is blue. Harry is kind. Harry is quiet. Harry is round. Harry is white. White, nice things are round. All green things are nice. Quiet things are green.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
White, nice things are round.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple5)]
("Harry" "is" "quiet" "-")
triple5
Harry is green.
True
2
proof
[(((triple5) -> rule3))]
("Harry" "is" "green" "+")
((triple5) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple5) -> rule3))]
("Harry" "is" "green" "-")
((triple5) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
True
3
proof
[(((((triple5) -> rule3)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is kind.[(triple1)] Dave is round.[(triple2)] Harry is blue.[(triple3)] Harry is kind.[(triple4)] Harry is quiet.[(triple5)] Harry is round.[(triple6 OR ((triple7 ((((triple5) -> rule3)) -> rule2)) -> rule1))] Harry is white.[(triple7)] @1: Harry is green.[(((triple5) -> rule3))] @2: Harry is nice.[(((((triple5) -> rule3)) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((triple7 ((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
((triple5) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2