Bob is smart. Gary is rough. All smart people are not cold. If someone is rough then they are cold. If someone is rough and white then they are not smart. If Bob is cold then Bob is rough. Cold people are white. If Bob is furry then Bob is cold.
Bob is smart.
("Bob" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All smart people are not cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "-"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and white then they are not smart.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "-"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Bob is furry then Bob is cold.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "cold" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple2)]
("Gary" "is" "rough" "-")
triple2
Bob is not cold.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Gary is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("Gary" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Gary" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
("Gary" "is" "smart" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is smart.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
("Gary" "is" "smart" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is smart.[(triple1)] Gary is rough.[(triple2)] @1: Bob is not cold.[(((triple1) -> rule1))] Gary is cold.[(((triple2) -> rule2))] @2: Gary is white.[(((((triple2) -> rule2)) -> rule5))] @3: Gary is not smart.[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
("Gary" "is" "smart" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3