Charlie is round. Dave is not blue. Gary is not cold. Kind people are rough. All round, kind people are not nice. Smart, rough people are cold. If someone is round then they are cold. Kind, blue people are round. All nice, cold people are blue.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All round, kind people are not nice.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
Smart, rough people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Kind, blue people are round.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All nice, cold people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Dave is not blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Charlie is cold.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is round.[(triple1)] Dave is not blue.[(triple2)] Gary is not cold.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule4))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Gary is not cold.
("Gary" "is" "cold" "-")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1