Charlie is nice. Charlie is round. Harry is not kind. All blue, nice people are not red. Round people are blue. All round people are blue.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
All blue, nice people are not red.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "-"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple2) -> rule2) OR ((triple2) -> rule3))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple2) -> rule3))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not red.
True
4
proof
[(((((triple2) -> rule2) triple1) -> rule1) OR ((((triple2) -> rule3) triple1) -> rule1))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
False
4
inv-proof
[(((((triple2) -> rule2) triple1) -> rule1) OR ((((triple2) -> rule3) triple1) -> rule1))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is nice.[(triple1)] Charlie is round.[(triple2)] Harry is not kind.[(triple3)] @1: Charlie is blue.[(((triple2) -> rule2) OR ((triple2) -> rule3))] @2: Charlie is not red.[(((((triple2) -> rule2) triple1) -> rule1) OR ((((triple2) -> rule3) triple1) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Harry is not kind.
("Harry" "is" "kind" "-")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2