Anne is white. Bob is red. Charlie is white. Dave is smart. If someone is red then they are white. White people are cold. If someone is cold then they are smart.
Anne is white.
("Anne" "is" "white" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Dave is not smart.
False
1
inv-proof
[(triple4)]
("Dave" "is" "smart" "-")
triple4
Bob is white.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "white" "+")
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is white.[(triple1)] Bob is red.[(triple2)] Charlie is white.[(triple3)] Dave is smart.[(triple4)] @1: Anne is cold.[(((triple1) -> rule2))] Bob is white.[(((triple2) -> rule1))] Charlie is cold.[(((triple3) -> rule2))] @2: Anne is smart.[(((((triple1) -> rule2)) -> rule3))] Bob is cold.[(((((triple2) -> rule1)) -> rule2))] Charlie is smart.[(((((triple3) -> rule2)) -> rule3))] @3: Bob is smart.[(((((((triple2) -> rule1)) -> rule2)) -> rule3))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3