Charlie is big. If someone is big then they are cold. If Charlie is cold and Charlie is young then Charlie is furry. If someone is cold then they are young.
Charlie is big.
("Charlie" "is" "big" "+")
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is young then Charlie is furry.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not furry.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is big.[(triple1)] @1: Charlie is cold.[(((triple1) -> rule1))] @2: Charlie is young.[(((((triple1) -> rule1)) -> rule3))] @3: Charlie is furry.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3