Harry is green. Quiet things are round. Quiet things are round. All smart, green things are quiet. If something is green and furry then it is not quiet. Round, smart things are cold. Green things are smart.
Harry is green.
("Harry" "is" "green" "+")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All smart, green things are quiet.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is green and furry then it is not quiet.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "-"))
Round, smart things are cold.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Harry is green.
True
1
proof
[(triple1)]
("Harry" "is" "green" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple1)]
("Harry" "is" "green" "-")
triple1
Harry is smart.
True
2
proof
[(((triple1) -> rule6))]
("Harry" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Harry" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule3))]
("Harry" "is" "quiet" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule3))]
("Harry" "is" "quiet" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
True
5
proof
[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule1) OR ((((((triple1) -> rule6) triple1) -> rule3)) -> rule2))]
("Harry" "is" "round" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule1) OR ((((((triple1) -> rule6) triple1) -> rule3)) -> rule2))]
("Harry" "is" "round" "-")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Harry is green.[(triple1)] @1: Harry is smart.[(((triple1) -> rule6))] @2: Harry is quiet.[(((((triple1) -> rule6) triple1) -> rule3))] @3: Harry is round.[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule1) OR ((((((triple1) -> rule6) triple1) -> rule3)) -> rule2))] @4: Harry is cold.[(((((((((triple1) -> rule6) triple1) -> rule3)) -> rule1) ((triple1) -> rule6)) -> rule5) OR ((((((((triple1) -> rule6) triple1) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule5))]
Harry is green.
("Harry" "is" "green" "+")
triple1
Harry is smart.
("Harry" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((((triple1) -> (rule6 % int4)) triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule6 % int4))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple1) -> (rule6 % int4)) triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int4))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4