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