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