Dave is big. Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is young. Erin is big. Erin is blue. Erin is furry. Erin is green. Erin is kind. Erin is young. Blue, young people are green. All big, young people are furry.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
Blue, young people are green.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All big, young people are furry.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple10 OR ((triple8 triple12) -> rule1))]
("Erin" "is" "green" "-")
triple10
((triple8 triple12) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3 OR ((triple1 triple6) -> rule2))] Dave is green.[(triple4 OR ((triple2 triple6) -> rule1))] Dave is kind.[(triple5)] Dave is young.[(triple6)] Erin is big.[(triple7)] Erin is blue.[(triple8)] Erin is furry.[(triple9 OR ((triple7 triple12) -> rule2))] Erin is green.[(triple10 OR ((triple8 triple12) -> rule1))] Erin is kind.[(triple11)] Erin is young.[(triple12)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple1 triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple2 triple6) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple7 triple12) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple10
((triple8 triple12) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12