Anne is big. Anne is blue. Bob is big. Bob is not kind. Bob is round. Harry is big. Harry is blue. Harry is cold. Harry is kind. Harry is not young. If something is young and not blue then it is cold. All round things are not cold. All quiet things are cold. All kind, big things are quiet. If something is big and young then it is kind. All blue things are kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is round.
("Bob" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is young and not blue then it is cold.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
All round things are not cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All kind, big things are quiet.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is big and young then it is kind.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple9 OR ((triple7) -> rule6))]
("Harry" "is" "kind" "+")
triple9
((triple7) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
False
1
inv-proof
[(triple10)]
("Harry" "is" "young" "+")
triple10
Bob is not cold.
True
2
proof
[(((triple5) -> rule2))]
("Bob" "is" "cold" "-")
((triple5) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Harry is not quiet.
False
3
inv-proof
[(((triple9 triple6) -> rule4) OR ((((triple7) -> rule6) triple6) -> rule4))]
("Harry" "is" "quiet" "-")
((triple9 triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is quiet.
True
4
proof
[(((((triple2) -> rule6) triple1) -> rule4))]
("Anne" "is" "quiet" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not quiet.
False
4
inv-proof
[(((((triple2) -> rule6) triple1) -> rule4))]
("Anne" "is" "quiet" "-")
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
True
5
proof
[(((((((triple2) -> rule6) triple1) -> rule4)) -> rule3))]
("Anne" "is" "cold" "+")
((((((triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((((((triple2) -> rule6) triple1) -> rule4)) -> rule3))]
("Anne" "is" "cold" "-")
((((((triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Bob is big.[(triple3)] Bob is not kind.[(triple4)] Bob is round.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7)] Harry is cold.[(triple8 OR ((((triple9 triple6) -> rule4)) -> rule3) OR ((((((triple7) -> rule6) triple6) -> rule4)) -> rule3))] Harry is kind.[(triple9 OR ((triple7) -> rule6))] Harry is not young.[(triple10)] @1: Anne is kind.[(((triple2) -> rule6))] Bob is not cold.[(((triple5) -> rule2))] Harry is quiet.[(((triple9 triple6) -> rule4) OR ((((triple7) -> rule6) triple6) -> rule4))] @2: Anne is quiet.[(((((triple2) -> rule6) triple1) -> rule4))] @3: Anne is cold.[(((((((triple2) -> rule6) triple1) -> rule4)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is not kind.
("Bob" "is" "kind" "-")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((((triple9 triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple7) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple7) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
triple10
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
((triple5) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9 triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3