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