Dave is blue. Dave is cold. Erin is big. Erin is cold. Erin is young. Gary is big. Gary is white. Big things are white. White things are cold.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is white.
("Gary" "is" "white" "+")
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Erin is young.
True
1
proof
[(triple5)]
("Erin" "is" "young" "+")
triple5
Gary is not white.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule1))]
("Gary" "is" "white" "-")
triple7
((triple6) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Erin is big.[(triple3)] Erin is cold.[(triple4 OR ((((triple3) -> rule1)) -> rule2))] Erin is young.[(triple5)] Gary is big.[(triple6)] Gary is white.[(triple7 OR ((triple6) -> rule1))] @1: Erin is white.[(((triple3) -> rule1))] Gary is cold.[(((triple7) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple6) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2