Bob is big. Bob is green. Bob is kind. Bob is white. Bob is young. Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is young. Big, kind things are young. If Dave is young then Dave is rough. If Bob is kind then Bob is furry. Young things are furry. Young things are kind. All green things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Big, kind things are young.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Dave is young then Dave is rough.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "rough" "+"))
If Bob is kind then Bob is furry.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "furry" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple10 OR ((triple8) -> rule6) OR ((triple6 triple9) -> rule1))]
("Dave" "is" "young" "+")
triple10
((triple8) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 triple9) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule6) OR ((triple6 triple9) -> rule1))]
("Dave" "is" "young" "-")
triple10
((triple8) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 triple9) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple5) -> rule5) OR ((((triple2) -> rule6)) -> rule5))] Bob is white.[(triple4)] Bob is young.[(triple5 OR ((triple2) -> rule6) OR ((triple1 triple3) -> rule1))] Dave is big.[(triple6)] Dave is furry.[(triple7 OR ((triple10) -> rule4) OR ((((triple8) -> rule6)) -> rule4) OR ((((triple6 triple9) -> rule1)) -> rule4))] Dave is green.[(triple8)] Dave is kind.[(triple9 OR ((triple10) -> rule5) OR ((((triple8) -> rule6)) -> rule5))] Dave is young.[(triple10 OR ((triple8) -> rule6) OR ((triple6 triple9) -> rule1))] @1: Bob is furry.[(((triple3) -> rule3) OR ((triple5) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((triple5) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule1)) -> rule4) OR ((((((triple2) -> rule6)) -> rule5)) -> rule3))] Dave is rough.[(((triple10) -> rule2) OR ((((triple8) -> rule6)) -> rule2) OR ((((triple6 triple9) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple1 triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple10) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple6 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
((triple10) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple8) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 triple9) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple10) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple6 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2