Bob is cold. Harry is not big. Harry is not cold. Harry is rough. Harry is smart. Harry is white. Harry is young. All big, smart people are not white. All cold people are smart. All smart people are furry. All white, rough people are furry. If Harry is young and Harry is cold then Harry is not furry. If Harry is rough and Harry is big then Harry is furry. If someone is cold and not young then they are not big. All cold, furry people are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All big, smart people are not white.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All white, rough people are furry.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Harry is young and Harry is cold then Harry is not furry.
((("Harry" "is" "young" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "-"))
If Harry is rough and Harry is big then Harry is furry.
((("Harry" "is" "rough" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "furry" "+"))
If someone is cold and not young then they are not big.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "big" "-"))
All cold, furry people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Harry is not cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "-")
triple3
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple5) -> rule3) OR ((triple6 triple4) -> rule4))]
("Harry" "is" "furry" "-")
((triple5) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule8))]
("Bob" "is" "rough" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule8))]
("Bob" "is" "rough" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is cold.[(triple1)] Harry is not big.[(triple2)] Harry is not cold.[(triple3)] Harry is rough.[(triple4)] Harry is smart.[(triple5)] Harry is white.[(triple6)] Harry is young.[(triple7)] @1: Bob is smart.[(((triple1) -> rule2))] Harry is furry.[(((triple5) -> rule3) OR ((triple6 triple4) -> rule4))] @2: Bob is furry.[(((((triple1) -> rule2)) -> rule3))] @3: Bob is rough.[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule8))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Harry is not big.
("Harry" "is" "big" "-")
triple2
Harry is not cold.
("Harry" "is" "cold" "-")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Harry is smart.
("Harry" "is" "smart" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3