Bob is not big. Bob is blue. Bob is young. Dave is not blue. Dave is cold. Dave is red. Dave is smart. If something is smart and not big then it is young. If something is young then it is round. If something is round and not blue then it is not smart.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is smart and not big then it is young.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "young" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is round and not blue then it is not smart.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "-"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Bob is not young.
False
1
inv-proof
[(triple3)]
("Bob" "is" "young" "-")
triple3
Bob is round.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "+")
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "round" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is blue.[(triple2)] Bob is not big.[(triple1)] Bob is young.[(triple3)] Dave is cold.[(triple5)] Dave is not blue.[(triple4)] Dave is red.[(triple6)] Dave is smart.[(triple7)] @1: Bob is round.[(((triple3) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1