Charlie is big. Charlie is nice. Charlie is red. All kind people are not red. If someone is cold and not nice then they are red. If Charlie is cold then Charlie is white. If Charlie is kind and Charlie is red then Charlie is cold. If someone is red and not rough then they are kind. If someone is kind then they are big. Red, nice people are cold. If Charlie is rough and Charlie is not kind then Charlie is not big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
All kind people are not red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
If someone is cold and not nice then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "+"))
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is kind and Charlie is red then Charlie is cold.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is red and not rough then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is rough and Charlie is not kind then Charlie is not big.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "big" "-"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Charlie is cold.
True
3
proof
[(((triple3 triple2) -> rule7))]
("Charlie" "is" "cold" "+")
((triple3 triple2) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
3
inv-proof
[(((triple3 triple2) -> rule7))]
("Charlie" "is" "cold" "-")
((triple3 triple2) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
True
4
proof
[(((((triple3 triple2) -> rule7)) -> rule3))]
("Charlie" "is" "white" "+")
((((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple3 triple2) -> rule7)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2)] Charlie is red.[(triple3)] @1: Charlie is cold.[(((triple3 triple2) -> rule7))] @2: Charlie is white.[(((((triple3 triple2) -> rule7)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3 triple2) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2