Bob is smart. Dave is big. Gary is quiet. Cold things are smart. If something is quiet then it is cold. Cold things are rough.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Gary is quiet.
True
1
proof
[(triple3)]
("Gary" "is" "quiet" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Gary is cold.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Bob is smart.[(triple1)] Dave is big.[(triple2)] Gary is quiet.[(triple3)] @1: Gary is cold.[(((triple3) -> rule2))] @2: Gary is rough.[(((((triple3) -> rule2)) -> rule3))] Gary is smart.[(((((triple3) -> rule2)) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2