Anne is big. Anne is kind. Anne is rough. Anne is round. Anne is white. Dave is blue. Dave is kind. Dave is round. Fiona is blue. Fiona is furry. Fiona is kind. Fiona is white. Harry is big. Harry is blue. Harry is rough. Harry is white. All rough things are blue. Big things are white. Round things are big. White things are furry. If Fiona is furry then Fiona is kind. All kind things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
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 kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Fiona is furry then Fiona is kind.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "kind" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple15)]
("Harry" "is" "rough" "+")
triple15
Anne is not round.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule6))]
("Anne" "is" "round" "-")
triple4
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is big.
True
3
proof
[(((((triple11) -> rule6)) -> rule3) OR ((((((triple10) -> rule5)) -> rule6)) -> rule3) OR ((((((((triple12) -> rule4)) -> rule5)) -> rule6)) -> rule3))]
("Fiona" "is" "big" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((((triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is not big.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule3) OR ((((((triple10) -> rule5)) -> rule6)) -> rule3) OR ((((((((triple12) -> rule4)) -> rule5)) -> rule6)) -> rule3))]
("Fiona" "is" "big" "-")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((((triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Dave is furry.
True
4
proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule4) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
("Dave" "is" "furry" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not furry.
False
4
inv-proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule4) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
("Dave" "is" "furry" "-")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule3) OR ((((triple2) -> rule6)) -> rule3))] Anne is kind.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4 OR ((triple2) -> rule6))] Anne is white.[(triple5 OR ((triple1) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((((triple2) -> rule6)) -> rule3)) -> rule2))] Dave is blue.[(triple6)] Dave is kind.[(triple7)] Dave is round.[(triple8 OR ((triple7) -> rule6))] Fiona is blue.[(triple9)] Fiona is furry.[(triple10 OR ((triple12) -> rule4) OR ((((((((triple11) -> rule6)) -> rule3)) -> rule2)) -> rule4))] Fiona is kind.[(triple11 OR ((triple10) -> rule5) OR ((((triple12) -> rule4)) -> rule5))] Fiona is white.[(triple12 OR ((((((triple11) -> rule6)) -> rule3)) -> rule2) OR ((((((((triple10) -> rule5)) -> rule6)) -> rule3)) -> rule2))] Harry is big.[(triple13)] Harry is blue.[(triple14 OR ((triple15) -> rule1))] Harry is rough.[(triple15)] Harry is white.[(triple16 OR ((triple13) -> rule2))] @1: Anne is blue.[(((triple3) -> rule1))] Anne is furry.[(((triple5) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule2)) -> rule4))] Dave is big.[(((triple8) -> rule3) OR ((((triple7) -> rule6)) -> rule3))] Fiona is round.[(((triple11) -> rule6) OR ((((triple10) -> rule5)) -> rule6) OR ((((((triple12) -> rule4)) -> rule5)) -> rule6))] Harry is furry.[(((triple16) -> rule4) OR ((((triple13) -> rule2)) -> rule4))] @2: Dave is white.[(((((triple8) -> rule3)) -> rule2) OR ((((((triple7) -> rule6)) -> rule3)) -> rule2))] Fiona is big.[(((((triple11) -> rule6)) -> rule3) OR ((((((triple10) -> rule5)) -> rule6)) -> rule3) OR ((((((((triple12) -> rule4)) -> rule5)) -> rule6)) -> rule3))] @3: Dave is furry.[(((((((triple8) -> rule3)) -> rule2)) -> rule4) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
((triple7) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
((triple12) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((((((triple11) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
((triple10) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((((triple10) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple14
((triple15) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple13) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((triple8) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple11) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((triple16) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((((triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4