Dave is quiet. Erin is white. Gary is red. Quiet people are white. All white people are cold. If Erin is green and Erin is kind then Erin is white. If someone is white then they are red. Red people are cold. If someone is red and green then they are kind.
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Erin is green and Erin is kind then Erin is white.
((("Erin" "is" "green" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "white" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is red and green then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Erin is white.
True
1
proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Dave is quiet.[(triple1)] Erin is white.[(triple2)] Gary is red.[(triple3)] @1: Dave is white.[(((triple1) -> rule1))] Erin is cold.[(((triple2) -> rule2) OR ((((triple2) -> rule4)) -> rule5))] Erin is red.[(((triple2) -> rule4))] Gary is cold.[(((triple3) -> rule5))] @2: Dave is cold.[(((((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule1)) -> rule4)) -> rule5))] Dave is red.[(((((triple1) -> rule1)) -> rule4))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2