Charlie is not cold. Charlie is nice. Charlie is red. Dave is cold. Dave is green. Dave is kind. Dave is young. If something is young and red then it is not cold. All rough things are young. All rough, young things are kind. If something is nice then it is rough. If something is nice and not young then it is green. If Charlie is green and Charlie is not nice then Charlie is cold.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is young and red then it is not cold.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "-"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
All rough, young things are kind.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is nice and not young then it is green.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
If Charlie is green and Charlie is not nice then Charlie is cold.
((("Charlie" "is" "green" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "cold" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is nice.[(triple2)] Charlie is not cold.[(triple1 OR ((((((triple2) -> rule4)) -> rule2) triple3) -> rule1))] Charlie is red.[(triple3)] Dave is cold.[(triple4)] Dave is green.[(triple5)] Dave is kind.[(triple6)] Dave is young.[(triple7)] @1: Charlie is rough.[(((triple2) -> rule4))] @2: Charlie is young.[(((((triple2) -> rule4)) -> rule2))] @3: Charlie is kind.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3