Charlie is white. Gary is quiet. Harry is big. If someone is kind and blue then they are white. All white, nice people are blue. All kind people are quiet. All big people are blue. All quiet people are big. If someone is quiet and big then they are kind.
Charlie is white.
("Charlie" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is kind and blue then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All white, nice people are blue.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and big then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Gary is big.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "big" "+")
((triple2) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is blue.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Gary" "is" "blue" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule6))]
("Gary" "is" "kind" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
True
8
proof
[(((((triple2 ((triple2) -> rule5)) -> rule6) ((((triple2) -> rule5)) -> rule4)) -> rule1))]
("Gary" "is" "white" "+")
((((triple2 ((triple2) -> (rule5 % int4))) -> (rule6 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is not white.
False
8
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule6) ((((triple2) -> rule5)) -> rule4)) -> rule1))]
("Gary" "is" "white" "-")
((((triple2 ((triple2) -> (rule5 % int4))) -> (rule6 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is quiet.
Unknown
rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "quiet" "+")
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is white.[(triple1)] Gary is quiet.[(triple2)] Harry is big.[(triple3)] @1: Gary is big.[(((triple2) -> rule5))] Harry is blue.[(((triple3) -> rule4))] @2: Gary is blue.[(((((triple2) -> rule5)) -> rule4))] Gary is kind.[(((triple2 ((triple2) -> rule5)) -> rule6))] @3: Gary is white.[(((((triple2 ((triple2) -> rule5)) -> rule6) ((((triple2) -> rule5)) -> rule4)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
((triple2) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple2 ((triple2) -> (rule5 % int4))) -> (rule6 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4