Anne is not quiet. Anne is not smart. Charlie is cold. Erin is kind. Erin is quiet. Fiona is blue. Fiona is cold. If someone is smart then they are quiet. All kind people are not young. All young people are not kind. Cold people are kind. All kind people are blue. All smart, quiet people are red. If someone is blue and cold then they are smart.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not smart.
("Anne" "is" "smart" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All kind people are not young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
All young people are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All smart, quiet people are red.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and cold then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Charlie is cold.
True
1
proof
[(triple3)]
("Charlie" "is" "cold" "+")
triple3
Anne is quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Charlie is kind.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is not smart.
False
3
inv-proof
[(((triple6 triple7) -> rule7) OR ((((((triple7) -> rule4)) -> rule5) triple7) -> rule7))]
("Fiona" "is" "smart" "-")
((triple6 triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not young.
True
3
proof
[(((((triple7) -> rule4)) -> rule2))]
("Fiona" "is" "young" "-")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple6 triple7) -> rule7)) -> rule1) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is red.
True
8
proof
[(((((triple6 triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((triple6 triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6))]
("Fiona" "is" "red" "+")
((((triple6 triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((triple6 triple7) -> (rule7 % int5)) ((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) triple7) -> (rule7 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not red.
False
8
inv-proof
[(((((triple6 triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((triple6 triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6))]
("Fiona" "is" "red" "-")
((((triple6 triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((triple6 triple7) -> (rule7 % int5)) ((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) triple7) -> (rule7 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Charlie is quiet.
True
6
proof
[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is not quiet.
False
6
inv-proof
[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is red.
True
12
proof
[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7) ((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1)) -> rule6))]
("Charlie" "is" "red" "+")
((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3)) ((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Charlie is not red.
False
12
inv-proof
[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7) ((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1)) -> rule6))]
("Charlie" "is" "red" "-")
((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3)) ((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "smart" "+")
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Erin" "is" "red" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is not quiet.[(triple1)] Anne is not smart.[(triple2)] Charlie is cold.[(triple3)] Erin is kind.[(triple4)] Erin is quiet.[(triple5)] Fiona is blue.[(triple6 OR ((((triple7) -> rule4)) -> rule5))] Fiona is cold.[(triple7)] @1: Charlie is kind.[(((triple3) -> rule4))] Erin is blue.[(((triple4) -> rule5))] Erin is not young.[(((triple4) -> rule2))] Fiona is kind.[(((triple7) -> rule4))] Fiona is smart.[(((triple6 triple7) -> rule7) OR ((((((triple7) -> rule4)) -> rule5) triple7) -> rule7))] @2: Charlie is blue.[(((((triple3) -> rule4)) -> rule5))] Charlie is not young.[(((((triple3) -> rule4)) -> rule2))] Fiona is not young.[(((((triple7) -> rule4)) -> rule2))] Fiona is quiet.[(((((triple6 triple7) -> rule7)) -> rule1) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1))] @3: Charlie is smart.[(((((((triple3) -> rule4)) -> rule5) triple3) -> rule7))] Fiona is red.[(((((triple6 triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((triple6 triple7) -> rule7)) -> rule1)) -> rule6) OR ((((triple6 triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6) OR ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7) ((((((((triple7) -> rule4)) -> rule5) triple7) -> rule7)) -> rule1)) -> rule6))] @4: Charlie is quiet.[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))] @5: Charlie is red.[(((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7) ((((((((triple3) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1)) -> rule6))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
((triple4) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple7) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6 triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Fiona is not young.
("Fiona" "is" "young" "-")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((triple6 triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((triple6 triple7) -> (rule7 % int5)) ((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) triple7) -> (rule7 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3)) ((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3)) ((((((((triple3) -> (rule4 % int5))) -> (rule5 % int4)) triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5