Bob is green. Bob is rough. Dave is not kind. Dave is smart. Erin is kind. Erin is nice. Erin is not rough. All smart, green things are nice. If Bob is green then Bob is smart. If something is furry and not big then it is green.
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
All smart, green things are nice.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Bob is green then Bob is smart.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
If something is furry and not big then it is green.
((("something" "is" "furry" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple6)]
("Erin" "is" "nice" "-")
triple6
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is green.[(triple1)] Bob is rough.[(triple2)] Dave is not kind.[(triple3)] Dave is smart.[(triple4)] Erin is kind.[(triple5)] Erin is nice.[(triple6)] Erin is not rough.[(triple7)] @1: Bob is smart.[(((triple1) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule2) triple1) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is not rough.
("Erin" "is" "rough" "-")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2