Erin is big. Erin is smart. Erin is young. Harry is big. Harry is cold. Harry is furry. Harry is quiet. Harry is smart. Harry is white. Harry is young. If something is young then it is cold. All young things are cold. All quiet things are cold. If Harry is young then Harry is smart. If something is smart and cold then it is white. If Harry is cold then Harry is white. If Harry is cold and Harry is not quiet then Harry is furry. If something is white and not quiet then it is not young.
Erin is big.
("Erin" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Harry is young then Harry is smart.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "smart" "+"))
If something is smart and cold then it is white.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Harry is cold then Harry is white.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "white" "+"))
If Harry is cold and Harry is not quiet then Harry is furry.
((("Harry" "is" "cold" "+") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "furry" "+"))
If something is white and not quiet then it is not young.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
Harry is smart.
True
1
proof
[(triple8 OR ((triple10) -> rule4))]
("Harry" "is" "smart" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not quiet.
False
1
inv-proof
[(triple7)]
("Harry" "is" "quiet" "-")
triple7
Erin is cold.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Erin" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
True
4
proof
[(((triple2 ((triple3) -> rule1)) -> rule5) OR ((triple2 ((triple3) -> rule2)) -> rule5))]
("Erin" "is" "white" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple2 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not white.
False
4
inv-proof
[(((triple2 ((triple3) -> rule1)) -> rule5) OR ((triple2 ((triple3) -> rule2)) -> rule5))]
("Erin" "is" "white" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple2 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Erin is big.[(triple1)] Erin is smart.[(triple2)] Erin is young.[(triple3)] Harry is big.[(triple4)] Harry is cold.[(triple5 OR ((triple10) -> rule1) OR ((triple10) -> rule2) OR ((triple7) -> rule3))] Harry is furry.[(triple6)] Harry is quiet.[(triple7)] Harry is smart.[(triple8 OR ((triple10) -> rule4))] Harry is white.[(triple9 OR ((triple5) -> rule6) OR ((triple8 triple5) -> rule5) OR ((((triple10) -> rule1)) -> rule6) OR ((((triple10) -> rule2)) -> rule6) OR ((((triple7) -> rule3)) -> rule6) OR ((triple8 ((triple10) -> rule1)) -> rule5) OR ((triple8 ((triple10) -> rule2)) -> rule5) OR ((triple8 ((triple7) -> rule3)) -> rule5) OR ((((triple10) -> rule4) triple5) -> rule5) OR ((((triple10) -> rule4) ((triple10) -> rule1)) -> rule5) OR ((((triple10) -> rule4) ((triple10) -> rule2)) -> rule5) OR ((((triple10) -> rule4) ((triple7) -> rule3)) -> rule5))] Harry is young.[(triple10)] @1: Erin is cold.[(((triple3) -> rule1) OR ((triple3) -> rule2))] @2: Erin is white.[(((triple2 ((triple3) -> rule1)) -> rule5) OR ((triple2 ((triple3) -> rule2)) -> rule5))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
((triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is smart.
("Harry" "is" "smart" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple9
((triple5) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8 triple5) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple8 ((triple10) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple8 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple8 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple10) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple10) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple10) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple10) -> (rule4 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple10
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple2 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2