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