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