Bob is big. Bob is smart. Bob is young. Dave is furry. Dave is young. Harry is not big. Harry is furry. If Dave is furry then Dave is smart. If Bob is furry and Bob is not big then Bob is not quiet. Furry people are young. If someone is young and furry then they are rough. If someone is smart and not furry then they are not nice. If someone is furry and not young then they are not smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is furry.
("Harry" "is" "furry" "+")
If Dave is furry then Dave is smart.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "smart" "+"))
If Bob is furry and Bob is not big then Bob is not quiet.
((("Bob" "is" "furry" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "quiet" "-"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is young and furry then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and not furry then they are not nice.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "-"))
If someone is furry and not young then they are not smart.
((("someone" "is" "furry" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "smart" "-"))
Harry is furry.
True
1
proof
[(triple7)]
("Harry" "is" "furry" "+")
triple7
Dave is not furry.
False
1
inv-proof
[(triple4)]
("Dave" "is" "furry" "-")
triple4
Dave is rough.
True
3
proof
[(((triple5 triple4) -> rule4) OR ((((triple4) -> rule3) triple4) -> rule4))]
("Dave" "is" "rough" "+")
((triple5 triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Harry is not young.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "young" "-")
((triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
True
4
proof
[(((((triple7) -> rule3) triple7) -> rule4))]
("Harry" "is" "rough" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((((triple7) -> rule3) triple7) -> rule4))]
("Harry" "is" "rough" "-")
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is smart.[(triple2)] Bob is young.[(triple3)] Dave is furry.[(triple4)] Dave is young.[(triple5 OR ((triple4) -> rule3))] Harry is furry.[(triple7)] Harry is not big.[(triple6)] @1: Dave is rough.[(((triple5 triple4) -> rule4) OR ((((triple4) -> rule3) triple4) -> rule4))] Dave is smart.[(((triple4) -> rule1))] Harry is young.[(((triple7) -> rule3))] @2: Harry is rough.[(((((triple7) -> rule3) triple7) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
((triple5 triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2