Bob is smart. Dave is nice. Kind people are not green. Blue people are green. Nice people are blue. All kind people are not white. If Dave is not smart then Dave is green. Kind people are furry. All nice people are furry. If someone is smart and not blue then they are furry.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Kind people are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All kind people are not white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "-"))
If Dave is not smart then Dave is green.
((("Dave" "is" "smart" "~")) -> ("Dave" "is" "green" "+"))
Kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and not blue then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Dave is furry.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule7))]
("Dave" "is" "furry" "-")
((triple2) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Dave" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is smart.[(triple1)] Dave is nice.[(triple2)] @1: Dave is blue.[(((triple2) -> rule3))] Dave is furry.[(((triple2) -> rule7))] @2: Dave is green.[(((((triple2) -> rule3)) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2