Anne is blue. Anne is cold. Anne is kind. Anne is round. Anne is white. Fiona is kind. Fiona is rough. Fiona is round. Fiona is white. Gary is cold. Gary is kind. Gary is rough. Gary is round. Gary is white. Harry is cold. Harry is round. If Gary is smart and Gary is rough then Gary is round. All cold people are kind. White, round people are cold. All blue people are smart. All cold, white people are blue. All round people are cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is smart and Gary is rough then Gary is round.
((("Gary" "is" "smart" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "round" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
White, round people are cold.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All cold, white people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Anne is cold.
True
1
proof
[(triple2 OR ((triple4) -> rule6) OR ((triple5 triple4) -> rule3))]
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is not white.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "white" "-")
triple9
Fiona is cold.
True
2
proof
[(((triple8) -> rule6) OR ((triple9 triple8) -> rule3))]
("Fiona" "is" "cold" "+")
((triple8) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple9 triple8) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple15) -> rule2) OR ((((triple16) -> rule6)) -> rule2))]
("Harry" "is" "kind" "-")
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple16) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is blue.
True
4
proof
[(((((triple8) -> rule6) triple9) -> rule5) OR ((((triple9 triple8) -> rule3) triple9) -> rule5))]
("Fiona" "is" "blue" "+")
((((triple8) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9 triple8) -> (rule3 % int2)) triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((((triple10 triple14) -> rule5)) -> rule4) OR ((((((triple13) -> rule6) triple14) -> rule5)) -> rule4) OR ((((((triple14 triple13) -> rule3) triple14) -> rule5)) -> rule4))]
("Gary" "is" "smart" "-")
((((triple10 triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple13) -> (rule6 % int3)) triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple14 triple13) -> (rule3 % int3)) triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is smart.
True
5
proof
[(((((((triple8) -> rule6) triple9) -> rule5)) -> rule4) OR ((((((triple9 triple8) -> rule3) triple9) -> rule5)) -> rule4))]
("Fiona" "is" "smart" "+")
((((((triple8) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((triple9 triple8) -> (rule3 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not smart.
False
5
inv-proof
[(((((((triple8) -> rule6) triple9) -> rule5)) -> rule4) OR ((((((triple9 triple8) -> rule3) triple9) -> rule5)) -> rule4))]
("Fiona" "is" "smart" "-")
((((((triple8) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((triple9 triple8) -> (rule3 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is smart.
Unknown
rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is blue.[(triple1 OR ((triple2 triple5) -> rule5) OR ((((triple4) -> rule6) triple5) -> rule5) OR ((((triple5 triple4) -> rule3) triple5) -> rule5))] Anne is cold.[(triple2 OR ((triple4) -> rule6) OR ((triple5 triple4) -> rule3))] Anne is kind.[(triple3 OR ((triple2) -> rule2) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple5 triple4) -> rule3)) -> rule2))] Anne is round.[(triple4)] Anne is white.[(triple5)] Fiona is kind.[(triple6 OR ((((triple8) -> rule6)) -> rule2) OR ((((triple9 triple8) -> rule3)) -> rule2))] Fiona is rough.[(triple7)] Fiona is round.[(triple8)] Fiona is white.[(triple9)] Gary is cold.[(triple10 OR ((triple13) -> rule6) OR ((triple14 triple13) -> rule3))] Gary is kind.[(triple11 OR ((triple10) -> rule2) OR ((((triple13) -> rule6)) -> rule2) OR ((((triple14 triple13) -> rule3)) -> rule2))] Gary is rough.[(triple12)] Gary is round.[(triple13 OR ((((((triple10 triple14) -> rule5)) -> rule4) triple12) -> rule1))] Gary is white.[(triple14)] Harry is cold.[(triple15 OR ((triple16) -> rule6))] Harry is round.[(triple16)] @1: Anne is smart.[(((triple1) -> rule4) OR ((((triple2 triple5) -> rule5)) -> rule4) OR ((((((triple4) -> rule6) triple5) -> rule5)) -> rule4) OR ((((((triple5 triple4) -> rule3) triple5) -> rule5)) -> rule4))] Fiona is cold.[(((triple8) -> rule6) OR ((triple9 triple8) -> rule3))] Gary is blue.[(((triple10 triple14) -> rule5) OR ((((triple13) -> rule6) triple14) -> rule5) OR ((((triple14 triple13) -> rule3) triple14) -> rule5))] Harry is kind.[(((triple15) -> rule2) OR ((((triple16) -> rule6)) -> rule2))] @2: Fiona is blue.[(((((triple8) -> rule6) triple9) -> rule5) OR ((((triple9 triple8) -> rule3) triple9) -> rule5))] Gary is smart.[(((((triple10 triple14) -> rule5)) -> rule4) OR ((((((triple13) -> rule6) triple14) -> rule5)) -> rule4) OR ((((((triple14 triple13) -> rule3) triple14) -> rule5)) -> rule4))] @3: Fiona is smart.[(((((((triple8) -> rule6) triple9) -> rule5)) -> rule4) OR ((((((triple9 triple8) -> rule3) triple9) -> rule5)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2 triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5 triple4) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9 triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((triple13) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple14 triple13) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((triple10) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple14 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is round.
("Gary" "is" "round" "+")
triple13
((((((triple10 triple14) -> (rule5 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple14
Harry is cold.
("Harry" "is" "cold" "+")
triple15
((triple16) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple16
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple4) -> (rule6 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple5 triple4) -> (rule3 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple9 triple8) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple10 triple14) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple13) -> (rule6 % int2)) triple14) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple14 triple13) -> (rule3 % int2)) triple14) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple16) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple8) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9 triple8) -> (rule3 % int2)) triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple10 triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple13) -> (rule6 % int3)) triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple14 triple13) -> (rule3 % int3)) triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple8) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((triple9 triple8) -> (rule3 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3