Bob is big. Bob is furry. Charlie is furry. Charlie is green. Erin is big. Erin is green. Erin is rough. If someone is green then they are kind. If someone is green and kind then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and kind then they are white.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Erin is green.
True
1
proof
[(triple6)]
("Erin" "is" "green" "+")
triple6
Erin is not green.
False
1
inv-proof
[(triple6)]
("Erin" "is" "green" "-")
triple6
Charlie is kind.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is white.
True
4
proof
[(((triple6 ((triple6) -> rule1)) -> rule2))]
("Erin" "is" "white" "+")
((triple6 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "white" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Charlie is furry.[(triple3)] Charlie is green.[(triple4)] Erin is big.[(triple5)] Erin is green.[(triple6)] Erin is rough.[(triple7)] @1: Charlie is kind.[(((triple4) -> rule1))] Erin is kind.[(((triple6) -> rule1))] @2: Charlie is white.[(((triple4 ((triple4) -> rule1)) -> rule2))] Erin is white.[(((triple6 ((triple6) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple6 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2