Anne is blue. Anne is round. Charlie is white. Erin is blue. Erin is round. Harry is blue. Harry is nice. Harry is rough. Harry is round. Harry is white. If Anne is blue and Anne is white then Anne is nice. All quiet, nice people are round. If someone is blue then they are quiet. If someone is round and rough then they are red. If someone is blue and rough then they are nice. If someone is white then they are rough. Blue people are nice. If someone is white then they are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is blue and Anne is white then Anne is nice.
((("Anne" "is" "blue" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "nice" "+"))
All quiet, nice people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and rough then they are red.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and rough then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Harry is nice.
True
1
proof
[(triple7 OR ((triple6) -> rule7) OR ((triple6 triple8) -> rule5) OR ((triple6 ((triple10) -> rule6)) -> rule5) OR ((triple6 ((triple10) -> rule8)) -> rule5))]
("Harry" "is" "nice" "+")
triple7
((triple6) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 triple8) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 ((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple6 ((triple10) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple6) -> rule3))]
("Harry" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple6) -> rule3))]
("Harry" "is" "quiet" "-")
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "rough" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is round.[(triple2 OR ((((triple1) -> rule3) ((triple1) -> rule7)) -> rule2))] Charlie is white.[(triple3)] Erin is blue.[(triple4)] Erin is round.[(triple5 OR ((((triple4) -> rule3) ((triple4) -> rule7)) -> rule2))] Harry is blue.[(triple6)] Harry is nice.[(triple7 OR ((triple6) -> rule7) OR ((triple6 triple8) -> rule5) OR ((triple6 ((triple10) -> rule6)) -> rule5) OR ((triple6 ((triple10) -> rule8)) -> rule5))] Harry is rough.[(triple8 OR ((triple10) -> rule6) OR ((triple10) -> rule8))] Harry is round.[(triple9 OR ((((triple6) -> rule3) triple7) -> rule2) OR ((((triple6) -> rule3) ((triple6) -> rule7)) -> rule2) OR ((((triple6) -> rule3) ((triple6 triple8) -> rule5)) -> rule2) OR ((((triple6) -> rule3) ((triple6 ((triple10) -> rule6)) -> rule5)) -> rule2) OR ((((triple6) -> rule3) ((triple6 ((triple10) -> rule8)) -> rule5)) -> rule2))] Harry is white.[(triple10)] @1: Anne is nice.[(((triple1) -> rule7))] Anne is quiet.[(((triple1) -> rule3))] Charlie is rough.[(((triple3) -> rule6) OR ((triple3) -> rule8))] Erin is nice.[(((triple4) -> rule7))] Erin is quiet.[(((triple4) -> rule3))] Harry is quiet.[(((triple6) -> rule3))] Harry is red.[(((triple9 triple8) -> rule4) OR ((triple9 ((triple10) -> rule6)) -> rule4) OR ((triple9 ((triple10) -> rule8)) -> rule4) OR ((((((triple6) -> rule3) triple7) -> rule2) triple8) -> rule4) OR ((((((triple6) -> rule3) triple7) -> rule2) ((triple10) -> rule6)) -> rule4) OR ((((((triple6) -> rule3) triple7) -> rule2) ((triple10) -> rule8)) -> rule4) OR ((((((triple6) -> rule3) ((triple6) -> rule7)) -> rule2) triple8) -> rule4) OR ((((((triple6) -> rule3) ((triple6 triple8) -> rule5)) -> rule2) triple8) -> rule4) OR ((((((triple6) -> rule3) ((triple6) -> rule7)) -> rule2) ((triple10) -> rule6)) -> rule4) OR ((((((triple6) -> rule3) ((triple6) -> rule7)) -> rule2) ((triple10) -> rule8)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 triple8) -> rule5)) -> rule2) ((triple10) -> rule6)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 triple8) -> rule5)) -> rule2) ((triple10) -> rule8)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule6)) -> rule5)) -> rule2) triple8) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule8)) -> rule5)) -> rule2) triple8) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule6)) -> rule5)) -> rule2) ((triple10) -> rule6)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule6)) -> rule5)) -> rule2) ((triple10) -> rule8)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule8)) -> rule5)) -> rule2) ((triple10) -> rule6)) -> rule4) OR ((((((triple6) -> rule3) ((triple6 ((triple10) -> rule8)) -> rule5)) -> rule2) ((triple10) -> rule8)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((((triple4) -> (rule3 % int3)) ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple6) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 triple8) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 ((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple6 ((triple10) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple8
((triple10) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple9
((((triple6) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple6) -> (rule3 % int3)) ((triple6 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple6) -> (rule3 % int4)) ((triple6 ((triple10) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((triple6) -> (rule3 % int4)) ((triple6 ((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple3) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple9 triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple9 ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple6) -> (rule3 % int3)) triple7) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple6) -> (rule3 % int4)) triple7) -> (rule2 % int3)) ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((triple6) -> (rule3 % int4)) triple7) -> (rule2 % int3)) ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((triple6) -> (rule3 % int4)) ((triple6) -> (rule7 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((triple6) -> (rule3 % int4)) ((triple6 triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((triple6) -> (rule3 % int5)) ((triple6) -> (rule7 % int4))) -> (rule2 % int3)) ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6) -> (rule7 % int4))) -> (rule2 % int3)) ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 triple8) -> (rule5 % int4))) -> (rule2 % int3)) ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 triple8) -> (rule5 % int4))) -> (rule2 % int3)) ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple10) -> (rule6 % int4))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple10) -> (rule8 % int4))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple10) -> (rule6 % int4))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
((((((triple6) -> (rule3 % int5)) ((triple6 ((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple10) -> (rule8 % int4))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5