Charlie is nice. Harry is red. All red people are blue. Kind, round people are not white. If someone is nice then they are not white. If Harry is blue then Harry is nice. All nice, white people are red. If someone is white and not round then they are red. Blue people are nice. Blue people are kind.
Charlie is nice.
("Charlie" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Kind, round people are not white.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
If someone is nice then they are not white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "-"))
If Harry is blue then Harry is nice.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
All nice, white people are red.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is white and not round then they are red.
((("someone" "is" "white" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Harry is blue.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule1)) -> rule7))]
("Harry" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule1)) -> rule7))]
("Harry" "is" "nice" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not white.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))]
("Harry" "is" "white" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))]
("Harry" "is" "white" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is kind.
Unknown
rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is nice.[(triple1)] Harry is red.[(triple2)] @1: Charlie is not white.[(((triple1) -> rule3))] Harry is blue.[(((triple2) -> rule1))] @2: Harry is kind.[(((((triple2) -> rule1)) -> rule8))] Harry is nice.[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule1)) -> rule7))] @3: Harry is not white.[(((((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
((triple1) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3