Anne is blue. Anne is kind. Anne is rough. Anne is white. Anne is young. Bob is rough. Fiona is cold. Fiona is kind. Fiona is round. Fiona is white. Fiona is young. Harry is cold. Harry is rough. Harry is round. Harry is young. All round things are rough. If something is blue then it is round. Rough things are kind. All young, cold things are blue. All white, blue things are cold. If something is white then it is young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All young, cold things are blue.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All white, blue things are cold.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Anne is kind.
True
1
proof
[(triple2 OR ((triple3) -> rule3) OR ((((((triple1) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "kind" "+")
triple2
((triple3) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Fiona is not kind.
False
1
inv-proof
[(triple8 OR ((((triple9) -> rule1)) -> rule3) OR ((((((((triple11 triple7) -> rule4)) -> rule2)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule6) triple7) -> rule4)) -> rule2)) -> rule1)) -> rule3))]
("Fiona" "is" "kind" "-")
triple8
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((((triple11 triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((((((triple10) -> (rule6 % int5)) triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2 OR ((triple3) -> rule3) OR ((((((triple1) -> rule2)) -> rule1)) -> rule3))] Anne is rough.[(triple3 OR ((((triple1) -> rule2)) -> rule1))] Anne is white.[(triple4)] Anne is young.[(triple5 OR ((triple4) -> rule6))] Bob is rough.[(triple6)] Fiona is cold.[(triple7)] Fiona is kind.[(triple8 OR ((((triple9) -> rule1)) -> rule3) OR ((((((((triple11 triple7) -> rule4)) -> rule2)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule6) triple7) -> rule4)) -> rule2)) -> rule1)) -> rule3))] Fiona is round.[(triple9 OR ((((triple11 triple7) -> rule4)) -> rule2) OR ((((((triple10) -> rule6) triple7) -> rule4)) -> rule2))] Fiona is white.[(triple10)] Fiona is young.[(triple11 OR ((triple10) -> rule6))] Harry is cold.[(triple12)] Harry is rough.[(triple13 OR ((triple14) -> rule1) OR ((((((triple15 triple12) -> rule4)) -> rule2)) -> rule1))] Harry is round.[(triple14 OR ((((triple15 triple12) -> rule4)) -> rule2))] Harry is young.[(triple15)] @1: Anne is cold.[(((triple4 triple1) -> rule5))] Anne is round.[(((triple1) -> rule2))] Bob is kind.[(((triple6) -> rule3))] Fiona is blue.[(((triple11 triple7) -> rule4) OR ((((triple10) -> rule6) triple7) -> rule4))] Fiona is rough.[(((triple9) -> rule1) OR ((((((triple11 triple7) -> rule4)) -> rule2)) -> rule1) OR ((((((((triple10) -> rule6) triple7) -> rule4)) -> rule2)) -> rule1))] Harry is blue.[(((triple15 triple12) -> rule4))] Harry is kind.[(((triple13) -> rule3) OR ((((triple14) -> rule1)) -> rule3) OR ((((((((triple15 triple12) -> rule4)) -> rule2)) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple3) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((((triple11 triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((((((triple10) -> (rule6 % int5)) triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Fiona is round.
("Fiona" "is" "round" "+")
triple9
((((triple11 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((((triple10) -> (rule6 % int3)) triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple10) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
((triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple15 triple12) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple14
((((triple15 triple12) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple15
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple1) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple6) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple11 triple7) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2)) triple7) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple11 triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((((triple10) -> (rule6 % int4)) triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
((triple15 triple12) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple13) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((((triple15 triple12) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4