Charlie is rough. Gary is red. Gary is smart. All big things are rough. Nice things are white. If something is white then it is not green. If something is rough then it is nice. If something is nice then it is red. If something is white and not rough then it is red.
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is white then it is not green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "-"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is white and not rough then it is red.
((("something" "is" "white" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is nice.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not green.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is green.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is white.
Unknown
rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule1 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is rough.[(triple1)] Gary is red.[(triple2)] Gary is smart.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule4))] @2: Charlie is red.[(((((triple1) -> rule4)) -> rule5))] Charlie is white.[(((((triple1) -> rule4)) -> rule2))] @3: Charlie is not green.[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not green.
("Charlie" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3