Bob is round. Charlie is smart. Dave is not white. Erin is white. All round people are white. All white people are kind. If Charlie is not white then Charlie is green.
Bob is round.
("Bob" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is white.
("Erin" "is" "white" "+")
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is not white then Charlie is green.
((("Charlie" "is" "white" "~")) -> ("Charlie" "is" "green" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple4)]
("Erin" "is" "white" "-")
triple4
Erin is kind.
True
2
proof
[(((triple4) -> rule2))]
("Erin" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple4) -> rule2))]
("Erin" "is" "kind" "-")
((triple4) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is round.[(triple1)] Charlie is smart.[(triple2)] Dave is not white.[(triple3)] Erin is white.[(triple4)] @1: Bob is white.[(((triple1) -> rule1))] Erin is kind.[(((triple4) -> rule2))] @2: Bob is kind.[(((((triple1) -> rule1)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2