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