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