Anne is blue. Erin is smart. Fiona is rough. Harry is cold. If Erin is furry and Erin is rough then Erin is blue. If something is cold then it is rough. If something is big and rough then it is quiet. If something is cold then it is smart. All smart, rough things are big. All furry things are smart. All smart, big things are quiet. All cold, smart things are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Erin is furry and Erin is rough then Erin is blue.
((("Erin" "is" "furry" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "blue" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is big and rough then it is quiet.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All smart, rough things are big.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All smart, big things are quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All cold, smart things are rough.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Erin is smart.[(triple2)] Fiona is rough.[(triple3)] Harry is cold.[(triple4)] @1: Harry is rough.[(((triple4) -> rule2) OR ((triple4 ((triple4) -> rule4)) -> rule8))] Harry is smart.[(((triple4) -> rule4))] @2: Harry is big.[(((((triple4) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule4) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule5))] @3: Harry is quiet.[(((((triple4) -> rule4) ((((triple4) -> rule4) ((triple4) -> rule2)) -> rule5)) -> rule7) OR ((((((triple4) -> rule4) ((triple4) -> rule2)) -> rule5) ((triple4) -> rule2)) -> rule3) OR ((((((triple4) -> rule4) ((triple4) -> rule2)) -> rule5) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule3) OR ((((triple4) -> rule4) ((((triple4) -> rule4) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule5)) -> rule7) OR ((((((triple4) -> rule4) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule5) ((triple4) -> rule2)) -> rule3) OR ((((((triple4) -> rule4) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule5) ((triple4 ((triple4) -> rule4)) -> rule8)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule4 % int3)) ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple4) -> (rule4 % int3)) ((triple4 ((triple4) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule4 % int4)) ((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((triple4) -> (rule4 % int4)) ((triple4) -> (rule2 % int3))) -> (rule5 % int2)) ((triple4) -> (rule2 % int3))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((triple4) -> (rule4 % int4)) ((triple4) -> (rule2 % int3))) -> (rule5 % int2)) ((triple4 ((triple4) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule4 % int4)) ((triple4 ((triple4) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((triple4) -> (rule4 % int4)) ((triple4 ((triple4) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((triple4) -> (rule2 % int3))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((triple4) -> (rule4 % int4)) ((triple4 ((triple4) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((triple4 ((triple4) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4