Bob is green. Charlie is furry. Erin is round. If Bob is green then Bob is furry. Big, blue things are round. All round, big things are furry. If Charlie is green and Charlie is round then Charlie is blue. Furry, big things are white. If Charlie is furry then Charlie is kind. If something is blue then it is green. All kind things are big.
Bob is green.
("Bob" "is" "green" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
If Bob is green then Bob is furry.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "furry" "+"))
Big, blue things are round.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All round, big things are furry.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Charlie is green and Charlie is round then Charlie is blue.
((("Charlie" "is" "green" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "blue" "+"))
Furry, big things are white.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Charlie is furry then Charlie is kind.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "kind" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
True
5
proof
[(((triple2 ((((triple2) -> rule6)) -> rule8)) -> rule5))]
("Charlie" "is" "white" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not white.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule6)) -> rule8)) -> rule5))]
("Charlie" "is" "white" "-")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Bob" "is" "white" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is green.[(triple1)] Charlie is furry.[(triple2)] Erin is round.[(triple3)] @1: Bob is furry.[(((triple1) -> rule1))] Charlie is kind.[(((triple2) -> rule6))] @2: Charlie is big.[(((((triple2) -> rule6)) -> rule8))] @3: Charlie is white.[(((triple2 ((((triple2) -> rule6)) -> rule8)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3