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