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