Charlie is kind. Dave is white. Gary is rough. If something is white then it is young. Nice, young things are cold. If something is young and rough then it is white.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Nice, young things are cold.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is young and rough then it is white.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Dave is young.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "young" "-")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] Dave is white.[(triple2)] Gary is rough.[(triple3)] @1: Dave is young.[(((triple2) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1