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