Anne is blue. Anne is rough. Anne is white. Dave is white. Erin is kind. Harry is blue. Harry is kind. If Dave is red and Dave is not kind then Dave is not rough. Green, rough things are red. If Anne is green then Anne is blue. Red, rough things are quiet. All blue things are quiet. If something is quiet then it is green. If something is white and blue then it is rough. All green, quiet things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Dave is red and Dave is not kind then Dave is not rough.
((("Dave" "is" "red" "+") ("Dave" "is" "kind" "~")) -> ("Dave" "is" "rough" "-"))
Green, rough things are red.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Anne is green then Anne is blue.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "blue" "+"))
Red, rough things are quiet.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is white and blue then it is rough.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All green, quiet things are white.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Anne is rough.
True
1
proof
[(triple2 OR ((triple3 triple1) -> rule7) OR ((((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8) triple1) -> rule7))]
("Anne" "is" "rough" "+")
triple2
((triple3 triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3)) ((triple1) -> (rule5 % int4))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is not white.
False
1
inv-proof
[(triple3 OR ((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8))]
("Anne" "is" "white" "-")
triple3
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1) -> (rule5 % int3))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Harry is quiet.
True
2
proof
[(((triple6) -> rule5))]
("Harry" "is" "quiet" "+")
((triple6) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple6) -> rule5))]
("Harry" "is" "quiet" "-")
((triple6) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule6))]
("Harry" "is" "green" "-")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is red.
True
5
proof
[(((((((triple1) -> rule5)) -> rule6) triple2) -> rule2) OR ((((((triple1) -> rule5)) -> rule6) ((triple3 triple1) -> rule7)) -> rule2) OR ((((((triple1) -> rule5)) -> rule6) ((((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8) triple1) -> rule7)) -> rule2))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((triple1) -> (rule5 % int4))) -> (rule6 % int3)) ((triple3 triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((triple1) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple1) -> (rule5 % int5))) -> (rule6 % int4)) ((triple1) -> (rule5 % int5))) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Harry is not white.
False
6
inv-proof
[(((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8))]
("Harry" "is" "white" "-")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2)) ((triple6) -> (rule5 % int3))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is rough.
True
8
proof
[(((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7))]
("Harry" "is" "rough" "+")
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3)) ((triple6) -> (rule5 % int4))) -> (rule8 % int2)) triple6) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not rough.
False
8
inv-proof
[(((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7))]
("Harry" "is" "rough" "-")
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3)) ((triple6) -> (rule5 % int4))) -> (rule8 % int2)) triple6) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is red.
True
12
proof
[(((((((triple6) -> rule5)) -> rule6) ((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7)) -> rule2))]
("Harry" "is" "red" "+")
((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((triple6) -> (rule5 % int5))) -> (rule8 % int3)) triple6) -> (rule7 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is not red.
False
12
inv-proof
[(((((((triple6) -> rule5)) -> rule6) ((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7)) -> rule2))]
("Harry" "is" "red" "-")
((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((triple6) -> (rule5 % int5))) -> (rule8 % int3)) triple6) -> (rule7 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule7 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not green.
Unknown
inv-rconc
[@3: Dave is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Erin" "is" "quiet" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2 OR ((triple3 triple1) -> rule7) OR ((((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8) triple1) -> rule7))] Anne is white.[(triple3 OR ((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8))] Dave is white.[(triple4)] Erin is kind.[(triple5)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule5))] Harry is quiet.[(((triple6) -> rule5))] @2: Anne is green.[(((((triple1) -> rule5)) -> rule6))] Harry is green.[(((((triple6) -> rule5)) -> rule6))] @3: Anne is red.[(((((((triple1) -> rule5)) -> rule6) triple2) -> rule2) OR ((((((triple1) -> rule5)) -> rule6) ((triple3 triple1) -> rule7)) -> rule2) OR ((((((triple1) -> rule5)) -> rule6) ((((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule8) triple1) -> rule7)) -> rule2))] Harry is white.[(((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8))] @4: Harry is rough.[(((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7))] @5: Harry is red.[(((((((triple6) -> rule5)) -> rule6) ((((((((triple6) -> rule5)) -> rule6) ((triple6) -> rule5)) -> rule8) triple6) -> rule7)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
((triple3 triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3)) ((triple1) -> (rule5 % int4))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
triple3
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1) -> (rule5 % int3))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((triple1) -> (rule5 % int4))) -> (rule6 % int3)) ((triple3 triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((triple1) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple1) -> (rule5 % int5))) -> (rule6 % int4)) ((triple1) -> (rule5 % int5))) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Harry is white.
("Harry" "is" "white" "+")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2)) ((triple6) -> (rule5 % int3))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3)) ((triple6) -> (rule5 % int4))) -> (rule8 % int2)) triple6) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) ((triple6) -> (rule5 % int5))) -> (rule8 % int3)) triple6) -> (rule7 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5