Anne is big. Anne is green. Anne is quiet. Erin is rough. Fiona is cold. Fiona is rough. Harry is rough. Rough, smart people are nice. Cold, quiet people are big. All smart people are rough. All quiet people are big. If Fiona is nice then Fiona is green. If someone is green then they are nice. Cold people are green. All rough people are cold. If someone is nice then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Rough, smart people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Cold, quiet people are big.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Fiona is nice then Fiona is green.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "green" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Erin is not rough.
False
1
inv-proof
[(triple4)]
("Erin" "is" "rough" "-")
triple4
Harry is cold.
True
2
proof
[(((triple7) -> rule8))]
("Harry" "is" "cold" "+")
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple7) -> rule8))]
("Harry" "is" "cold" "-")
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple5) -> rule7)) -> rule6) OR ((((((triple6) -> rule8)) -> rule7)) -> rule6))]
("Fiona" "is" "nice" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Erin is not green.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("Erin" "is" "green" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
True
4
proof
[(((((((triple4) -> rule8)) -> rule7)) -> rule6))]
("Erin" "is" "nice" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not nice.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule7)) -> rule6))]
("Erin" "is" "nice" "-")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is quiet.
True
5
proof
[(((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9))]
("Erin" "is" "quiet" "+")
((((((((triple4) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Harry is not quiet.
False
5
inv-proof
[(((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9))]
("Harry" "is" "quiet" "-")
((((((((triple7) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Erin is big.
True
6
proof
[(((((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((((triple4) -> rule8) ((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2))]
("Erin" "is" "big" "+")
((((((((((triple4) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
((((triple4) -> (rule8 % int5)) ((((((((triple4) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Harry is not big.
False
6
inv-proof
[(((((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((((triple7) -> rule8) ((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2))]
("Harry" "is" "big" "-")
((((((((((triple7) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((triple7) -> (rule8 % int5)) ((((((((triple7) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule4) OR ((((((triple2) -> rule6)) -> rule9)) -> rule4))] Anne is green.[(triple2)] Anne is quiet.[(triple3 OR ((((triple2) -> rule6)) -> rule9))] Erin is rough.[(triple4)] Fiona is cold.[(triple5 OR ((triple6) -> rule8))] Fiona is rough.[(triple6)] Harry is rough.[(triple7)] @1: Anne is nice.[(((triple2) -> rule6))] Erin is cold.[(((triple4) -> rule8))] Fiona is green.[(((triple5) -> rule7) OR ((((triple6) -> rule8)) -> rule7))] Harry is cold.[(((triple7) -> rule8))] @2: Erin is green.[(((((triple4) -> rule8)) -> rule7))] Fiona is nice.[(((((triple5) -> rule7)) -> rule6) OR ((((((triple6) -> rule8)) -> rule7)) -> rule6))] Harry is green.[(((((triple7) -> rule8)) -> rule7))] @3: Erin is nice.[(((((((triple4) -> rule8)) -> rule7)) -> rule6))] Fiona is quiet.[(((((((triple5) -> rule7)) -> rule6)) -> rule9) OR ((((((((triple6) -> rule8)) -> rule7)) -> rule6)) -> rule9))] Harry is nice.[(((((((triple7) -> rule8)) -> rule7)) -> rule6))] @4: Erin is quiet.[(((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9))] Fiona is big.[(((((((((triple5) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((triple5 ((((((triple5) -> rule7)) -> rule6)) -> rule9)) -> rule2) OR ((((triple6) -> rule8) ((((((triple5) -> rule7)) -> rule6)) -> rule9)) -> rule2) OR ((((((((((triple6) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((triple5 ((((((((triple6) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2) OR ((((triple6) -> rule8) ((((((((triple6) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2))] Harry is quiet.[(((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9))] @5: Erin is big.[(((((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((((triple4) -> rule8) ((((((((triple4) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2))] Harry is big.[(((((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule4) OR ((((triple7) -> rule8) ((((((((triple7) -> rule8)) -> rule7)) -> rule6)) -> rule9)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((((triple2) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((((triple2) -> (rule6 % int2))) -> (rule9 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
((triple6) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((((triple6) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((((triple4) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((triple5 ((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((triple6) -> (rule8 % int5)) ((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((triple5 ((((((((triple6) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((((triple6) -> (rule8 % int5)) ((((((((triple6) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((((((triple4) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
((((triple4) -> (rule8 % int5)) ((((((((triple4) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Harry is big.
("Harry" "is" "big" "+")
((((((((((triple7) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((triple7) -> (rule8 % int5)) ((((((((triple7) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5