Bob is white. Erin is white. Erin is young. If something is kind then it is white. If something is young then it is big. Big, white things are blue.
Bob is white.
("Bob" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Big, white things are blue.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Erin is big.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "big" "+")
((triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "big" "-")
((triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
True
4
proof
[(((((triple3) -> rule2) triple2) -> rule3))]
("Erin" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((((triple3) -> rule2) triple2) -> rule3))]
("Erin" "is" "blue" "-")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is white.[(triple1)] Erin is white.[(triple2)] Erin is young.[(triple3)] @1: Erin is big.[(((triple3) -> rule2))] @2: Erin is blue.[(((((triple3) -> rule2) triple2) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2