Charlie is blue. Charlie is not cold. Charlie is kind. Charlie is not red. Gary is not cold. Gary is red. Gary is rough. Round, blue things are cold. If something is kind and not round then it is not cold. If something is kind and not red then it is blue. If something is nice then it is blue. All red, nice things are kind. All round things are not rough. All blue things are rough. If Charlie is kind then Charlie is blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Round, blue things are cold.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is kind and not round then it is not cold.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "-"))
If something is kind and not red then it is blue.
((("something" "is" "kind" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All red, nice things are kind.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All round things are not rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "-"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Charlie is kind then Charlie is blue.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple1) -> rule7) OR ((((triple3) -> rule8)) -> rule7) OR ((((triple3 triple4) -> rule3)) -> rule7))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule7) OR ((((triple3) -> rule8)) -> rule7) OR ((((triple3 triple4) -> rule3)) -> rule7))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Charlie is blue.[(triple1 OR ((triple3) -> rule8) OR ((triple3 triple4) -> rule3))] Charlie is kind.[(triple3)] Charlie is not cold.[(triple2)] Charlie is not red.[(triple4)] Gary is not cold.[(triple5)] Gary is red.[(triple6)] Gary is rough.[(triple7)] @1: Charlie is rough.[(((triple1) -> rule7) OR ((((triple3) -> rule8)) -> rule7) OR ((((triple3 triple4) -> rule3)) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple3 triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2