Anne is nice. Bob is quiet. Dave is white. Harry is smart. All white things are green. If Dave is white then Dave is green. All smart things are quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Dave is white then Dave is green.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Harry is quiet.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Bob is quiet.[(triple2)] Dave is white.[(triple3)] Harry is smart.[(triple4)] @1: Dave is green.[(((triple3) -> rule1) OR ((triple3) -> rule2))] Harry is quiet.[(((triple4) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1