Anne is cold. Anne is green. Anne is kind. Anne is nice. Anne is red. Bob is green. Bob is kind. Bob is quiet. Charlie is cold. Charlie is green. Charlie is red. Charlie is round. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is round. If something is quiet and round then it is nice. All cold things are quiet. Nice things are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If something is quiet and round then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Anne is green.
True
1
proof
[(triple2)]
("Anne" "is" "green" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple16)]
("Fiona" "is" "round" "-")
triple16
Charlie is quiet.
True
2
proof
[(((triple9) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple9) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple9) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple9) -> rule2) triple12) -> rule1))]
("Charlie" "is" "nice" "+")
((((triple9) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple9) -> rule2) triple12) -> rule1))]
("Charlie" "is" "nice" "-")
((((triple9) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
True
5
proof
[(((((((triple9) -> rule2) triple12) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "+")
((((((triple9) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((((((triple9) -> rule2) triple12) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "-")
((((((triple9) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple4) -> rule3))] Anne is nice.[(triple4)] Anne is red.[(triple5)] Bob is green.[(triple6)] Bob is kind.[(triple7)] Bob is quiet.[(triple8)] Charlie is cold.[(triple9)] Charlie is green.[(triple10)] Charlie is red.[(triple11)] Charlie is round.[(triple12)] Fiona is cold.[(triple13)] Fiona is kind.[(triple14 OR ((triple15) -> rule3) OR ((((((triple13) -> rule2) triple16) -> rule1)) -> rule3))] Fiona is nice.[(triple15 OR ((((triple13) -> rule2) triple16) -> rule1))] Fiona is round.[(triple16)] @1: Anne is quiet.[(((triple1) -> rule2))] Charlie is quiet.[(((triple9) -> rule2))] Fiona is quiet.[(((triple13) -> rule2))] @2: Charlie is nice.[(((((triple9) -> rule2) triple12) -> rule1))] @3: Charlie is kind.[(((((((triple9) -> rule2) triple12) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple4) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Fiona is cold.
("Fiona" "is" "cold" "+")
triple13
Fiona is kind.
("Fiona" "is" "kind" "+")
triple14
((triple15) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((((triple13) -> (rule2 % int3)) triple16) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple15
((((triple13) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple16
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple13) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple9) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple9) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3