Anne is furry. Charlie is big. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is smart. Erin is furry. Erin is nice. Erin is quiet. Gary is furry. All smart, quiet things are rough. If something is smart and big then it is nice. If something is green then it is quiet. If something is smart and furry then it is big. If something is furry then it is smart. All big, furry things are green.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All smart, quiet things are rough.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is smart and big then it is nice.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and furry then it is big.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All big, furry things are green.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple9 OR ((((((((triple7) -> rule5) triple7) -> rule4) triple7) -> rule6)) -> rule3))]
("Erin" "is" "quiet" "+")
triple9
((((((((triple7) -> (rule5 % int4)) triple7) -> (rule4 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not furry.
False
1
inv-proof
[(triple7)]
("Erin" "is" "furry" "-")
triple7
Anne is smart.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is big.
True
4
proof
[(((((triple7) -> rule5) triple7) -> rule4))]
("Erin" "is" "big" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is not big.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule4))]
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is green.
True
6
proof
[(((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not green.
False
6
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Gary is quiet.
True
7
proof
[(((((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6)) -> rule3))]
("Gary" "is" "quiet" "+")
((((((((triple10) -> (rule5 % int4)) triple10) -> (rule4 % int3)) triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Anne is not quiet.
False
7
inv-proof
[(((((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6)) -> rule3))]
("Anne" "is" "quiet" "-")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Gary is rough.
True
10
proof
[(((((triple10) -> rule5) ((((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "rough" "+")
((((triple10) -> (rule5 % int5)) ((((((((triple10) -> (rule5 % int5)) triple10) -> (rule4 % int4)) triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is not rough.
False
10
inv-proof
[(((((triple10) -> rule5) ((((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "rough" "-")
((((triple10) -> (rule5 % int5)) ((((((((triple10) -> (rule5 % int5)) triple10) -> (rule4 % int4)) triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Charlie is nice.[(triple3 OR ((triple6 triple2) -> rule2))] Charlie is quiet.[(triple4)] Charlie is rough.[(triple5 OR ((triple6 triple4) -> rule1))] Charlie is smart.[(triple6)] Erin is furry.[(triple7)] Erin is nice.[(triple8 OR ((((triple7) -> rule5) ((((triple7) -> rule5) triple7) -> rule4)) -> rule2))] Erin is quiet.[(triple9 OR ((((((((triple7) -> rule5) triple7) -> rule4) triple7) -> rule6)) -> rule3))] Gary is furry.[(triple10)] @1: Anne is smart.[(((triple1) -> rule5))] Erin is smart.[(((triple7) -> rule5))] Gary is smart.[(((triple10) -> rule5))] @2: Anne is big.[(((((triple1) -> rule5) triple1) -> rule4))] Erin is big.[(((((triple7) -> rule5) triple7) -> rule4))] Erin is rough.[(((((triple7) -> rule5) triple9) -> rule1) OR ((((triple7) -> rule5) ((((((((triple7) -> rule5) triple7) -> rule4) triple7) -> rule6)) -> rule3)) -> rule1))] Gary is big.[(((((triple10) -> rule5) triple10) -> rule4))] @3: Anne is green.[(((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6))] Anne is nice.[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule4)) -> rule2))] Erin is green.[(((((((triple7) -> rule5) triple7) -> rule4) triple7) -> rule6))] Gary is green.[(((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6))] Gary is nice.[(((((triple10) -> rule5) ((((triple10) -> rule5) triple10) -> rule4)) -> rule2))] @4: Anne is quiet.[(((((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6)) -> rule3))] Gary is quiet.[(((((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6)) -> rule3))] @5: Anne is rough.[(((((triple1) -> rule5) ((((((((triple1) -> rule5) triple1) -> rule4) triple1) -> rule6)) -> rule3)) -> rule1))] Gary is rough.[(((((triple10) -> rule5) ((((((((triple10) -> rule5) triple10) -> rule4) triple10) -> rule6)) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple6 triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple6 triple4) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((((triple7) -> (rule5 % int3)) ((((triple7) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((((((((triple7) -> (rule5 % int4)) triple7) -> (rule4 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple10) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple7) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule5 % int5)) ((((((((triple7) -> (rule5 % int5)) triple7) -> (rule4 % int4)) triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Gary is big.
("Gary" "is" "big" "+")
((((triple10) -> (rule5 % int2)) triple10) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple7) -> (rule5 % int3)) triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple10) -> (rule5 % int3)) triple10) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((triple10) -> (rule5 % int3)) ((((triple10) -> (rule5 % int3)) triple10) -> (rule4 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((((triple10) -> (rule5 % int4)) triple10) -> (rule4 % int3)) triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5)) triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
((((triple10) -> (rule5 % int5)) ((((((((triple10) -> (rule5 % int5)) triple10) -> (rule4 % int4)) triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5