Charlie is green. If someone is quiet then they are green. Green people are big. Big, green people are quiet. If Charlie is quiet then Charlie is cold. If Charlie is big and Charlie is green then Charlie is red. All big people are green.
Charlie is green.
("Charlie" "is" "green" "+")
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Big, green people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is quiet then Charlie is cold.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "+"))
If Charlie is big and Charlie is green then Charlie is red.
((("Charlie" "is" "big" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "red" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule4))]
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule4))]
("Charlie" "is" "cold" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is green.[(triple1)] @1: Charlie is big.[(((triple1) -> rule2))] @2: Charlie is quiet.[(((((triple1) -> rule2) triple1) -> rule3))] Charlie is red.[(((((triple1) -> rule2) triple1) -> rule5))] @3: Charlie is cold.[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3