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