Anne is furry. Anne is kind. Anne is nice. Anne is smart. Erin is big. Erin is furry. Erin is rough. Fiona is blue. Gary is big. Gary is rough. If someone is rough and kind then they are blue. Kind, rough people are furry. If someone is blue then they are smart. Smart, nice people are rough. If someone is big then they are furry. Blue, big people are kind. All smart people are nice. If Erin is kind then Erin is nice. Nice, rough people are big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is rough and kind then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Kind, rough people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Smart, nice people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Blue, big people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Erin is kind then Erin is nice.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
Nice, rough people are big.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Erin is rough.
True
1
proof
[(triple7)]
("Erin" "is" "rough" "+")
triple7
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Gary is furry.
True
2
proof
[(((triple9) -> rule5))]
("Gary" "is" "furry" "+")
((triple9) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple9) -> rule5))]
("Gary" "is" "furry" "-")
((triple9) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple8) -> rule3)) -> rule7))]
("Fiona" "is" "nice" "+")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is not big.
False
5
inv-proof
[(((triple3 ((triple4 triple3) -> rule4)) -> rule9) OR ((((triple4) -> rule7) ((triple4 triple3) -> rule4)) -> rule9) OR ((triple3 ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9) OR ((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9))]
("Anne" "is" "big" "-")
((triple3 ((triple4 triple3) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4 triple3) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((triple3 ((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Fiona is rough.
True
6
proof
[(((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not rough.
False
6
inv-proof
[(((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4))]
("Fiona" "is" "rough" "-")
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
True
10
proof
[(((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9))]
("Fiona" "is" "big" "+")
((((((triple8) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is not big.
False
10
inv-proof
[(((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9))]
("Fiona" "is" "big" "-")
((((((triple8) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is furry.
True
11
proof
[(((((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule5) OR ((((triple8 ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule6) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule2))]
("Fiona" "is" "furry" "+")
((((((((triple8) -> (rule3 % int5))) -> (rule7 % int4)) ((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
((((triple8 ((((((triple8) -> (rule3 % int6))) -> (rule7 % int5)) ((((triple8) -> (rule3 % int6)) ((((triple8) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple8) -> (rule3 % int6)) ((((triple8) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is smart.
("Fiona" "is" "smart" "+")
int6
Fiona is not kind.
False
12
inv-proof
[(((triple8 ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule6))]
("Fiona" "is" "kind" "-")
((triple8 ((((((triple8) -> (rule3 % int5))) -> (rule7 % int4)) ((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is nice.
Unknown
rconc
[@4: Erin is nice.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule1 <- rule6 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not smart.
Unknown
inv-rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Gary is nice.
Unknown
rconc
[@4: Gary is nice.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule1 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is furry.[(triple1 OR ((triple2 ((triple4 triple3) -> rule4)) -> rule2) OR ((((triple3 ((triple4 triple3) -> rule4)) -> rule9)) -> rule5) OR ((triple2 ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule2) OR ((((((triple4) -> rule7) ((triple4 triple3) -> rule4)) -> rule9)) -> rule5) OR ((((triple3 ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9)) -> rule5) OR ((((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9)) -> rule5))] Anne is kind.[(triple2)] Anne is nice.[(triple3 OR ((triple4) -> rule7))] Anne is smart.[(triple4)] Erin is big.[(triple5)] Erin is furry.[(triple6 OR ((triple5) -> rule5))] Erin is rough.[(triple7)] Fiona is blue.[(triple8)] Gary is big.[(triple9)] Gary is rough.[(triple10)] @1: Anne is rough.[(((triple4 triple3) -> rule4) OR ((triple4 ((triple4) -> rule7)) -> rule4))] Fiona is smart.[(((triple8) -> rule3))] Gary is furry.[(((triple9) -> rule5))] @2: Anne is big.[(((triple3 ((triple4 triple3) -> rule4)) -> rule9) OR ((((triple4) -> rule7) ((triple4 triple3) -> rule4)) -> rule9) OR ((triple3 ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9) OR ((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule4)) -> rule9))] Anne is blue.[(((((triple4 triple3) -> rule4) triple2) -> rule1) OR ((((triple4 ((triple4) -> rule7)) -> rule4) triple2) -> rule1))] Fiona is nice.[(((((triple8) -> rule3)) -> rule7))] @3: Fiona is rough.[(((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4))] @4: Fiona is big.[(((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9))] @5: Fiona is furry.[(((((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule5) OR ((((triple8 ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule6) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule2))] Fiona is kind.[(((triple8 ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule4)) -> rule9)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2 ((triple4 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple3 ((triple4 triple3) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple2 ((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((triple4) -> (rule7 % int4)) ((triple4 triple3) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((triple3 ((triple4 ((triple4) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((((triple4) -> (rule7 % int4)) ((triple4 ((triple4) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple4) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
((triple5) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Anne is rough.
("Anne" "is" "rough" "+")
((triple4 triple3) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple9) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple3 ((triple4 triple3) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4 triple3) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((triple3 ((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple4 triple3) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple8) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((((triple8) -> (rule3 % int5))) -> (rule7 % int4)) ((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
((((triple8 ((((((triple8) -> (rule3 % int6))) -> (rule7 % int5)) ((((triple8) -> (rule3 % int6)) ((((triple8) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple8) -> (rule3 % int6)) ((((triple8) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is smart.
("Fiona" "is" "smart" "+")
int6
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8 ((((((triple8) -> (rule3 % int5))) -> (rule7 % int4)) ((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5