Bob is red. Dave is smart. If someone is smart and round then they are not kind. Smart people are round. If someone is round and not cold then they are not red.
Bob is red.
("Bob" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is smart and round then they are not kind.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "-"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not cold then they are not red.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "-"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Dave is round.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "round" "+")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "round" "-")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not kind.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is red.[(triple1)] Dave is smart.[(triple2)] @1: Dave is round.[(((triple2) -> rule2))] @2: Dave is not kind.[(((triple2 ((triple2) -> rule2)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2