Bob is rough. Bob is smart. Bob is white. Dave is green. Erin is cold. Erin is quiet. Erin is white. All smart, cold people are white. Smart people are white. If someone is smart and cold then they are green. All quiet, smart people are white. All white, green people are kind. If someone is quiet and white then they are smart.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
All smart, cold people are white.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and cold then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All quiet, smart people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All white, green people are kind.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and white then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Bob is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2))]
("Bob" "is" "white" "-")
triple3
((triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is smart.
True
3
proof
[(((triple6 triple7) -> rule6))]
("Erin" "is" "smart" "+")
((triple6 triple7) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple6 triple7) -> rule6))]
("Erin" "is" "smart" "-")
((triple6 triple7) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
True
5
proof
[(((((triple6 triple7) -> rule6) triple5) -> rule3))]
("Erin" "is" "green" "+")
((((triple6 triple7) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not green.
False
5
inv-proof
[(((((triple6 triple7) -> rule6) triple5) -> rule3))]
("Erin" "is" "green" "-")
((((triple6 triple7) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
True
7
proof
[(((triple7 ((((triple6 triple7) -> rule6) triple5) -> rule3)) -> rule5))]
("Erin" "is" "kind" "+")
((triple7 ((((triple6 triple7) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not kind.
False
7
inv-proof
[(((triple7 ((((triple6 triple7) -> rule6) triple5) -> rule3)) -> rule5))]
("Erin" "is" "kind" "-")
((triple7 ((((triple6 triple7) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Dave is kind.
Unknown
rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule6 <- FAIL)]]
("Dave" "is" "kind" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is rough.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3 OR ((triple2) -> rule2))] Dave is green.[(triple4)] Erin is cold.[(triple5)] Erin is quiet.[(triple6)] Erin is white.[(triple7)] @1: Erin is smart.[(((triple6 triple7) -> rule6))] @2: Erin is green.[(((((triple6 triple7) -> rule6) triple5) -> rule3))] @3: Erin is kind.[(((triple7 ((((triple6 triple7) -> rule6) triple5) -> rule3)) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple6 triple7) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple6 triple7) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple7 ((((triple6 triple7) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3