Bob is cold. Charlie is cold. Charlie is kind. All cold things are kind. All white, quiet things are blue. If Bob is nice and Bob is cold then Bob is white. Blue things are furry. If something is cold and white then it is kind. Furry, kind things are blue. All kind things are white. If Charlie is quiet then Charlie is white.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All white, quiet things are blue.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Bob is nice and Bob is cold then Bob is white.
((("Bob" "is" "nice" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "white" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is cold and white then it is kind.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Furry, kind things are blue.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Charlie is quiet then Charlie is white.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "white" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Bob is kind.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple3) -> rule7) OR ((((triple2) -> rule1)) -> rule7))]
("Charlie" "is" "white" "-")
((triple3) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("Bob" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Bob is blue.
Unknown
rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Charlie is cold.[(triple2)] Charlie is kind.[(triple3 OR ((triple2) -> rule1))] @1: Bob is kind.[(((triple1) -> rule1))] Charlie is white.[(((triple3) -> rule7) OR ((((triple2) -> rule1)) -> rule7))] @2: Bob is white.[(((((triple1) -> rule1)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2