Charlie is big. Charlie is kind. Charlie is red. Charlie is smart. Dave is not big. Dave is kind. Gary is rough. Harry is not kind. Harry is nice. Harry is not red. Harry is rough. Harry is not smart. White people are smart. If someone is kind then they are white. Smart people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Charlie is smart.
True
1
proof
[(triple4 OR ((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
triple4
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is red.
False
1
inv-proof
[(triple10)]
("Harry" "is" "red" "+")
triple10
Charlie is white.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple4) -> rule3) OR ((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "-")
((triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Dave is smart.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Gary is not nice.
Unknown
inv-rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is red.[(triple3)] Charlie is smart.[(triple4 OR ((((triple2) -> rule2)) -> rule1))] Dave is kind.[(triple6)] Dave is not big.[(triple5)] Gary is rough.[(triple7)] Harry is nice.[(triple9)] Harry is not kind.[(triple8)] Harry is not red.[(triple10)] Harry is not smart.[(triple12)] Harry is rough.[(triple11)] @1: Charlie is nice.[(((triple4) -> rule3) OR ((((((triple2) -> rule2)) -> rule1)) -> rule3))] Charlie is white.[(((triple2) -> rule2))] Dave is white.[(((triple6) -> rule2))] @2: Dave is smart.[(((((triple6) -> rule2)) -> rule1))] @3: Dave is nice.[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is not big.
("Dave" "is" "big" "-")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is not kind.
("Harry" "is" "kind" "-")
triple8
Harry is not red.
("Harry" "is" "red" "-")
triple10
Harry is not smart.
("Harry" "is" "smart" "-")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple6) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3