Anne is furry. Harry is furry. All furry things are cold. All furry, big things are green. If something is cold then it is big.
Anne is furry.
("Anne" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All furry, big things are green.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Harry is furry.
True
1
proof
[(triple2)]
("Harry" "is" "furry" "+")
triple2
Harry is not furry.
False
1
inv-proof
[(triple2)]
("Harry" "is" "furry" "-")
triple2
Harry is cold.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
True
5
proof
[(((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "green" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Anne is not green.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Anne" "is" "green" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is furry.[(triple1)] Harry is furry.[(triple2)] @1: Anne is cold.[(((triple1) -> rule1))] Harry is cold.[(((triple2) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule3))] Harry is big.[(((((triple2) -> rule1)) -> rule3))] @3: Anne is green.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))] Harry is green.[(((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3