Anne is not nice. Charlie is kind. Fiona is furry. Fiona is nice. Harry is not furry. Harry is nice. Harry is not white. All white, green things are smart. If Fiona is nice then Fiona is white. If something is smart and white then it is quiet. If something is furry and white then it is green. All white things are green. If something is green then it is furry. All quiet things are not kind. Green, quiet things are nice.
Anne is not nice.
("Anne" "is" "nice" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not white.
("Harry" "is" "white" "-")
All white, green things are smart.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Fiona is nice then Fiona is white.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "white" "+"))
If something is smart and white then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and white then it is green.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All quiet things are not kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
Green, quiet things are nice.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Harry is not white.
True
1
proof
[(triple7)]
("Harry" "is" "white" "-")
triple7
Fiona is not nice.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "nice" "-")
triple4
Fiona is white.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "white" "+")
((triple4) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple4) -> rule2))]
("Fiona" "is" "white" "-")
((triple4) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
True
3
proof
[(((((triple4) -> rule2)) -> rule5) OR ((triple3 ((triple4) -> rule2)) -> rule4))]
("Fiona" "is" "green" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((triple3 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule5) OR ((triple3 ((triple4) -> rule2)) -> rule4))]
("Fiona" "is" "green" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((triple3 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is smart.
True
6
proof
[(((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) OR ((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1))]
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((triple4) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not smart.
False
6
inv-proof
[(((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) OR ((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1))]
("Fiona" "is" "smart" "-")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((triple4) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is quiet.
True
9
proof
[(((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3) OR ((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3))]
("Fiona" "is" "quiet" "+")
((((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
((((((triple4) -> (rule2 % int4)) ((triple3 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not quiet.
False
9
inv-proof
[(((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3) OR ((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3))]
("Fiona" "is" "quiet" "-")
((((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
((((((triple4) -> (rule2 % int4)) ((triple3 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not kind.
True
10
proof
[(((((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
((((((((triple4) -> (rule2 % int5)) ((triple3 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Fiona is kind.
False
10
inv-proof
[(((((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7))]
("Fiona" "is" "kind" "+")
((((((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
((((((((triple4) -> (rule2 % int5)) ((triple3 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is not nice.[(triple1)] Charlie is kind.[(triple2)] Fiona is furry.[(triple3 OR ((((((triple4) -> rule2)) -> rule5)) -> rule6))] Fiona is nice.[(triple4)] Harry is nice.[(triple6)] Harry is not furry.[(triple5)] Harry is not white.[(triple7)] @1: Fiona is white.[(((triple4) -> rule2))] @2: Fiona is green.[(((((triple4) -> rule2)) -> rule5) OR ((triple3 ((triple4) -> rule2)) -> rule4))] @3: Fiona is smart.[(((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) OR ((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1))] @4: Fiona is quiet.[(((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3) OR ((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3))] @5: Fiona is not kind.[(((((((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule5)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule2) ((triple3 ((triple4) -> rule2)) -> rule4)) -> rule1) ((triple4) -> rule2)) -> rule3)) -> rule7))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is not furry.
("Harry" "is" "furry" "-")
triple5
Harry is not white.
("Harry" "is" "white" "-")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((triple3 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((triple4) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
((((((triple4) -> (rule2 % int4)) ((triple3 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not kind.
("Fiona" "is" "kind" "-")
((((((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
((((((((triple4) -> (rule2 % int5)) ((triple3 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int5))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5