Bob is green. Erin is smart. Gary is not blue. All kind, white people are red. Smart, kind people are red. All smart, green people are rough. If someone is blue and white then they are kind. If someone is green and not white then they are kind. If someone is smart then they are green. Rough people are green. Red, rough people are not smart.
Bob is green.
("Bob" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
All kind, white people are red.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Smart, kind people are red.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All smart, green people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and white then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and not white then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Red, rough people are not smart.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
Gary is not blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Erin is green.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "-")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule3))]
("Erin" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule3))]
("Erin" "is" "rough" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Erin" "is" "red" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is green.[(triple1)] Erin is smart.[(triple2)] Gary is not blue.[(triple3)] @1: Erin is green.[(((triple2) -> rule6))] @2: Erin is rough.[(((triple2 ((triple2) -> rule6)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2