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