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