Anne is rough. Anne is round. Charlie is furry. Charlie is red. Charlie is rough. Charlie is smart. Dave is rough. Dave is round. Erin is furry. Erin is smart. Erin is young. Round people are green. If someone is green then they are furry. Green people are round. Smart people are furry. All red people are young. If Anne is round then Anne is green. Young, round people are green. Furry, round people are smart. If someone is smart and green then they are red.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Anne is round then Anne is green.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "green" "+"))
Young, round people are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Furry, round people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and green then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Charlie is furry.
True
1
proof
[(triple3 OR ((triple6) -> rule4))]
("Charlie" "is" "furry" "+")
triple3
((triple6) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Anne is green.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule6))]
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple4) -> rule5))]
("Charlie" "is" "young" "-")
((triple4) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is furry.
True
3
proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple2) -> rule6)) -> rule2))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple2) -> rule6)) -> rule2))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) OR ((((((triple2) -> rule6)) -> rule2) triple2) -> rule8))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) OR ((((((triple2) -> rule6)) -> rule2) triple2) -> rule8))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is red.
True
8
proof
[(((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9))]
("Anne" "is" "red" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not red.
False
8
inv-proof
[(((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9))]
("Anne" "is" "red" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Dave is young.
True
9
proof
[(((((((((((triple8) -> rule1)) -> rule2) triple8) -> rule8) ((triple8) -> rule1)) -> rule9)) -> rule5))]
("Dave" "is" "young" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4)) triple8) -> (rule8 % int3)) ((triple8) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is not young.
False
9
inv-proof
[(((((((((((triple8) -> rule1)) -> rule2) triple8) -> rule8) ((triple8) -> rule1)) -> rule9)) -> rule5))]
("Dave" "is" "young" "-")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4)) triple8) -> (rule8 % int3)) ((triple8) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Erin is round.
Unknown
rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not green.
Unknown
inv-rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule7 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "green" "+")
Erin is not red.
Unknown
inv-rconc
[@4: Erin is red.[CWA. Example of deepest failure = (rule9 <- rule1 <- rule3 <- rule7 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Charlie is furry.[(triple3 OR ((triple6) -> rule4))] Charlie is red.[(triple4)] Charlie is rough.[(triple5)] Charlie is smart.[(triple6)] Dave is rough.[(triple7)] Dave is round.[(triple8)] Erin is furry.[(triple9 OR ((triple10) -> rule4))] Erin is smart.[(triple10)] Erin is young.[(triple11)] @1: Anne is green.[(((triple2) -> rule1) OR ((triple2) -> rule6))] Charlie is young.[(((triple4) -> rule5))] Dave is green.[(((triple8) -> rule1))] @2: Anne is furry.[(((((triple2) -> rule1)) -> rule2) OR ((((triple2) -> rule6)) -> rule2))] Dave is furry.[(((((triple8) -> rule1)) -> rule2))] @3: Anne is smart.[(((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) OR ((((((triple2) -> rule6)) -> rule2) triple2) -> rule8))] Dave is smart.[(((((((triple8) -> rule1)) -> rule2) triple8) -> rule8))] @4: Anne is red.[(((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9) OR ((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9))] Dave is red.[(((((((((triple8) -> rule1)) -> rule2) triple8) -> rule8) ((triple8) -> rule1)) -> rule9))] @5: Anne is young.[(((((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9)) -> rule5) OR ((((((((((triple2) -> rule1)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9)) -> rule5) OR ((((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule1)) -> rule9)) -> rule5) OR ((((((((((triple2) -> rule6)) -> rule2) triple2) -> rule8) ((triple2) -> rule6)) -> rule9)) -> rule5))] Dave is young.[(((((((((((triple8) -> rule1)) -> rule2) triple8) -> rule8) ((triple8) -> rule1)) -> rule9)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple6) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple10) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple11
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule1 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple2) -> (rule6 % int4))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((((((triple8) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule8 % int2)) ((triple8) -> (rule1 % int4))) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4)) triple2) -> (rule8 % int3)) ((triple2) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4)) triple2) -> (rule8 % int3)) ((triple2) -> (rule6 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4)) triple2) -> (rule8 % int3)) ((triple2) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4)) triple2) -> (rule8 % int3)) ((triple2) -> (rule6 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Dave is young.
("Dave" "is" "young" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4)) triple8) -> (rule8 % int3)) ((triple8) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5