Bob is big. Bob is blue. Bob is furry. Bob is green. Bob is kind. Bob is rough. Erin is blue. Erin is furry. Erin is green. Erin is quiet. Erin is rough. Harry is big. Harry is blue. Harry is furry. Harry is kind. Harry is quiet. If Harry is kind and Harry is furry then Harry is quiet. All big, green things are quiet. All blue, kind things are quiet. If something is green then it is kind. All rough, kind things are big. If Harry is big and Harry is furry then Harry is blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is kind and Harry is furry then Harry is quiet.
((("Harry" "is" "kind" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "quiet" "+"))
All big, green things are quiet.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All blue, kind things are quiet.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All rough, kind things are big.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If Harry is big and Harry is furry then Harry is blue.
((("Harry" "is" "big" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "blue" "+"))
Bob is big.
True
1
proof
[(triple1 OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple4) -> rule4)) -> rule5))]
("Bob" "is" "big" "+")
triple1
((triple6 triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is not green.
False
1
inv-proof
[(triple9)]
("Erin" "is" "green" "-")
triple9
Bob is quiet.
True
3
proof
[(((triple1 triple4) -> rule2) OR ((triple2 triple5) -> rule3) OR ((triple2 ((triple4) -> rule4)) -> rule3) OR ((((triple6 triple5) -> rule5) triple4) -> rule2) OR ((((triple6 ((triple4) -> rule4)) -> rule5) triple4) -> rule2))]
("Bob" "is" "quiet" "+")
((triple1 triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple6 triple5) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple6 ((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is not kind.
False
2
inv-proof
[(((triple9) -> rule4))]
("Erin" "is" "kind" "-")
((triple9) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is big.[(triple1 OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple4) -> rule4)) -> rule5))] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5 OR ((triple4) -> rule4))] Bob is rough.[(triple6)] Erin is blue.[(triple7)] Erin is furry.[(triple8)] Erin is green.[(triple9)] Erin is quiet.[(triple10 OR ((triple7 ((triple9) -> rule4)) -> rule3) OR ((((triple11 ((triple9) -> rule4)) -> rule5) triple9) -> rule2))] Erin is rough.[(triple11)] Harry is big.[(triple12)] Harry is blue.[(triple13 OR ((triple12 triple14) -> rule6))] Harry is furry.[(triple14)] Harry is kind.[(triple15)] Harry is quiet.[(triple16 OR ((triple13 triple15) -> rule3) OR ((triple15 triple14) -> rule1) OR ((((triple12 triple14) -> rule6) triple15) -> rule3))] @1: Bob is quiet.[(((triple1 triple4) -> rule2) OR ((triple2 triple5) -> rule3) OR ((triple2 ((triple4) -> rule4)) -> rule3) OR ((((triple6 triple5) -> rule5) triple4) -> rule2) OR ((((triple6 ((triple4) -> rule4)) -> rule5) triple4) -> rule2))] Erin is kind.[(((triple9) -> rule4))] @2: Erin is big.[(((triple11 ((triple9) -> rule4)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple6 triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
((triple7 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple11 ((triple9) -> (rule4 % int3))) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
((triple12 triple14) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple16
((triple13 triple15) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple15 triple14) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple12 triple14) -> (rule6 % int2)) triple15) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1 triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple6 triple5) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple6 ((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple9) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple11 ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2