Anne is nice. Erin is nice. Erin is smart. Erin is white. Erin is young. Fiona is big. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is white. Fiona is young. Harry is big. Harry is cold. Harry is furry. Harry is white. Harry is young. All furry people are big. Big people are young. If someone is young and white then they are cold. If Anne is young then Anne is white. All furry, white people are nice. If Anne is nice then Anne is furry. All smart, nice people are white. If Harry is young then Harry is big. All smart people are nice.
Anne is nice.
("Anne" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is young and white then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Anne is young then Anne is white.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "white" "+"))
All furry, white people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Anne is nice then Anne is furry.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "+"))
All smart, nice people are white.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Harry is young then Harry is big.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "big" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Harry is cold.
True
1
proof
[(triple13 OR ((triple16 triple15) -> rule3) OR ((((triple12) -> rule2) triple15) -> rule3) OR ((((((triple14) -> rule1)) -> rule2) triple15) -> rule3))]
("Harry" "is" "cold" "+")
triple13
((triple16 triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple12) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple14) -> (rule1 % int3))) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Fiona is not nice.
False
1
inv-proof
[(triple9 OR ((triple8 triple10) -> rule5))]
("Fiona" "is" "nice" "-")
triple9
((triple8 triple10) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Erin is cold.
True
3
proof
[(((triple5 triple4) -> rule3) OR ((triple5 ((triple3 triple2) -> rule7)) -> rule3) OR ((triple5 ((triple3 ((triple3) -> rule9)) -> rule7)) -> rule3))]
("Erin" "is" "cold" "+")
((triple5 triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple5 ((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple5 ((triple3 ((triple3) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not cold.
False
3
inv-proof
[(((triple5 triple4) -> rule3) OR ((triple5 ((triple3 triple2) -> rule7)) -> rule3) OR ((triple5 ((triple3 ((triple3) -> rule9)) -> rule7)) -> rule3))]
("Erin" "is" "cold" "-")
((triple5 triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple5 ((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple5 ((triple3 ((triple3) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Anne is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Anne" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not young.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
True
5
proof
[(((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4))]
("Anne" "is" "white" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not white.
False
5
inv-proof
[(((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4))]
("Anne" "is" "white" "-")
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is cold.
True
10
proof
[(((((((((triple1) -> rule6)) -> rule1)) -> rule2) ((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4)) -> rule3))]
("Anne" "is" "cold" "+")
((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Anne is not cold.
False
10
inv-proof
[(((((((((triple1) -> rule6)) -> rule1)) -> rule2) ((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4)) -> rule3))]
("Anne" "is" "cold" "-")
((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Erin is nice.[(triple2 OR ((triple3) -> rule9))] Erin is smart.[(triple3)] Erin is white.[(triple4 OR ((triple3 triple2) -> rule7) OR ((triple3 ((triple3) -> rule9)) -> rule7))] Erin is young.[(triple5)] Fiona is big.[(triple6 OR ((triple8) -> rule1))] Fiona is cold.[(triple7 OR ((triple11 triple10) -> rule3) OR ((((triple6) -> rule2) triple10) -> rule3) OR ((((((triple8) -> rule1)) -> rule2) triple10) -> rule3))] Fiona is furry.[(triple8)] Fiona is nice.[(triple9 OR ((triple8 triple10) -> rule5))] Fiona is white.[(triple10)] Fiona is young.[(triple11 OR ((triple6) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] Harry is big.[(triple12 OR ((triple14) -> rule1) OR ((triple16) -> rule8))] Harry is cold.[(triple13 OR ((triple16 triple15) -> rule3) OR ((((triple12) -> rule2) triple15) -> rule3) OR ((((((triple14) -> rule1)) -> rule2) triple15) -> rule3))] Harry is furry.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16 OR ((triple12) -> rule2) OR ((((triple14) -> rule1)) -> rule2))] @1: Anne is furry.[(((triple1) -> rule6))] Erin is cold.[(((triple5 triple4) -> rule3) OR ((triple5 ((triple3 triple2) -> rule7)) -> rule3) OR ((triple5 ((triple3 ((triple3) -> rule9)) -> rule7)) -> rule3))] Harry is nice.[(((triple14 triple15) -> rule5))] @2: Anne is big.[(((((triple1) -> rule6)) -> rule1))] @3: Anne is young.[(((((((triple1) -> rule6)) -> rule1)) -> rule2))] @4: Anne is white.[(((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4))] @5: Anne is cold.[(((((((((triple1) -> rule6)) -> rule1)) -> rule2) ((((((((triple1) -> rule6)) -> rule1)) -> rule2)) -> rule4)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
((triple3) -> (rule9 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
((triple3 triple2) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple3 ((triple3) -> (rule9 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
((triple8) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
((triple11 triple10) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple8 triple10) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple6) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple12
((triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple16) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple16 triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple12) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple14) -> (rule1 % int3))) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple5 triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple5 ((triple3 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple5 ((triple3 ((triple3) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple14 triple15) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((((((((triple1) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5