Anne is cold. Erin is green. Erin is not nice. Fiona is cold. Fiona is green. Harry is cold. Harry is green. If something is nice and rough then it is kind. All rough, round things are kind. All round things are nice. Cold things are round. All nice, red things are rough. If Erin is kind and Erin is red then Erin is green. Nice, cold things are red. If Anne is green then Anne is not cold.
Anne is cold.
("Anne" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is nice and rough then it is kind.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All rough, round things are kind.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All nice, red things are rough.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Erin is kind and Erin is red then Erin is green.
((("Erin" "is" "kind" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "green" "+"))
Nice, cold things are red.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Anne is green then Anne is not cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "-"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "round" "-")
((triple4) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
True
5
proof
[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule7))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Fiona is not red.
False
5
inv-proof
[(((((((triple4) -> rule4)) -> rule3) triple4) -> rule7))]
("Fiona" "is" "red" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Anne is rough.
True
9
proof
[(((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5))]
("Anne" "is" "rough" "+")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Harry is not rough.
False
9
inv-proof
[(((((((triple6) -> rule4)) -> rule3) ((((((triple6) -> rule4)) -> rule3) triple6) -> rule7)) -> rule5))]
("Harry" "is" "rough" "-")
((((((triple6) -> (rule4 % int4))) -> (rule3 % int3)) ((((((triple6) -> (rule4 % int4))) -> (rule3 % int3)) triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Anne is kind.
True
12
proof
[(((((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5) ((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5)) -> rule1))]
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int5))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not kind.
False
12
inv-proof
[(((((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5) ((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5)) -> rule1))]
("Anne" "is" "kind" "-")
((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int5))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is cold.[(triple1)] Erin is green.[(triple2)] Erin is not nice.[(triple3)] Fiona is cold.[(triple4)] Fiona is green.[(triple5)] Harry is cold.[(triple6)] Harry is green.[(triple7)] @1: Anne is round.[(((triple1) -> rule4))] Fiona is round.[(((triple4) -> rule4))] Harry is round.[(((triple6) -> rule4))] @2: Anne is nice.[(((((triple1) -> rule4)) -> rule3))] Fiona is nice.[(((((triple4) -> rule4)) -> rule3))] Harry is nice.[(((((triple6) -> rule4)) -> rule3))] @3: Anne is red.[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule7))] Fiona is red.[(((((((triple4) -> rule4)) -> rule3) triple4) -> rule7))] Harry is red.[(((((((triple6) -> rule4)) -> rule3) triple6) -> rule7))] @4: Anne is rough.[(((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5))] Fiona is rough.[(((((((triple4) -> rule4)) -> rule3) ((((((triple4) -> rule4)) -> rule3) triple4) -> rule7)) -> rule5))] Harry is rough.[(((((((triple6) -> rule4)) -> rule3) ((((((triple6) -> rule4)) -> rule3) triple6) -> rule7)) -> rule5))] @5: Anne is kind.[(((((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5) ((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) ((((((triple1) -> rule4)) -> rule3) triple1) -> rule7)) -> rule5)) -> rule1))] Fiona is kind.[(((((((((triple4) -> rule4)) -> rule3) ((((((triple4) -> rule4)) -> rule3) triple4) -> rule7)) -> rule5) ((triple4) -> rule4)) -> rule2) OR ((((((triple4) -> rule4)) -> rule3) ((((((triple4) -> rule4)) -> rule3) ((((((triple4) -> rule4)) -> rule3) triple4) -> rule7)) -> rule5)) -> rule1))] Harry is kind.[(((((((((triple6) -> rule4)) -> rule3) ((((((triple6) -> rule4)) -> rule3) triple6) -> rule7)) -> rule5) ((triple6) -> rule4)) -> rule2) OR ((((((triple6) -> rule4)) -> rule3) ((((((triple6) -> rule4)) -> rule3) ((((((triple6) -> rule4)) -> rule3) triple6) -> rule7)) -> rule5)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is not nice.
("Erin" "is" "nice" "-")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple4) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple6) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) ((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple6) -> (rule4 % int4))) -> (rule3 % int3)) ((((((triple6) -> (rule4 % int4))) -> (rule3 % int3)) triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int5))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((((triple4) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple4) -> (rule4 % int5))) -> (rule3 % int4)) triple4) -> (rule7 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int5))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
((((((triple4) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple4) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple4) -> (rule4 % int5))) -> (rule3 % int4)) triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Harry is kind.
("Harry" "is" "kind" "+")
((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3))) -> (rule5 % int2)) ((triple6) -> (rule4 % int5))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5
((((((triple6) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5