Bob is quiet. Dave is smart. If Dave is red and Dave is smart then Dave is round. If Dave is red and Dave is smart then Dave is nice. If something is quiet then it is green. Smart things are green. Nice, quiet things are green. Smart, green things are nice.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is red and Dave is smart then Dave is round.
((("Dave" "is" "red" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
If Dave is red and Dave is smart then Dave is nice.
((("Dave" "is" "red" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "nice" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Nice, quiet things are green.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Smart, green things are nice.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "-")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule6))]
("Dave" "is" "nice" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule6))]
("Dave" "is" "nice" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is quiet.[(triple1)] Dave is smart.[(triple2)] @1: Bob is green.[(((triple1) -> rule3))] Dave is green.[(((triple2) -> rule4))] @2: Dave is nice.[(((triple2 ((triple2) -> rule4)) -> rule6))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2