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