Bob is green. Bob is not white. Erin is cold. Erin is furry. Erin is kind. Erin is not round. Erin is white. If someone is furry and green then they are blue. If Bob is white then Bob is not blue. If someone is white and not cold then they are kind. All green, round people are kind. Furry people are green. If Erin is white and Erin is blue then Erin is kind.
Bob is green.
("Bob" "is" "green" "+")
Bob is not white.
("Bob" "is" "white" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is white.
("Erin" "is" "white" "+")
If someone is furry and green then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Bob is white then Bob is not blue.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "-"))
If someone is white and not cold then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "kind" "+"))
All green, round people are kind.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If Erin is white and Erin is blue then Erin is kind.
((("Erin" "is" "white" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
Erin is furry.
True
1
proof
[(triple4)]
("Erin" "is" "furry" "+")
triple4
Erin is round.
False
1
inv-proof
[(triple6)]
("Erin" "is" "round" "+")
triple6
Erin is green.
True
2
proof
[(((triple4) -> rule5))]
("Erin" "is" "green" "+")
((triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple4) -> rule5))]
("Erin" "is" "green" "-")
((triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
True
4
proof
[(((triple4 ((triple4) -> rule5)) -> rule1))]
("Erin" "is" "blue" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((triple4 ((triple4) -> rule5)) -> rule1))]
("Erin" "is" "blue" "-")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is not white.[(triple2)] Erin is cold.[(triple3)] Erin is furry.[(triple4)] Erin is kind.[(triple5 OR ((triple7 ((triple4 ((triple4) -> rule5)) -> rule1)) -> rule6))] Erin is not round.[(triple6)] Erin is white.[(triple7)] @1: Erin is green.[(((triple4) -> rule5))] @2: Erin is blue.[(((triple4 ((triple4) -> rule5)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
((triple7 ((triple4 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not round.
("Erin" "is" "round" "-")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2