Bob is blue. Bob is rough. Bob is smart. Dave is not big. Dave is kind. Dave is round. Dave is young. Gary is big. Gary is kind. Gary is not rough. Gary is not smart. Gary is young. All round things are smart. If something is round and not big then it is smart. If something is blue then it is not kind. If Bob is rough then Bob is young. If something is smart then it is rough. If Gary is smart then Gary is blue. If Gary is not young then Gary is rough. If Gary is round and Gary is not smart then Gary is kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is young.
("Gary" "is" "young" "+")
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is round and not big then it is smart.
((("something" "is" "round" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
If something is blue then it is not kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If Bob is rough then Bob is young.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "young" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Gary is smart then Gary is blue.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "blue" "+"))
If Gary is not young then Gary is rough.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "rough" "+"))
If Gary is round and Gary is not smart then Gary is kind.
((("Gary" "is" "round" "+") ("Gary" "is" "smart" "~")) -> ("Gary" "is" "kind" "+"))
Dave is not big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "-")
triple4
Dave is big.
False
1
inv-proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Bob is not kind.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Dave is rough.
True
3
proof
[(((((triple6) -> rule1)) -> rule5) OR ((((triple6 triple4) -> rule2)) -> rule5))]
("Dave" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple6 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule5) OR ((((triple6 triple4) -> rule2)) -> rule5))]
("Dave" "is" "rough" "-")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple6 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2 OR ((triple3) -> rule5))] Bob is smart.[(triple3)] Dave is kind.[(triple5)] Dave is not big.[(triple4)] Dave is round.[(triple6)] Dave is young.[(triple7)] Gary is big.[(triple8)] Gary is kind.[(triple9)] Gary is not rough.[(triple10)] Gary is not smart.[(triple11)] Gary is young.[(triple12)] @1: Bob is not kind.[(((triple1) -> rule3))] Bob is young.[(((triple2) -> rule4) OR ((((triple3) -> rule5)) -> rule4))] Dave is smart.[(((triple6) -> rule1) OR ((triple6 triple4) -> rule2))] @2: Dave is rough.[(((((triple6) -> rule1)) -> rule5) OR ((((triple6 triple4) -> rule2)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not big.
("Dave" "is" "big" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is not rough.
("Gary" "is" "rough" "-")
triple10
Gary is not smart.
("Gary" "is" "smart" "-")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Bob is not kind.
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple6 triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple6 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2