Anne is nice. Charlie is cold. Charlie is round. Erin is blue. Erin is kind. Erin is not young. Harry is cold. If someone is cold and young then they are round. If someone is young and cold then they are round. Cold people are nice. All rough, young people are kind. Round people are rough. Nice, cold people are young.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not young.
("Erin" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is cold and young then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is young and cold then they are round.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All rough, young people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Nice, cold people are young.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Charlie is round.
True
1
proof
[(triple3 OR ((triple2 ((((triple2) -> rule3) triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule3) triple2) -> rule6) triple2) -> rule2))]
("Charlie" "is" "round" "+")
triple3
((triple2 ((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is young.
False
1
inv-proof
[(triple6)]
("Erin" "is" "young" "+")
triple6
Charlie is nice.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "nice" "-")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is young.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule6))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Harry is not young.
False
4
inv-proof
[(((((triple7) -> rule3) triple7) -> rule6))]
("Harry" "is" "young" "-")
((((triple7) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is kind.
True
7
proof
[(((((triple3) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4) OR ((((((triple2 ((((triple2) -> rule3) triple2) -> rule6)) -> rule1)) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4) OR ((((((((((triple2) -> rule3) triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4))]
("Charlie" "is" "kind" "+")
((((triple3) -> (rule5 % int4)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((((((triple2 ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Harry is not round.
False
6
inv-proof
[(((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1) OR ((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2))]
("Harry" "is" "round" "-")
((triple7 ((((triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
True
7
proof
[(((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5))]
("Harry" "is" "rough" "+")
((((triple7 ((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is not rough.
False
7
inv-proof
[(((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5))]
("Harry" "is" "rough" "-")
((((triple7 ((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is kind.
True
12
proof
[(((((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4) OR ((((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4))]
("Harry" "is" "kind" "+")
((((((triple7 ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
((((((((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4)) triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Harry is not kind.
False
12
inv-proof
[(((((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4) OR ((((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4))]
("Harry" "is" "kind" "-")
((((((triple7 ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
((((((((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4)) triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not rough.
Unknown
inv-rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Charlie is cold.[(triple2)] Charlie is round.[(triple3 OR ((triple2 ((((triple2) -> rule3) triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule3) triple2) -> rule6) triple2) -> rule2))] Erin is blue.[(triple4)] Erin is kind.[(triple5)] Erin is not young.[(triple6)] Harry is cold.[(triple7)] @1: Charlie is nice.[(((triple2) -> rule3))] Charlie is rough.[(((triple3) -> rule5) OR ((((triple2 ((((triple2) -> rule3) triple2) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple2) -> rule3) triple2) -> rule6) triple2) -> rule2)) -> rule5))] Harry is nice.[(((triple7) -> rule3))] @2: Charlie is young.[(((((triple2) -> rule3) triple2) -> rule6))] Harry is young.[(((((triple7) -> rule3) triple7) -> rule6))] @3: Charlie is kind.[(((((triple3) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4) OR ((((((triple2 ((((triple2) -> rule3) triple2) -> rule6)) -> rule1)) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4) OR ((((((((((triple2) -> rule3) triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule3) triple2) -> rule6)) -> rule4))] Harry is round.[(((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1) OR ((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2))] @4: Harry is rough.[(((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5))] @5: Harry is kind.[(((((((triple7 ((((triple7) -> rule3) triple7) -> rule6)) -> rule1)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4) OR ((((((((((triple7) -> rule3) triple7) -> rule6) triple7) -> rule2)) -> rule5) ((((triple7) -> rule3) triple7) -> rule6)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
((triple2 ((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is not young.
("Erin" "is" "young" "-")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2 ((((triple2) -> (rule3 % int4)) triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple3) -> (rule5 % int4)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((((((triple2 ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule3 % int5)) triple2) -> (rule6 % int4))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Harry is round.
("Harry" "is" "round" "+")
((triple7 ((((triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7 ((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple7) -> (rule3 % int4)) triple7) -> (rule6 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple7 ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
((((((((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4)) triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule3 % int5)) triple7) -> (rule6 % int4))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5