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