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