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