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