Anne is big. Anne is young. Dave is big. Erin is big. Fiona is big. Fiona is nice. Fiona is white. Rough people are nice. All nice people are young. White people are furry. Big people are furry. Rough people are big. All white, young people are big. If someone is furry then they are rough. If someone is rough and not furry then they are smart. If someone is young then they are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All white, young people are big.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and not furry then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Fiona is white.
True
1
proof
[(triple7)]
("Fiona" "is" "white" "+")
triple7
Fiona is not nice.
False
1
inv-proof
[(triple6 OR ((((((triple5) -> rule4)) -> rule7)) -> rule1) OR ((((((triple7) -> rule3)) -> rule7)) -> rule1))]
("Fiona" "is" "nice" "-")
triple6
((((((triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Dave is furry.
True
2
proof
[(((triple3) -> rule4))]
("Dave" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple3) -> rule4))]
("Dave" "is" "furry" "-")
((triple3) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is rough.
True
3
proof
[(((((triple5) -> rule4)) -> rule7) OR ((((triple7) -> rule3)) -> rule7) OR ((((((triple7 ((triple6) -> rule2)) -> rule6)) -> rule4)) -> rule7))]
("Fiona" "is" "rough" "+")
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((((triple7 ((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Anne is not rough.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is nice.
True
4
proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule1))]
("Erin" "is" "nice" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule7)) -> rule1))]
("Dave" "is" "nice" "-")
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Erin is young.
True
5
proof
[(((((((((triple4) -> rule4)) -> rule7)) -> rule1)) -> rule2))]
("Erin" "is" "young" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Dave is not young.
False
5
inv-proof
[(((((((((triple3) -> rule4)) -> rule7)) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is smart.
True
6
proof
[(((((((((((triple3) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9))]
("Dave" "is" "smart" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Erin is not smart.
False
6
inv-proof
[(((((((((((triple4) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9))]
("Erin" "is" "smart" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is young.[(triple2 OR ((((((((triple1) -> rule4)) -> rule7)) -> rule1)) -> rule2))] Dave is big.[(triple3)] Erin is big.[(triple4)] Fiona is big.[(triple5 OR ((triple7 ((triple6) -> rule2)) -> rule6) OR ((((((triple7) -> rule3)) -> rule7)) -> rule5) OR ((triple7 ((((((((triple7) -> rule3)) -> rule7)) -> rule1)) -> rule2)) -> rule6))] Fiona is nice.[(triple6 OR ((((((triple5) -> rule4)) -> rule7)) -> rule1) OR ((((((triple7) -> rule3)) -> rule7)) -> rule1))] Fiona is white.[(triple7)] @1: Anne is furry.[(((triple1) -> rule4))] Anne is smart.[(((triple2) -> rule9) OR ((((((((((triple1) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9))] Dave is furry.[(((triple3) -> rule4))] Erin is furry.[(((triple4) -> rule4))] Fiona is furry.[(((triple5) -> rule4) OR ((triple7) -> rule3) OR ((((triple7 ((triple6) -> rule2)) -> rule6)) -> rule4))] Fiona is young.[(((triple6) -> rule2) OR ((((((((triple5) -> rule4)) -> rule7)) -> rule1)) -> rule2) OR ((((((((triple7) -> rule3)) -> rule7)) -> rule1)) -> rule2))] @2: Anne is rough.[(((((triple1) -> rule4)) -> rule7))] Dave is rough.[(((((triple3) -> rule4)) -> rule7))] Erin is rough.[(((((triple4) -> rule4)) -> rule7))] Fiona is rough.[(((((triple5) -> rule4)) -> rule7) OR ((((triple7) -> rule3)) -> rule7) OR ((((((triple7 ((triple6) -> rule2)) -> rule6)) -> rule4)) -> rule7))] Fiona is smart.[(((((triple6) -> rule2)) -> rule9) OR ((((((((((triple5) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9) OR ((((((((((triple7) -> rule3)) -> rule7)) -> rule1)) -> rule2)) -> rule9))] @3: Anne is nice.[(((((((triple1) -> rule4)) -> rule7)) -> rule1))] Dave is nice.[(((((((triple3) -> rule4)) -> rule7)) -> rule1))] Erin is nice.[(((((((triple4) -> rule4)) -> rule7)) -> rule1))] @4: Dave is young.[(((((((((triple3) -> rule4)) -> rule7)) -> rule1)) -> rule2))] Erin is young.[(((((((((triple4) -> rule4)) -> rule7)) -> rule1)) -> rule2))] @5: Dave is smart.[(((((((((((triple3) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9))] Erin is smart.[(((((((((((triple4) -> rule4)) -> rule7)) -> rule1)) -> rule2)) -> rule9))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
((triple7 ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple7 ((((((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
((((((triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule9 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((((((((triple1) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple7) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple7 ((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((((((triple5) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
((((((((triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((((triple7 ((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple6) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((((((((triple5) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
((((((((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Erin is smart.
("Erin" "is" "smart" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5