Bob is quiet. Bob is smart. Erin is blue. Erin is green. Erin is young. Gary is green. Gary is smart. All green people are blue. If someone is young then they are green.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is young then they are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Erin is not green.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule2))]
("Erin" "is" "green" "-")
triple4
((triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is blue.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "-")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2)] Erin is blue.[(triple3 OR ((triple4) -> rule1) OR ((((triple5) -> rule2)) -> rule1))] Erin is green.[(triple4 OR ((triple5) -> rule2))] Erin is young.[(triple5)] Gary is green.[(triple6)] Gary is smart.[(triple7)] @1: Gary is blue.[(((triple6) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
((triple4) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple4
((triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1