Charlie is cold. Erin is cold. If something is smart and blue then it is kind. Cold things are blue. All blue things are smart. If Erin is smart and Erin is cold then Erin is furry. If something is smart and cold then it is furry. If something is cold then it is nice. All cold things are furry. All quiet things are furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If something is smart and blue then it is kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Erin is smart and Erin is cold then Erin is furry.
((("Erin" "is" "smart" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
If something is smart and cold then it is furry.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is furry.
True
2
proof
[(((triple2) -> rule7) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule5))]
("Erin" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule7) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule5))]
("Erin" "is" "furry" "-")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Charlie is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Erin" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
True
6
proof
[(((((((triple2) -> rule2)) -> rule3) ((triple2) -> rule2)) -> rule1))]
("Erin" "is" "kind" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2) -> (rule2 % int3))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Charlie is not kind.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Erin is cold.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule2))] Charlie is furry.[(((triple1) -> rule7) OR ((((((triple1) -> rule2)) -> rule3) triple1) -> rule5))] Charlie is nice.[(((triple1) -> rule6))] Erin is blue.[(((triple2) -> rule2))] Erin is furry.[(((triple2) -> rule7) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule2)) -> rule3) triple2) -> rule5))] Erin is nice.[(((triple2) -> rule6))] @2: Charlie is smart.[(((((triple1) -> rule2)) -> rule3))] Erin is smart.[(((((triple2) -> rule2)) -> rule3))] @3: Charlie is kind.[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))] Erin is kind.[(((((((triple2) -> rule2)) -> rule3) ((triple2) -> rule2)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2) -> (rule2 % int3))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3