Anne is furry. Anne is green. Anne is rough. Anne is smart. Anne is young. Charlie is blue. Charlie is furry. Charlie is green. Charlie is nice. Charlie is young. Dave is blue. Dave is furry. Fiona is blue. Fiona is furry. Fiona is rough. Fiona is young. Nice people are blue. All blue, nice people are furry. Blue people are furry. If Charlie is blue then Charlie is young. If Fiona is green and Fiona is furry then Fiona is rough. All furry people are rough.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All blue, nice people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is blue then Charlie is young.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "young" "+"))
If Fiona is green and Fiona is furry then Fiona is rough.
((("Fiona" "is" "green" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "rough" "+"))
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Charlie is blue.
True
1
proof
[(triple6 OR ((triple9) -> rule1))]
("Charlie" "is" "blue" "+")
triple6
((triple9) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Anne is not green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Charlie is rough.
True
2
proof
[(((triple7) -> rule6) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple6 triple9) -> rule2)) -> rule6) OR ((((((triple9) -> rule1)) -> rule3)) -> rule6) OR ((((((triple9) -> rule1) triple9) -> rule2)) -> rule6))]
("Charlie" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple6 triple9) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple9) -> (rule1 % int3)) triple9) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is not rough.
False
2
inv-proof
[(((triple12) -> rule6) OR ((((triple11) -> rule3)) -> rule6))]
("Dave" "is" "rough" "-")
((triple12) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is rough.[(triple3 OR ((triple1) -> rule6))] Anne is smart.[(triple4)] Anne is young.[(triple5)] Charlie is blue.[(triple6 OR ((triple9) -> rule1))] Charlie is furry.[(triple7 OR ((triple6) -> rule3) OR ((triple6 triple9) -> rule2) OR ((((triple9) -> rule1)) -> rule3) OR ((((triple9) -> rule1) triple9) -> rule2))] Charlie is green.[(triple8)] Charlie is nice.[(triple9)] Charlie is young.[(triple10 OR ((triple6) -> rule4) OR ((((triple9) -> rule1)) -> rule4))] Dave is blue.[(triple11)] Dave is furry.[(triple12 OR ((triple11) -> rule3))] Fiona is blue.[(triple13)] Fiona is furry.[(triple14 OR ((triple13) -> rule3))] Fiona is rough.[(triple15 OR ((triple14) -> rule6) OR ((((triple13) -> rule3)) -> rule6))] Fiona is young.[(triple16)] @1: Charlie is rough.[(((triple7) -> rule6) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple6 triple9) -> rule2)) -> rule6) OR ((((((triple9) -> rule1)) -> rule3)) -> rule6) OR ((((((triple9) -> rule1) triple9) -> rule2)) -> rule6))] Dave is rough.[(((triple12) -> rule6) OR ((((triple11) -> rule3)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
((triple9) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple6) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6 triple9) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple9) -> (rule1 % int2)) triple9) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
((triple6) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
((triple11) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple13
Fiona is furry.
("Fiona" "is" "furry" "+")
triple14
((triple13) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
((triple14) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple16
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple6 triple9) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple9) -> (rule1 % int3)) triple9) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2