Charlie is green. Gary is big. All rough people are quiet. All nice people are blue. If someone is big then they are nice. Nice, blue people are round. All quiet people are round. If Charlie is nice and Charlie is not big then Charlie is blue.
Charlie is green.
("Charlie" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Nice, blue people are round.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Charlie is nice and Charlie is not big then Charlie is blue.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "blue" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Gary is nice.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Gary" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Gary" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
True
6
proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule2)) -> rule4))]
("Gary" "is" "round" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not round.
False
6
inv-proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule2)) -> rule4))]
("Gary" "is" "round" "-")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is green.[(triple1)] Gary is big.[(triple2)] @1: Gary is nice.[(((triple2) -> rule3))] @2: Gary is blue.[(((((triple2) -> rule3)) -> rule2))] @3: Gary is round.[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule2)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3