Charlie is furry. Fiona is big. Gary is kind. Big people are smart. Furry people are not blue. If someone is kind and nice then they are not blue. Nice people are kind. If someone is smart and not furry then they are kind. If someone is big then they are nice. If someone is big and not young then they are nice. All young people are big.
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Furry people are not blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "-"))
If someone is kind and nice then they are not blue.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "-"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart and not furry then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and not young then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Charlie is not blue.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Fiona is kind.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("Fiona" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Fiona" "is" "kind" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
True
6
proof
[(((((((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule3))]
("Fiona" "is" "blue" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is blue.
False
6
inv-proof
[(((((((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule3))]
("Fiona" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not kind.
Unknown
inv-rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule8 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is furry.[(triple1)] Fiona is big.[(triple2)] Gary is kind.[(triple3)] @1: Charlie is not blue.[(((triple1) -> rule2))] Fiona is nice.[(((triple2) -> rule6))] Fiona is smart.[(((triple2) -> rule1))] @2: Fiona is kind.[(((((triple2) -> rule6)) -> rule4))] @3: Fiona is not blue.[(((((((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3