Bob is red. Erin is smart. Fiona is smart. Gary is young. Red people are white. If Bob is red and Bob is smart then Bob is rough. White, green people are red. All white people are red. If someone is white and smart then they are nice. If Gary is smart and Gary is green then Gary is white.
Bob is red.
("Bob" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If Bob is red and Bob is smart then Bob is rough.
((("Bob" "is" "red" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
White, green people are red.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is white and smart then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Gary is smart and Gary is green then Gary is white.
((("Gary" "is" "smart" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "white" "+"))
Gary is young.
True
1
proof
[(triple4)]
("Gary" "is" "young" "+")
triple4
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Bob is white.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Fiona is red.
Unknown
rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is red.[(triple1)] Erin is smart.[(triple2)] Fiona is smart.[(triple3)] Gary is young.[(triple4)] @1: Bob is white.[(((triple1) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1