Erin is blue. Erin is kind. Erin is round. Erin is smart. Erin is white. Harry is rough. Harry is round. If Harry is rough and Harry is smart then Harry is white. If Erin is rough and Erin is kind then Erin is smart. Smart things are white. White, blue things are kind. If something is smart then it is round. Smart things are blue. All rough, blue things are kind. All rough, round things are smart.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is rough and Harry is smart then Harry is white.
((("Harry" "is" "rough" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "white" "+"))
If Erin is rough and Erin is kind then Erin is smart.
((("Erin" "is" "rough" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "smart" "+"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
White, blue things are kind.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All rough, blue things are kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All rough, round things are smart.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Erin is not blue.
False
1
inv-proof
[(triple1 OR ((triple4) -> rule6))]
("Erin" "is" "blue" "-")
triple1
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is smart.
True
3
proof
[(((triple6 triple7) -> rule8))]
("Harry" "is" "smart" "+")
((triple6 triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
3
inv-proof
[(((triple6 triple7) -> rule8))]
("Harry" "is" "smart" "-")
((triple6 triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
True
4
proof
[(((((triple6 triple7) -> rule8)) -> rule3) OR ((triple6 ((triple6 triple7) -> rule8)) -> rule1))]
("Harry" "is" "white" "+")
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple6 ((triple6 triple7) -> (rule8 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple6 triple7) -> rule8)) -> rule3) OR ((triple6 ((triple6 triple7) -> rule8)) -> rule1))]
("Harry" "is" "white" "-")
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple6 ((triple6 triple7) -> (rule8 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
True
6
proof
[(((triple6 ((((triple6 triple7) -> rule8)) -> rule6)) -> rule7) OR ((((((triple6 triple7) -> rule8)) -> rule3) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4) OR ((((triple6 ((triple6 triple7) -> rule8)) -> rule1) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4))]
("Harry" "is" "kind" "+")
((triple6 ((((triple6 triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple6 triple7) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((triple6 ((triple6 triple7) -> (rule8 % int4))) -> (rule1 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is not kind.
False
6
inv-proof
[(((triple6 ((((triple6 triple7) -> rule8)) -> rule6)) -> rule7) OR ((((((triple6 triple7) -> rule8)) -> rule3) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4) OR ((((triple6 ((triple6 triple7) -> rule8)) -> rule1) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4))]
("Harry" "is" "kind" "-")
((triple6 ((((triple6 triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple6 triple7) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((triple6 ((triple6 triple7) -> (rule8 % int4))) -> (rule1 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Erin is blue.[(triple1 OR ((triple4) -> rule6))] Erin is kind.[(triple2 OR ((triple5 triple1) -> rule4) OR ((triple5 ((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule3) triple1) -> rule4) OR ((((triple4) -> rule3) ((triple4) -> rule6)) -> rule4))] Erin is round.[(triple3 OR ((triple4) -> rule5))] Erin is smart.[(triple4)] Erin is white.[(triple5 OR ((triple4) -> rule3))] Harry is rough.[(triple6)] Harry is round.[(triple7)] @1: Harry is smart.[(((triple6 triple7) -> rule8))] @2: Harry is blue.[(((((triple6 triple7) -> rule8)) -> rule6))] Harry is white.[(((((triple6 triple7) -> rule8)) -> rule3) OR ((triple6 ((triple6 triple7) -> rule8)) -> rule1))] @3: Harry is kind.[(((triple6 ((((triple6 triple7) -> rule8)) -> rule6)) -> rule7) OR ((((((triple6 triple7) -> rule8)) -> rule3) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4) OR ((((triple6 ((triple6 triple7) -> rule8)) -> rule1) ((((triple6 triple7) -> rule8)) -> rule6)) -> rule4))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
((triple5 triple1) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple5 ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple3
((triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
((triple4) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Harry is smart.
("Harry" "is" "smart" "+")
((triple6 triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple6 triple7) -> (rule8 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple6 ((triple6 triple7) -> (rule8 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple6 ((((triple6 triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple6 triple7) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((triple6 ((triple6 triple7) -> (rule8 % int4))) -> (rule1 % int3)) ((((triple6 triple7) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4