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