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