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