Erin is green. Erin is kind. Harry is kind. All kind things are green. If Harry is nice then Harry is kind. Furry things are smart. If something is kind and green then it is quiet. Smart, blue things are quiet. All kind, green things are furry. Blue, nice things are furry. If Erin is blue and Erin is not green then Erin is not quiet.
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Harry is nice then Harry is kind.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "kind" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is kind and green then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Smart, blue things are quiet.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All kind, green things are furry.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Blue, nice things are furry.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Erin is blue and Erin is not green then Erin is not quiet.
((("Erin" "is" "blue" "+") ("Erin" "is" "green" "~")) -> ("Erin" "is" "quiet" "-"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Harry is not kind.
False
1
inv-proof
[(triple3)]
("Harry" "is" "kind" "-")
triple3
Erin is quiet.
True
3
proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Erin" "is" "quiet" "+")
((triple2 triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Erin" "is" "quiet" "-")
((triple2 triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Harry is quiet.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule4))]
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("Harry" "is" "furry" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not smart.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Erin is green.[(triple1 OR ((triple2) -> rule1))] Erin is kind.[(triple2)] Harry is kind.[(triple3)] @1: Erin is furry.[(((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule1)) -> rule6))] Erin is quiet.[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule1)) -> rule4))] Harry is green.[(((triple3) -> rule1))] @2: Erin is smart.[(((((triple2 triple1) -> rule6)) -> rule3) OR ((((triple2 ((triple2) -> rule1)) -> rule6)) -> rule3))] Harry is furry.[(((triple3 ((triple3) -> rule1)) -> rule6))] Harry is quiet.[(((triple3 ((triple3) -> rule1)) -> rule4))] @3: Harry is smart.[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
((triple2) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
((triple2 triple1) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2 triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3