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