Erin is smart. If something is white then it is cold. Green things are cold. All furry, white things are smart. If Erin is green and Erin is not furry then Erin is red. Smart, big things are green. All furry, smart things are not big. Smart things are big. If something is cold then it is red.
Erin is smart.
("Erin" "is" "smart" "+")
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Erin is green and Erin is not furry then Erin is red.
((("Erin" "is" "green" "+") ("Erin" "is" "furry" "~")) -> ("Erin" "is" "red" "+"))
Smart, big things are green.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All furry, smart things are not big.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "-"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple1)]
("Erin" "is" "smart" "-")
triple1
Erin is big.
True
2
proof
[(((triple1) -> rule7))]
("Erin" "is" "big" "+")
((triple1) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("Erin" "is" "big" "-")
((triple1) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
True
4
proof
[(((triple1 ((triple1) -> rule7)) -> rule5))]
("Erin" "is" "green" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule7)) -> rule5))]
("Erin" "is" "green" "-")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
True
5
proof
[(((((triple1 ((triple1) -> rule7)) -> rule5)) -> rule2))]
("Erin" "is" "cold" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule7)) -> rule5)) -> rule2))]
("Erin" "is" "cold" "-")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Erin is smart.[(triple1)] @1: Erin is big.[(((triple1) -> rule7))] @2: Erin is green.[(((triple1 ((triple1) -> rule7)) -> rule5))] @3: Erin is cold.[(((((triple1 ((triple1) -> rule7)) -> rule5)) -> rule2))] @4: Erin is red.[(((((((triple1 ((triple1) -> rule7)) -> rule5)) -> rule2)) -> rule8))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((((triple1 ((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4