Charlie is round. Erin is round. If something is round then it is furry. All round things are furry. All rough things are big. If something is furry then it is rough. All big things are round. Rough, big things are smart.
Charlie is round.
("Charlie" "is" "round" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Rough, big things are smart.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Erin is round.
True
1
proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Erin is not round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "-")
triple2
Erin is furry.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("Erin" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("Erin" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule2)) -> rule4))]
("Erin" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule2)) -> rule4))]
("Erin" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((((triple2) -> rule2)) -> rule4)) -> rule3))]
("Erin" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is not big.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule4)) -> rule3))]
("Charlie" "is" "big" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is round.[(triple1)] Erin is round.[(triple2)] @1: Charlie is furry.[(((triple1) -> rule1) OR ((triple1) -> rule2))] Erin is furry.[(((triple2) -> rule1) OR ((triple2) -> rule2))] @2: Charlie is rough.[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] Erin is rough.[(((((triple2) -> rule1)) -> rule4) OR ((((triple2) -> rule2)) -> rule4))] @3: Charlie is big.[(((((((triple1) -> rule1)) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule4)) -> rule3))] Erin is big.[(((((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((((triple2) -> rule2)) -> rule4)) -> rule3))] @4: Charlie is smart.[(((((((triple1) -> rule1)) -> rule4) ((((((triple1) -> rule1)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple1) -> rule1)) -> rule4) ((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple1) -> rule2)) -> rule4) ((((((triple1) -> rule1)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple1) -> rule2)) -> rule4) ((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6))] Erin is smart.[(((((((triple2) -> rule1)) -> rule4) ((((((triple2) -> rule1)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple2) -> rule1)) -> rule4) ((((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule1)) -> rule4)) -> rule3)) -> rule6) OR ((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule6))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple2) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((triple2) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4