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