Bob is big. Dave is smart. Erin is kind. Gary is green. Green things are white. If something is white then it is kind. If something is kind then it is white. Blue things are smart. If something is big then it is white. If Erin is kind and Erin is smart then Erin is white.
Bob is big.
("Bob" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Erin is kind and Erin is smart then Erin is white.
((("Erin" "is" "kind" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Erin is white.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "white" "+")
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "white" "-")
((triple4) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is big.[(triple1)] Dave is smart.[(triple2)] Erin is kind.[(triple3)] Gary is green.[(triple4)] @1: Bob is white.[(((triple1) -> rule5))] Erin is white.[(((triple3) -> rule3))] Gary is white.[(((triple4) -> rule1))] @2: Bob is kind.[(((((triple1) -> rule5)) -> rule2))] Gary is kind.[(((((triple4) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2