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