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