Anne is smart. Dave is cold. Erin is furry. Fiona is big. If Erin is furry and Erin is green then Erin is rough. If something is furry then it is green. If something is smart and rough then it is cold. Big, cold things are smart. Rough things are big. If Erin is big then Erin is cold.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If Erin is furry and Erin is green then Erin is rough.
((("Erin" "is" "furry" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "rough" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is smart and rough then it is cold.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Big, cold things are smart.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Erin is big then Erin is cold.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "cold" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Erin is green.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "green" "+")
((triple3) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "green" "-")
((triple3) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Erin" "is" "rough" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Erin" "is" "rough" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
True
5
proof
[(((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5))]
("Erin" "is" "big" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not big.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5))]
("Erin" "is" "big" "-")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is smart.[(triple1)] Dave is cold.[(triple2)] Erin is furry.[(triple3)] Fiona is big.[(triple4)] @1: Erin is green.[(((triple3) -> rule2))] @2: Erin is rough.[(((triple3 ((triple3) -> rule2)) -> rule1))] @3: Erin is big.[(((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5))] @4: Erin is cold.[(((((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5)) -> rule6))] @5: Erin is smart.[(((((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5) ((((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule5)) -> rule6)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple3 ((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3 ((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) ((((((triple3 ((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5