Bob is furry. Bob is green. Bob is nice. Bob is young. Dave is big. Dave is furry. Dave is round. Dave is smart. Dave is young. Harry is big. Harry is not furry. Harry is green. Harry is nice. Harry is smart. Harry is not young. All big, green people are smart. If Harry is smart then Harry is round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not young.
("Harry" "is" "young" "-")
All big, green people are smart.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart then Harry is round.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "+"))
Dave is big.
True
1
proof
[(triple5)]
("Dave" "is" "big" "+")
triple5
Dave is not young.
False
1
inv-proof
[(triple9)]
("Dave" "is" "young" "-")
triple9
Harry is round.
True
2
proof
[(((triple14) -> rule2) OR ((((triple10 triple12) -> rule1)) -> rule2))]
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not round.
False
2
inv-proof
[(((triple14) -> rule2) OR ((((triple10 triple12) -> rule1)) -> rule2))]
("Harry" "is" "round" "-")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is young.[(triple4)] Dave is big.[(triple5)] Dave is furry.[(triple6)] Dave is round.[(triple7)] Dave is smart.[(triple8)] Dave is young.[(triple9)] Harry is big.[(triple10)] Harry is green.[(triple12)] Harry is nice.[(triple13)] Harry is not furry.[(triple11)] Harry is not young.[(triple15)] Harry is smart.[(triple14 OR ((triple10 triple12) -> rule1))] @1: Harry is round.[(((triple14) -> rule2) OR ((((triple10 triple12) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is not furry.
("Harry" "is" "furry" "-")
triple11
Harry is not young.
("Harry" "is" "young" "-")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple10 triple12) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2